![]() |
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 1116 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) | |
2 | peano2z 11830 | . . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) | |
3 | 2 | 3ad2ant2 1114 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ) |
4 | zre 11791 | . . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
5 | zre 11791 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
6 | letrp1 11279 | . . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) | |
7 | 5, 6 | syl3an2 1144 | . . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
8 | 4, 7 | syl3an1 1143 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
9 | 1, 3, 8 | 3jca 1108 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) |
10 | eluz2 12058 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
11 | eluz2 12058 | . 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) | |
12 | 9, 10, 11 | 3imtr4i 284 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 ∈ wcel 2050 class class class wbr 4923 ‘cfv 6182 (class class class)co 6970 ℝcr 10328 1c1 10330 + caddc 10332 ≤ cle 10469 ℤcz 11787 ℤ≥cuz 12052 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-er 8083 df-en 8301 df-dom 8302 df-sdom 8303 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-nn 11434 df-n0 11702 df-z 11788 df-uz 12053 |
This theorem is referenced by: peano2uzs 12110 peano2uzr 12111 uzaddcl 12112 fzsplit 12743 fzssp1 12760 fzsuc 12764 fzpred 12765 fzp1ss 12768 fzp1elp1 12770 fztp 12773 fzneuz 12798 fzosplitsnm1 12921 fzofzp1 12943 fzosplitsn 12954 fzosplitpr 12955 fzostep1 12962 om2uzuzi 13126 uzrdgsuci 13137 fzen2 13146 fzfi 13149 seqsplit 13212 seqf1olem1 13218 seqf1olem2 13219 seqz 13227 faclbnd3 13461 bcm1k 13484 seqcoll 13629 seqcoll2 13630 swrds1 13838 pfxccatpfx2 13935 clim2ser 14866 clim2ser2 14867 serf0 14892 iseraltlem2 14894 iseralt 14896 fsump1 14965 fsump1i 14978 fsumparts 15015 cvgcmp 15025 isum1p 15050 isumsup2 15055 climcndslem1 15058 climcndslem2 15059 climcnds 15060 cvgrat 15093 mertenslem1 15094 clim2prod 15098 clim2div 15099 ntrivcvgfvn0 15109 fprodntriv 15150 fprodp1 15177 fprodabs 15182 binomfallfaclem2 15248 pcfac 16085 gsumprval 17743 telgsumfzslem 18852 telgsumfzs 18853 dvply2g 24571 aaliou3lem2 24629 ppinprm 25425 chtnprm 25427 ppiublem1 25474 chtublem 25483 chtub 25484 bposlem6 25561 pntlemf 25877 ostth2lem2 25906 clwwlkvbij 27635 clwwlkvbijOLD 27636 fzsplit3 30267 esumcvg 30989 sseqf 31296 gsumnunsn 31457 signstfvp 31488 iprodefisumlem 32492 poimirlem1 34334 poimirlem2 34335 poimirlem3 34336 poimirlem4 34337 poimirlem6 34339 poimirlem7 34340 poimirlem8 34341 poimirlem9 34342 poimirlem12 34345 poimirlem13 34346 poimirlem14 34347 poimirlem15 34348 poimirlem16 34349 poimirlem17 34350 poimirlem18 34351 poimirlem19 34352 poimirlem20 34353 poimirlem21 34354 poimirlem22 34355 poimirlem23 34356 poimirlem24 34357 poimirlem26 34359 poimirlem27 34360 poimirlem31 34364 poimirlem32 34365 sdclem2 34459 fdc 34462 mettrifi 34474 bfplem2 34543 rexrabdioph 38787 monotuz 38934 wallispilem1 41781 dirkertrigeqlem2 41815 sge0p1 42127 carageniuncllem1 42234 iccpartres 42950 iccelpart 42965 fmtno4prm 43105 |
Copyright terms: Public domain | W3C validator |