Theorem peano2uz 12721

Description: Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.)

Assertion

Ref	Expression
peano2uz	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))

Proof of Theorem peano2uz

Step	Hyp	Ref	Expression
1		simp1 1135	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
2		peano2z 12441	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
3	2	3ad2ant2 1133	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ)
4		zre 12403	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 12403	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		letrp1 11899	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
7	5, 6	syl3an2 1163	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
8	4, 7	syl3an1 1162	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
9	1, 3, 8	3jca 1127	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
10		eluz2 12668	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
11		eluz2 12668	. 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
12	9, 10, 11	3imtr4i 291	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2105   class class class wbr 5087  ‘cfv 6466  (class class class)co 7317  ℝcr 10950  1c1 10952   + caddc 10954   ≤ cle 11090  ℤcz 12399  ℤ_≥cuz 12662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-er 8548  df-en 8784  df-dom 8785  df-sdom 8786  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-n0 12314  df-z 12400  df-uz 12663

This theorem is referenced by:  peano2uzs  12722  peano2uzr  12723  uzaddcl  12724  fzsplit  13362  fzssp1  13379  fzsuc  13383  fzpred  13384  fzp1ss  13387  fzp1elp1  13389  fztp  13392  fzneuz  13417  fzosplitsnm1  13542  fzofzp1  13564  fzosplitsn  13575  fzosplitpr  13576  fzostep1  13583  om2uzuzi  13749  uzrdgsuci  13760  fzen2  13769  fzfi  13772  seqsplit  13836  seqf1olem1  13842  seqf1olem2  13843  seqz  13851  faclbnd3  14086  bcm1k  14109  seqcoll  14257  seqcoll2  14258  swrds1  14458  pfxccatpfx2  14529  clim2ser  15445  clim2ser2  15446  serf0  15471  iseraltlem2  15473  iseralt  15475  fsump1  15547  fsump1i  15560  fsumparts  15597  cvgcmp  15607  isum1p  15632  isumsup2  15637  climcndslem1  15640  climcndslem2  15641  climcnds  15642  cvgrat  15674  mertenslem1  15675  clim2prod  15679  clim2div  15680  ntrivcvgfvn0  15690  fprodntriv  15731  fprodp1  15758  fprodabs  15763  binomfallfaclem2  15829  pcfac  16677  gsumsplit1r  18448  gsumprval  18449  telgsumfzslem  19664  telgsumfzs  19665  dvply2g  25528  aaliou3lem2  25586  ppinprm  26384  chtnprm  26386  ppiublem1  26433  chtublem  26442  chtub  26443  bposlem6  26520  pntlemf  26836  ostth2lem2  26865  clwwlkvbij  28613  fzsplit3  31250  esumcvg  32194  sseqf  32499  gsumnunsn  32660  signstfvp  32690  iprodefisumlem  33841  poimirlem1  35850  poimirlem2  35851  poimirlem3  35852  poimirlem4  35853  poimirlem6  35855  poimirlem7  35856  poimirlem8  35857  poimirlem9  35858  poimirlem12  35861  poimirlem13  35862  poimirlem14  35863  poimirlem15  35864  poimirlem16  35865  poimirlem17  35866  poimirlem18  35867  poimirlem19  35868  poimirlem20  35869  poimirlem21  35870  poimirlem22  35871  poimirlem23  35872  poimirlem24  35873  poimirlem26  35875  poimirlem27  35876  poimirlem31  35880  poimirlem32  35881  sdclem2  35972  fdc  35975  mettrifi  35987  bfplem2  36053  rexrabdioph  40832  monotuz  40980  wallispilem1  43856  dirkertrigeqlem2  43890  sge0p1  44203  carageniuncllem1  44310  iccpartres  45135  iccelpart  45150  fmtno4prm  45292