Theorem uzind 6207

Description: Induction on the upper integers that start at M. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis.

Hypotheses

Ref	Expression
uzind.1	⊢ (j = M → (φ ↔ ψ))
uzind.2	⊢ (j = k → (φ ↔ χ))
uzind.3	⊢ (j = (k + 1) → (φ ↔ θ))
uzind.4	⊢ (j = N → (φ ↔ τ))
uzind.5	⊢ (M ∈ ℤ → ψ)
uzind.6	⊢ ((M ∈ ℤ ⋀ k ∈ ℤ ⋀ M ≤ k) → (χ → θ))

Assertion

Ref	Expression
uzind	⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ M ≤ N) → τ)

Distinct variable groups:   j,N   ψ,j   χ,j   θ,j   τ,j   φ,k   j,k,M

Proof of Theorem uzind

Step	Hyp	Ref	Expression
1		zret 6141	. . . . . . . . . . 11 ⊢ (M ∈ ℤ → M ∈ ℝ)
2		leidt 5543	. . . . . . . . . . 11 ⊢ (M ∈ ℝ → M ≤ M)
3	1, 2	syl 10	. . . . . . . . . 10 ⊢ (M ∈ ℤ → M ≤ M)
4		uzind.5	. . . . . . . . . 10 ⊢ (M ∈ ℤ → ψ)
5	3, 4	jca 288	. . . . . . . . 9 ⊢ (M ∈ ℤ → (M ≤ M ⋀ ψ))
6	5	ancli 296	. . . . . . . 8 ⊢ (M ∈ ℤ → (M ∈ ℤ ⋀ (M ≤ M ⋀ ψ)))
7		breq2 2628	. . . . . . . . . 10 ⊢ (j = M → (M ≤ j ↔ M ≤ M))
8		uzind.1	. . . . . . . . . 10 ⊢ (j = M → (φ ↔ ψ))
9	7, 8	anbi12d 630	. . . . . . . . 9 ⊢ (j = M → ((M ≤ j ⋀ φ) ↔ (M ≤ M ⋀ ψ)))
10	9	elrab 1908	. . . . . . . 8 ⊢ (M ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ↔ (M ∈ ℤ ⋀ (M ≤ M ⋀ ψ)))
11	6, 10	sylibr 200	. . . . . . 7 ⊢ (M ∈ ℤ → M ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)})
12		peano2z 6168	. . . . . . . . . . . 12 ⊢ (k ∈ ℤ → (k + 1) ∈ ℤ)
13	12	a1i 8	. . . . . . . . . . 11 ⊢ (M ∈ ℤ → (k ∈ ℤ → (k + 1) ∈ ℤ))
14	13	adantrd 393	. . . . . . . . . 10 ⊢ (M ∈ ℤ → ((k ∈ ℤ ⋀ (M ≤ k ⋀ χ)) → (k + 1) ∈ ℤ))
15		ltp1t 5813	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℝ → k < (k + 1))
16	15	adantl 390	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ) → k < (k + 1))
17		lelttrt 5535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ ⋀ (k + 1) ∈ ℝ) → ((M ≤ k ⋀ k < (k + 1)) → M < (k + 1)))
18	17	3expb 836	. . . . . . . . . . . . . . . . . 18 ⊢ ((M ∈ ℝ ⋀ (k ∈ ℝ ⋀ (k + 1) ∈ ℝ)) → ((M ≤ k ⋀ k < (k + 1)) → M < (k + 1)))
19		peano2re 5448	. . . . . . . . . . . . . . . . . . 19 ⊢ (k ∈ ℝ → (k + 1) ∈ ℝ)
20	19	ancli 296	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℝ → (k ∈ ℝ ⋀ (k + 1) ∈ ℝ))
21	18, 20	sylan2 453	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ) → ((M ≤ k ⋀ k < (k + 1)) → M < (k + 1)))
22	16, 21	mpan2d 704	. . . . . . . . . . . . . . . 16 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ) → (M ≤ k → M < (k + 1)))
23		ltlet 5532	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℝ ⋀ (k + 1) ∈ ℝ) → (M < (k + 1) → M ≤ (k + 1)))
24	23, 19	sylan2 453	. . . . . . . . . . . . . . . 16 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ) → (M < (k + 1) → M ≤ (k + 1)))
25	22, 24	syld 27	. . . . . . . . . . . . . . 15 ⊢ ((M ∈ ℝ ⋀ k ∈ ℝ) → (M ≤ k → M ≤ (k + 1)))
26		zret 6141	. . . . . . . . . . . . . . 15 ⊢ (k ∈ ℤ → k ∈ ℝ)
27	25, 1, 26	syl2an 456	. . . . . . . . . . . . . 14 ⊢ ((M ∈ ℤ ⋀ k ∈ ℤ) → (M ≤ k → M ≤ (k + 1)))
28	27	adantrd 393	. . . . . . . . . . . . 13 ⊢ ((M ∈ ℤ ⋀ k ∈ ℤ) → ((M ≤ k ⋀ χ) → M ≤ (k + 1)))
29	28	exp4b 381	. . . . . . . . . . . 12 ⊢ (M ∈ ℤ → (k ∈ ℤ → (M ≤ k → (χ → M ≤ (k + 1)))))
30	29	imp4d 367	. . . . . . . . . . 11 ⊢ (M ∈ ℤ → ((k ∈ ℤ ⋀ (M ≤ k ⋀ χ)) → M ≤ (k + 1)))
31		uzind.6	. . . . . . . . . . . . 13 ⊢ ((M ∈ ℤ ⋀ k ∈ ℤ ⋀ M ≤ k) → (χ → θ))
32	31	3exp 834	. . . . . . . . . . . 12 ⊢ (M ∈ ℤ → (k ∈ ℤ → (M ≤ k → (χ → θ))))
33	32	imp4d 367	. . . . . . . . . . 11 ⊢ (M ∈ ℤ → ((k ∈ ℤ ⋀ (M ≤ k ⋀ χ)) → θ))
34	30, 33	jcad 602	. . . . . . . . . 10 ⊢ (M ∈ ℤ → ((k ∈ ℤ ⋀ (M ≤ k ⋀ χ)) → (M ≤ (k + 1) ⋀ θ)))
35	14, 34	jcad 602	. . . . . . . . 9 ⊢ (M ∈ ℤ → ((k ∈ ℤ ⋀ (M ≤ k ⋀ χ)) → ((k + 1) ∈ ℤ ⋀ (M ≤ (k + 1) ⋀ θ))))
36		breq2 2628	. . . . . . . . . . 11 ⊢ (j = k → (M ≤ j ↔ M ≤ k))
37		uzind.2	. . . . . . . . . . 11 ⊢ (j = k → (φ ↔ χ))
38	36, 37	anbi12d 630	. . . . . . . . . 10 ⊢ (j = k → ((M ≤ j ⋀ φ) ↔ (M ≤ k ⋀ χ)))
39	38	elrab 1908	. . . . . . . . 9 ⊢ (k ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ↔ (k ∈ ℤ ⋀ (M ≤ k ⋀ χ)))
40		breq2 2628	. . . . . . . . . . 11 ⊢ (j = (k + 1) → (M ≤ j ↔ M ≤ (k + 1)))
41		uzind.3	. . . . . . . . . . 11 ⊢ (j = (k + 1) → (φ ↔ θ))
42	40, 41	anbi12d 630	. . . . . . . . . 10 ⊢ (j = (k + 1) → ((M ≤ j ⋀ φ) ↔ (M ≤ (k + 1) ⋀ θ)))
43	42	elrab 1908	. . . . . . . . 9 ⊢ ((k + 1) ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ↔ ((k + 1) ∈ ℤ ⋀ (M ≤ (k + 1) ⋀ θ)))
44	35, 39, 43	3imtr4g 555	. . . . . . . 8 ⊢ (M ∈ ℤ → (k ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} → (k + 1) ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)}))
45	44	r19.21aiv 1716	. . . . . . 7 ⊢ (M ∈ ℤ → ∀k ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} (k + 1) ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)})
46		zex 6146	. . . . . . . . 9 ⊢ ℤ ∈ V
47	46	rabex 2730	. . . . . . . 8 ⊢ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ∈ V
48	47	peano5uzt 6206	. . . . . . 7 ⊢ (M ∈ ℤ → ((M ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ⋀ ∀k ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} (k + 1) ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)}) → {w ∈ ℤ∣M ≤ w} ⊆ {j ∈ ℤ∣(M ≤ j ⋀ φ)}))
49	11, 45, 48	mp2and 705	. . . . . 6 ⊢ (M ∈ ℤ → {w ∈ ℤ∣M ≤ w} ⊆ {j ∈ ℤ∣(M ≤ j ⋀ φ)})
50	49	sseld 2070	. . . . 5 ⊢ (M ∈ ℤ → (N ∈ {w ∈ ℤ∣M ≤ w} → N ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)}))
51		breq2 2628	. . . . . 6 ⊢ (w = N → (M ≤ w ↔ M ≤ N))
52	51	elrab 1908	. . . . 5 ⊢ (N ∈ {w ∈ ℤ∣M ≤ w} ↔ (N ∈ ℤ ⋀ M ≤ N))
53		breq2 2628	. . . . . . 7 ⊢ (j = N → (M ≤ j ↔ M ≤ N))
54		uzind.4	. . . . . . 7 ⊢ (j = N → (φ ↔ τ))
55	53, 54	anbi12d 630	. . . . . 6 ⊢ (j = N → ((M ≤ j ⋀ φ) ↔ (M ≤ N ⋀ τ)))
56	55	elrab 1908	. . . . 5 ⊢ (N ∈ {j ∈ ℤ∣(M ≤ j ⋀ φ)} ↔ (N ∈ ℤ ⋀ (M ≤ N ⋀ τ)))
57	50, 52, 56	3imtr3g 554	. . . 4 ⊢ (M ∈ ℤ → ((N ∈ ℤ ⋀ M ≤ N) → (N ∈ ℤ ⋀ (M ≤ N ⋀ τ))))
58	57	3impib 833	. . 3 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ M ≤ N) → (N ∈ ℤ ⋀ (M ≤ N ⋀ τ)))
59	58	pm3.27d 325	. 2 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ M ≤ N) → (M ≤ N ⋀ τ))
60	59	pm3.27d 325	1 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ M ≤ N) → τ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960  ∀wral 1648  {crab 1651   ⊆ wss 2050   class class class wbr 2624  (class class class)co 3969  ℝcr 5245  1c1 5247   + caddc 5249   ≤ cle 5307  ℤcz 5310   < clt 5498

This theorem is referenced by:  uzind2 6208  uzind3 6209  nn0ind 6214  om2uzran 6301

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-en 4374  df-dom 4375  df-sdom 4376  df-ni 5012  df-pli 5013  df-mi 5014  df-lti 5015  df-plpq 5047  df-mpq 5048  df-enq 5049  df-nq 5050  df-plq 5051  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-1p 5099  df-plp 5100  df-mp 5101  df-ltp 5102  df-plpr 5176  df-mpr 5177  df-enr 5178  df-nr 5179  df-plr 5180  df-mr 5181  df-ltr 5182  df-0r 5183  df-1r 5184  df-m1r 5185  df-c 5252  df-0 5253  df-1 5254  df-i 5255  df-r 5256  df-plus 5257  df-mul 5258  df-lt 5259  df-sub 5368  df-neg 5370  df-pnf 5499  df-mnf 5500  df-xr 5501  df-ltxr 5502  df-le 5503  df-n 5927  df-n0 6102  df-z 6138

Copyright terms: Public domain