Theorem uzind4 12850

Description: Induction on the upper set of integers that starts at an integer 𝑀. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.)

Hypotheses

Ref	Expression
uzind4.1	⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))
uzind4.2	⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))
uzind4.3	⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))
uzind4.4	⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))
uzind4.5	⊢ (𝑀 ∈ ℤ → 𝜓)
uzind4.6	⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))

Assertion

Ref	Expression
uzind4	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)

Distinct variable groups:   𝑗,𝑁   𝜓,𝑗   𝜒,𝑗   𝜃,𝑗   𝜏,𝑗   𝜑,𝑘   𝑗,𝑘,𝑀

Allowed substitution hints:   𝜑(𝑗)   𝜓(𝑘)   𝜒(𝑘)   𝜃(𝑘)   𝜏(𝑘)   𝑁(𝑘)

Proof of Theorem uzind4

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluzel2 12787	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		breq2 5079	. . 3 ⊢ (𝑚 = 𝑁 → (𝑀 ≤ 𝑚 ↔ 𝑀 ≤ 𝑁))
3		eluzelz 12792	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
4		eluzle 12795	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)
5	2, 3, 4	elrabd 3634	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ {𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚})
6		uzind4.1	. . 3 ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))
7		uzind4.2	. . 3 ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))
8		uzind4.3	. . 3 ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))
9		uzind4.4	. . 3 ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))
10		uzind4.5	. . 3 ⊢ (𝑀 ∈ ℤ → 𝜓)
11		breq2 5079	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑀 ≤ 𝑚 ↔ 𝑀 ≤ 𝑘))
12	11	elrab 3632	. . . . 5 ⊢ (𝑘 ∈ {𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚} ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘))
13		eluz2 12788	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘))
14	13	biimpri 229	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘) → 𝑘 ∈ (ℤ≥‘𝑀))
15	14	3expb 1122	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑀))
16	12, 15	sylan2b 596	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ {𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚}) → 𝑘 ∈ (ℤ≥‘𝑀))
17		uzind4.6	. . . 4 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))
18	16, 17	syl 17	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ {𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚}) → (𝜒 → 𝜃))
19	6, 7, 8, 9, 10, 18	uzind3 12617	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ {𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚}) → 𝜏)
20	1, 5, 19	syl2anc 586	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1088   = wceq 1543   ∈ wcel 2115  {crab 3388   class class class wbr 5075  ‘cfv 6488  (class class class)co 7359  1c1 11033   + caddc 11035   ≤ cle 11174  ℤcz 12518  ℤ_≥cuz 12782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1970  ax-7 2011  ax-8 2117  ax-9 2125  ax-10 2148  ax-11 2164  ax-12 2185  ax-ext 2708  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7681  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 850  df-3or 1089  df-3an 1090  df-tru 1546  df-fal 1556  df-ex 1783  df-nf 1787  df-sb 2070  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3061  df-reu 3342  df-rab 3389  df-v 3430  df-sbc 3727  df-csb 3835  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-pss 3906  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-om 7810  df-2nd 7935  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783

This theorem is referenced by:  uzind4ALT  12851  uzind4s  12852  uzind4s2  12853  uzind4i  12854  seqexw  13973  seqcl2  13976  seqshft2  13984  seqsplit  13991  seqf1o  13999  seqid2  14004  clim2prod  15847  fprodabs  15933  fprodefsum  16054  seq1st  16534  1stcelcls  23447  caubl  25296  caublcls  25297  volsuplem  25543  cpnord  25923  bcmono  27261  sseqp1  34582  iprodefisumlem  35965  sdclem2  38106  seqpo  38111  mettrifi  38121  incssnn0  43157  dvgrat  44753  monoordxrv  45921  climsuselem1  46049  smonoord  47837