Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uz2m1nn | Structured version Visualization version GIF version |
Description: One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.) |
Ref | Expression |
---|---|
uz2m1nn | ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2b1 12650 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁)) | |
2 | 1z 12342 | . . . 4 ⊢ 1 ∈ ℤ | |
3 | znnsub 12358 | . . . 4 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 < 𝑁 ↔ (𝑁 − 1) ∈ ℕ)) | |
4 | 2, 3 | mpan 687 | . . 3 ⊢ (𝑁 ∈ ℤ → (1 < 𝑁 ↔ (𝑁 − 1) ∈ ℕ)) |
5 | 4 | biimpa 477 | . 2 ⊢ ((𝑁 ∈ ℤ ∧ 1 < 𝑁) → (𝑁 − 1) ∈ ℕ) |
6 | 1, 5 | sylbi 216 | 1 ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2110 class class class wbr 5079 ‘cfv 6431 (class class class)co 7269 1c1 10865 < clt 11002 − cmin 11197 ℕcn 11965 2c2 12020 ℤcz 12311 ℤ≥cuz 12573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7580 ax-cnex 10920 ax-resscn 10921 ax-1cn 10922 ax-icn 10923 ax-addcl 10924 ax-addrcl 10925 ax-mulcl 10926 ax-mulrcl 10927 ax-mulcom 10928 ax-addass 10929 ax-mulass 10930 ax-distr 10931 ax-i2m1 10932 ax-1ne0 10933 ax-1rid 10934 ax-rnegex 10935 ax-rrecex 10936 ax-cnre 10937 ax-pre-lttri 10938 ax-pre-lttrn 10939 ax-pre-ltadd 10940 ax-pre-mulgt0 10941 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4846 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6200 df-ord 6267 df-on 6268 df-lim 6269 df-suc 6270 df-iota 6389 df-fun 6433 df-fn 6434 df-f 6435 df-f1 6436 df-fo 6437 df-f1o 6438 df-fv 6439 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-om 7702 df-2nd 7819 df-frecs 8082 df-wrecs 8113 df-recs 8187 df-rdg 8226 df-er 8473 df-en 8709 df-dom 8710 df-sdom 8711 df-pnf 11004 df-mnf 11005 df-xr 11006 df-ltxr 11007 df-le 11008 df-sub 11199 df-neg 11200 df-nn 11966 df-2 12028 df-n0 12226 df-z 12312 df-uz 12574 |
This theorem is referenced by: nn0ge2m1nnALT 12673 bernneq3 13936 pfxtrcfv0 14397 climcndslem1 15551 exprmfct 16399 oddprm 16501 pockthg 16597 vdwlem5 16676 vdwlem8 16679 efgs1b 19332 efgredlema 19336 wilthlem3 26209 ppiprm 26290 ppinprm 26291 chtprm 26292 chtnprm 26293 lgsval2lem 26445 lgsqrlem2 26485 lgseisenlem1 26513 lgseisenlem3 26515 lgsquadlem3 26520 rplogsumlem1 26622 rplogsumlem2 26623 rpvmasumlem 26625 clwwisshclwwslemlem 28365 umgr2cwwk2dif 28416 psgnfzto1stlem 31355 ballotlemic 32461 ballotlem1c 32462 signstfveq0 32544 fltnltalem 40488 fltnlta 40489 jm3.1lem1 40828 jm3.1lem2 40829 trclfvdecomr 41298 itgsinexp 43459 stirlinglem12 43589 fourierdlem54 43664 fourierdlem102 43712 fourierdlem114 43724 blennngt2o2 45899 |
Copyright terms: Public domain | W3C validator |