![]() |
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 1134 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) | |
2 | peano2z 12628 | . . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) | |
3 | 2 | 3ad2ant2 1132 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 + 1) ∈ ℤ) |
4 | zre 12587 | . . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
5 | zre 12587 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
6 | letrp1 12083 | . . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) | |
7 | 5, 6 | syl3an2 1162 | . . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
8 | 4, 7 | syl3an1 1161 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ (𝑁 + 1)) |
9 | 1, 3, 8 | 3jca 1126 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) |
10 | eluz2 12853 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
11 | eluz2 12853 | . 2 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑁 + 1))) | |
12 | 9, 10, 11 | 3imtr4i 292 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1085 ∈ wcel 2099 class class class wbr 5143 ‘cfv 6543 (class class class)co 7415 ℝcr 11132 1c1 11134 + caddc 11136 ≤ cle 11274 ℤcz 12583 ℤ≥cuz 12847 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5294 ax-nul 5301 ax-pow 5360 ax-pr 5424 ax-un 7735 ax-cnex 11189 ax-resscn 11190 ax-1cn 11191 ax-icn 11192 ax-addcl 11193 ax-addrcl 11194 ax-mulcl 11195 ax-mulrcl 11196 ax-mulcom 11197 ax-addass 11198 ax-mulass 11199 ax-distr 11200 ax-i2m1 11201 ax-1ne0 11202 ax-1rid 11203 ax-rnegex 11204 ax-rrecex 11205 ax-cnre 11206 ax-pre-lttri 11207 ax-pre-lttrn 11208 ax-pre-ltadd 11209 ax-pre-mulgt0 11210 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-iun 4994 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7371 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7866 df-2nd 7989 df-frecs 8281 df-wrecs 8312 df-recs 8386 df-rdg 8425 df-er 8719 df-en 8959 df-dom 8960 df-sdom 8961 df-pnf 11275 df-mnf 11276 df-xr 11277 df-ltxr 11278 df-le 11279 df-sub 11471 df-neg 11472 df-nn 12238 df-n0 12498 df-z 12584 df-uz 12848 |
This theorem is referenced by: peano2uzs 12911 peano2uzr 12912 uzaddcl 12913 fzsplit 13554 fzssp1 13571 fzsuc 13575 fzpred 13576 fzp1ss 13579 fzp1elp1 13581 fztp 13584 fzneuz 13609 fzosplitsnm1 13734 fzofzp1 13756 fzosplitsn 13767 fzosplitpr 13768 fzostep1 13775 om2uzuzi 13941 uzrdgsuci 13952 fzen2 13961 fzfi 13964 seqsplit 14027 seqf1olem1 14033 seqf1olem2 14034 seqz 14042 faclbnd3 14278 bcm1k 14301 seqcoll 14452 seqcoll2 14453 swrds1 14643 pfxccatpfx2 14714 clim2ser 15628 clim2ser2 15629 serf0 15654 iseraltlem2 15656 iseralt 15658 fsump1 15729 fsump1i 15742 fsumparts 15779 cvgcmp 15789 isum1p 15814 isumsup2 15819 climcndslem1 15822 climcndslem2 15823 climcnds 15824 cvgrat 15856 mertenslem1 15857 clim2prod 15861 clim2div 15862 ntrivcvgfvn0 15872 fprodntriv 15913 fprodp1 15940 fprodabs 15945 binomfallfaclem2 16011 pcfac 16862 gsumsplit1r 18641 gsumprval 18642 telgsumfzslem 19937 telgsumfzs 19938 dvply2g 26213 dvply2gOLD 26214 aaliou3lem2 26272 ppinprm 27078 chtnprm 27080 ppiublem1 27129 chtublem 27138 chtub 27139 bposlem6 27216 pntlemf 27532 ostth2lem2 27561 clwwlkvbij 29917 fzsplit3 32557 esumcvg 33700 sseqf 34007 gsumnunsn 34168 signstfvp 34198 iprodefisumlem 35329 poimirlem1 37089 poimirlem2 37090 poimirlem3 37091 poimirlem4 37092 poimirlem6 37094 poimirlem7 37095 poimirlem8 37096 poimirlem9 37097 poimirlem12 37100 poimirlem13 37101 poimirlem14 37102 poimirlem15 37103 poimirlem16 37104 poimirlem17 37105 poimirlem18 37106 poimirlem19 37107 poimirlem20 37108 poimirlem21 37109 poimirlem22 37110 poimirlem23 37111 poimirlem24 37112 poimirlem26 37114 poimirlem27 37115 poimirlem31 37119 poimirlem32 37120 sdclem2 37210 fdc 37213 mettrifi 37225 bfplem2 37291 rexrabdioph 42205 monotuz 42353 wallispilem1 45444 dirkertrigeqlem2 45478 sge0p1 45793 carageniuncllem1 45900 iccpartres 46749 iccelpart 46764 fmtno4prm 46906 |
Copyright terms: Public domain | W3C validator |