ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  peano2uz GIF version

Theorem peano2uz 8592
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
StepHypRef Expression
1 simp1 913 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
2 peano2z 8308 . . . 4 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
323ad2ant2 935 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → (𝑁 + 1) ∈ ℤ)
4 zre 8276 . . . 4 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5 zre 8276 . . . . 5 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6 letrp1 7859 . . . . 5 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀𝑁) → 𝑀 ≤ (𝑁 + 1))
75, 6syl3an2 1178 . . . 4 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ≤ (𝑁 + 1))
84, 7syl3an1 1177 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ≤ (𝑁 + 1))
91, 3, 83jca 1093 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
10 eluz2 8545 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
11 eluz2 8545 . 2 ((𝑁 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1)))
129, 10, 113imtr4i 194 1 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 894  wcel 1407   class class class wbr 3789  cfv 4927  (class class class)co 5537  cr 6916  1c1 6918   + caddc 6920  cle 7090  cz 8272  cuz 8539
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-coll 3897  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-setind 4287  ax-iinf 4336  ax-cnex 7003  ax-resscn 7004  ax-1cn 7005  ax-1re 7006  ax-icn 7007  ax-addcl 7008  ax-addrcl 7009  ax-mulcl 7010  ax-addcom 7012  ax-addass 7014  ax-distr 7016  ax-i2m1 7017  ax-0id 7020  ax-rnegex 7021  ax-cnre 7023  ax-pre-ltirr 7024  ax-pre-ltwlin 7025  ax-pre-lttrn 7026  ax-pre-ltadd 7028
This theorem depends on definitions:  df-bi 114  df-dc 752  df-3or 895  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-nel 2313  df-ral 2326  df-rex 2327  df-reu 2328  df-rab 2330  df-v 2574  df-sbc 2785  df-csb 2878  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-int 3641  df-iun 3684  df-br 3790  df-opab 3844  df-mpt 3845  df-tr 3880  df-eprel 4051  df-id 4055  df-po 4058  df-iso 4059  df-iord 4128  df-on 4130  df-suc 4133  df-iom 4339  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-f 4931  df-f1 4932  df-fo 4933  df-f1o 4934  df-fv 4935  df-riota 5493  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 5985  df-1o 6029  df-2o 6030  df-oadd 6033  df-omul 6034  df-er 6134  df-ec 6136  df-qs 6140  df-ni 6430  df-pli 6431  df-mi 6432  df-lti 6433  df-plpq 6470  df-mpq 6471  df-enq 6473  df-nqqs 6474  df-plqqs 6475  df-mqqs 6476  df-1nqqs 6477  df-rq 6478  df-ltnqqs 6479  df-enq0 6550  df-nq0 6551  df-0nq0 6552  df-plq0 6553  df-mq0 6554  df-inp 6592  df-i1p 6593  df-iplp 6594  df-iltp 6596  df-enr 6839  df-nr 6840  df-ltr 6843  df-0r 6844  df-1r 6845  df-0 6924  df-1 6925  df-r 6927  df-lt 6930  df-pnf 7091  df-mnf 7092  df-xr 7093  df-ltxr 7094  df-le 7095  df-sub 7217  df-neg 7218  df-inn 7961  df-n0 8210  df-z 8273  df-uz 8540
This theorem is referenced by:  peano2uzs  8593  peano2uzr  8594  uzaddcl  8595  fzsplit  8987  fzssp1  9002  fzsuc  9003  fzpred  9004  fzp1ss  9007  fzp1elp1  9009  fztp  9012  fzneuz  9035  fzosplitsnm1  9137  fzofzp1  9155  fzosplitsn  9161  fzostep1  9165  frec2uzuzd  9317  frecuzrdgrrn  9323  frec2uzrdg  9324  frecuzrdgsuc  9330  frecfzen2  9333  fzfig  9335  iseqovex  9348  iseqval  9349  iseqp1  9354  iseqsplit  9367  iseqhomo  9377  iseqz  9378  faclbnd3  9575  bcm1k  9592  clim2iser  10051  clim2iser2  10052  serif0  10065
  Copyright terms: Public domain W3C validator