Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > peano2uz | Structured version Visualization version GIF version |
Description: Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
Ref | Expression |
---|---|
peano2uz | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1132 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) | |
2 | peano2z 12024 | . . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) | |
3 | 2 | 3ad2ant2 1130 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ) |
4 | zre 11986 | . . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
5 | zre 11986 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
6 | letrp1 11484 | . . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) | |
7 | 5, 6 | syl3an2 1160 | . . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
8 | 4, 7 | syl3an1 1159 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
9 | 1, 3, 8 | 3jca 1124 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) |
10 | eluz2 12250 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
11 | eluz2 12250 | . 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) | |
12 | 9, 10, 11 | 3imtr4i 294 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 ∈ wcel 2114 class class class wbr 5066 ‘cfv 6355 (class class class)co 7156 ℝcr 10536 1c1 10538 + caddc 10540 ≤ cle 10676 ℤcz 11982 ℤ≥cuz 12244 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-n0 11899 df-z 11983 df-uz 12245 |
This theorem is referenced by: peano2uzs 12303 peano2uzr 12304 uzaddcl 12305 fzsplit 12934 fzssp1 12951 fzsuc 12955 fzpred 12956 fzp1ss 12959 fzp1elp1 12961 fztp 12964 fzneuz 12989 fzosplitsnm1 13113 fzofzp1 13135 fzosplitsn 13146 fzosplitpr 13147 fzostep1 13154 om2uzuzi 13318 uzrdgsuci 13329 fzen2 13338 fzfi 13341 seqsplit 13404 seqf1olem1 13410 seqf1olem2 13411 seqz 13419 faclbnd3 13653 bcm1k 13676 seqcoll 13823 seqcoll2 13824 swrds1 14028 pfxccatpfx2 14099 clim2ser 15011 clim2ser2 15012 serf0 15037 iseraltlem2 15039 iseralt 15041 fsump1 15111 fsump1i 15124 fsumparts 15161 cvgcmp 15171 isum1p 15196 isumsup2 15201 climcndslem1 15204 climcndslem2 15205 climcnds 15206 cvgrat 15239 mertenslem1 15240 clim2prod 15244 clim2div 15245 ntrivcvgfvn0 15255 fprodntriv 15296 fprodp1 15323 fprodabs 15328 binomfallfaclem2 15394 pcfac 16235 gsumsplit1r 17897 gsumprval 17898 telgsumfzslem 19108 telgsumfzs 19109 dvply2g 24874 aaliou3lem2 24932 ppinprm 25729 chtnprm 25731 ppiublem1 25778 chtublem 25787 chtub 25788 bposlem6 25865 pntlemf 26181 ostth2lem2 26210 clwwlkvbij 27892 fzsplit3 30517 esumcvg 31345 sseqf 31650 gsumnunsn 31811 signstfvp 31841 iprodefisumlem 32972 poimirlem1 34908 poimirlem2 34909 poimirlem3 34910 poimirlem4 34911 poimirlem6 34913 poimirlem7 34914 poimirlem8 34915 poimirlem9 34916 poimirlem12 34919 poimirlem13 34920 poimirlem14 34921 poimirlem15 34922 poimirlem16 34923 poimirlem17 34924 poimirlem18 34925 poimirlem19 34926 poimirlem20 34927 poimirlem21 34928 poimirlem22 34929 poimirlem23 34930 poimirlem24 34931 poimirlem26 34933 poimirlem27 34934 poimirlem31 34938 poimirlem32 34939 sdclem2 35032 fdc 35035 mettrifi 35047 bfplem2 35116 rexrabdioph 39411 monotuz 39558 wallispilem1 42370 dirkertrigeqlem2 42404 sge0p1 42716 carageniuncllem1 42823 iccpartres 43598 iccelpart 43613 fmtno4prm 43757 |
Copyright terms: Public domain | W3C validator |