Theorem peano2uz 12927

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 1152	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
2		peano2z 12637	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
3	2	3ad2ant2 1150	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ)
4		zre 12597	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 12597	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		letrp1 12061	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
7	5, 6	syl3an2 1180	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
8	4, 7	syl3an1 1179	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1))
9	1, 3, 8	3jca 1144	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
10		eluz2 12870	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
11		eluz2 12870	. 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
12	9, 10, 11	3imtr4i 295	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ w3a 1101   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6539  (class class class)co 7413  ℝcr 11101  1c1 11103   + caddc 11105   ≤ cle 11246  ℤcz 12593  ℤ_≥cuz 12864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-cnex 11158  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-nn 12236  df-n0 12507  df-z 12594  df-uz 12865

This theorem is referenced by:  peano2uzs  12928  peano2uzr  12929  uzaddcl  12930  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  16096  pcfac  16961  gsumsplit1r  18747  gsumprval  18748  telgsumfzslem  20060  telgsumfzs  20061  dvply2g  26417  aaliou3lem2  26475  ppinprm  27284  chtnprm  27286  ppiublem1  27334  chtublem  27343  chtub  27344  bposlem6  27421  pntlemf  27737  ostth2lem2  27766  clwwlkvbij  30407  fzsplit3  33081  esumcvg  34423  sseqf  34729  gsumnunsn  34878  signstfvp  34905  iprodefisumlem  36167  poimirlem1  38197  poimirlem2  38198  poimirlem3  38199  poimirlem4  38200  poimirlem6  38202  poimirlem7  38203  poimirlem8  38204  poimirlem9  38205  poimirlem12  38208  poimirlem13  38209  poimirlem14  38210  poimirlem15  38211  poimirlem16  38212  poimirlem17  38213  poimirlem18  38214  poimirlem19  38215  poimirlem20  38216  poimirlem21  38217  poimirlem22  38218  poimirlem23  38219  poimirlem24  38220  poimirlem26  38222  poimirlem27  38223  poimirlem31  38227  poimirlem32  38228  sdclem2  38318  fdc  38321  mettrifi  38333  bfplem2  38399  rexrabdioph  43450  monotuz  43597  wallispilem1  46708  dirkertrigeqlem2  46742  sge0p1  47057  carageniuncllem1  47164  iccpartres  48093  iccelpart  48108  fmtno4prm  48253