Theorem peano2uz 12926

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 1154	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
2		peano2z 12636	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
3	2	3ad2ant2 1152	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ)
4		zre 12596	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 12596	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		letrp1 12060	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
7	5, 6	syl3an2 1182	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
8	4, 7	syl3an1 1181	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
9	1, 3, 8	3jca 1146	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
10		eluz2 12869	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
11		eluz2 12869	. 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
12	9, 10, 11	3imtr4i 295	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ w3a 1103   ∈ wcel 2143   class class class wbr 5110  ‘cfv 6538  (class class class)co 7412  ℝcr 11100  1c1 11102   + caddc 11104   ≤ cle 11245  ℤcz 12592  ℤ_≥cuz 12863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-n0 12506  df-z 12593  df-uz 12864

This theorem is referenced by:  peano2uzs  12927  peano2uzr  12928  uzaddcl  12929  fzsplit  13580  fzssp1  13597  fzsuc  13601  fzpred  13602  fzp1ss  13605  fzp1elp1  13607  fztp  13610  fzdif1  13635  fzneuz  13638  fzosplitsnm1  13771  fzofzp1  13795  fzosplitsn  13807  fzosplitpr  13808  fzostep1  13817  om2uzuzi  13987  uzrdgsuci  13998  fzen2  14007  fzfi  14010  seqsplit  14073  seqf1olem1  14079  seqf1olem2  14080  seqz  14088  faclbnd3  14330  bcm1k  14353  seqcoll  14503  seqcoll2  14504  swrds1  14706  pfxccatpfx2  14776  clim2ser  15708  clim2ser2  15709  serf0  15734  iseraltlem2  15736  iseralt  15738  fsump1  15809  fsump1i  15822  fsumparts  15860  cvgcmp  15870  isum1p  15897  isumsup2  15902  climcndslem1  15905  climcndslem2  15906  climcnds  15907  cvgrat  15939  mertenslem1  15940  clim2prod  15944  clim2div  15945  ntrivcvgfvn0  15955  fprodntriv  15998  fprodp1  16025  fprodabs  16030  binomfallfaclem2  16095  pcfac  16960  gsumsplit1r  18746  gsumprval  18747  telgsumfzslem  20059  telgsumfzs  20060  dvply2g  26427  aaliou3lem2  26487  ppinprm  27297  chtnprm  27299  ppiublem1  27347  chtublem  27356  chtub  27357  bposlem6  27434  pntlemf  27750  ostth2lem2  27779  clwwlkvbij  30445  fzsplit3  33119  esumcvg  34457  sseqf  34763  gsumnunsn  34912  signstfvp  34939  iprodefisumlem  36213  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem9  38261  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem26  38278  poimirlem27  38279  poimirlem31  38283  poimirlem32  38284  sdclem2  38374  fdc  38377  mettrifi  38389  bfplem2  38455  rexrabdioph  43504  monotuz  43651  wallispilem1  46762  dirkertrigeqlem2  46796  sge0p1  47111  carageniuncllem1  47218  iccpartres  48150  iccelpart  48165  fmtno4prm  48310