MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnm1nn0 Structured version   Visualization version   GIF version

Theorem nnm1nn0 11930
Description: A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
nnm1nn0 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Proof of Theorem nnm1nn0
StepHypRef Expression
1 nn1m1nn 11650 . . . 4 (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2 oveq1 7146 . . . . . 6 (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3 1m1e0 11701 . . . . . 6 (1 − 1) = 0
42, 3eqtrdi 2852 . . . . 5 (𝑁 = 1 → (𝑁 − 1) = 0)
54orim1i 907 . . . 4 ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
61, 5syl 17 . . 3 (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
76orcomd 868 . 2 (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8 elnn0 11891 . 2 ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
97, 8sylibr 237 1 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 844   = wceq 1538  wcel 2112  (class class class)co 7139  0cc0 10530  1c1 10531  cmin 10863  cn 11629  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-ltxr 10673  df-sub 10865  df-nn 11630  df-n0 11890
This theorem is referenced by:  elnn0nn  11931  nn0n0n1ge2  11954  nnaddm1cl  12031  fseq1m1p1  12981  elfznelfzo  13141  nn0ennn  13346  expm1t  13457  expgt1  13467  digit1  13598  bcn1  13673  bcm1k  13675  bcn2m1  13684  cshwidxn  14166  isercoll2  15020  iseralt  15036  binomlem  15179  incexc  15187  incexc2  15188  arisum  15210  arisum2  15211  pwdif  15218  mertenslem2  15236  risefallfac  15373  fallfacfwd  15385  0fallfac  15386  bpolydiflem  15403  ruclem12  15589  iddvdsexp  15628  dvdsfac  15671  oexpneg  15689  pwp1fsum  15735  bitsfzolem  15776  bitsf1  15788  phibnd  16101  phiprmpw  16106  prmdiv  16115  oddprm  16140  iserodd  16165  fldivp1  16226  prmpwdvds  16233  4sqlem12  16285  4sqlem19  16292  vdwapid1  16304  vdwlem1  16310  vdwlem3  16312  vdwlem5  16314  vdwlem6  16315  vdwlem9  16318  0ram  16349  ram0  16351  ramub1lem1  16355  ramub1lem2  16356  ramcl  16358  prmonn2  16368  1259lem5  16463  2503lem3  16467  4001lem4  16472  gsumwsubmcl  17996  gsumsgrpccat  17999  gsumccatOLD  18000  gsumwmhm  18005  sylow1lem1  18718  efgsrel  18855  efgredlem  18868  srgbinomlem4  19289  chfacfisf  21462  chfacfisfcpmat  21463  cpmadugsumlemF  21484  lebnumii  23574  ovolunlem1  24104  dvexp  24559  dgreq0  24865  dvply1  24883  vieta1lem2  24910  aaliou3lem8  24944  dvtaylp  24968  taylthlem1  24971  pserdvlem2  25026  pserdv2  25028  abelthlem6  25034  logtayl  25254  logtayl2  25256  cxpeq  25349  gamfac  25655  wilthlem1  25656  wilthlem2  25657  wilthlem3  25658  wilth  25659  wilthimp  25660  ftalem1  25661  basellem5  25673  1sgm2ppw  25787  chtublem  25798  perfect1  25815  perfect  25818  bcmono  25864  lgslem1  25884  lgsquadlem1  25967  lgsquad2lem2  25972  m1lgs  25975  selberg2lem  26137  logdivbnd  26143  pntrsumo1  26152  cusgrsize2inds  27246  cusgrrusgr  27374  pthdlem2  27560  crctcshwlkn0lem4  27602  wlkiswwlks2lem1  27658  wlkiswwlksupgr2  27666  clwwlkccatlem  27777  clwlkclwwlklem2a2  27781  clwwlknwwlksn  27826  clwwlkel  27834  clwwlkwwlksb  27842  wwlksubclwwlk  27846  freshmansdream  30912  fibp1  31767  plymulx0  31925  plymulx  31926  signstfvn  31947  signsvtn0  31948  subfacp1lem6  32540  erdszelem10  32555  erdsze2lem1  32558  erdsze2lem2  32559  cvmliftlem2  32641  bcprod  33078  poimirlem5  35055  poimirlem6  35056  poimirlem7  35057  poimirlem10  35060  poimirlem11  35061  poimirlem13  35063  poimirlem14  35064  poimirlem20  35070  poimirlem21  35071  poimirlem22  35072  poimirlem23  35073  poimirlem25  35075  poimirlem26  35076  poimirlem31  35081  lcmfunnnd  39293  lcmineqlem2  39311  lcmineqlem3  39312  lcmineqlem8  39317  lcmineqlem10  39319  lcmineqlem12  39321  fltnltalem  39605  irrapxlem1  39750  rmspecsqrtnq  39834  jm2.24nn  39887  jm2.17a  39888  acongeq  39911  jm2.18  39916  jm2.22  39923  jm2.23  39924  jm2.20nn  39925  jm2.27c  39935  bccm1k  41033  binomcxplemwb  41039  binomcxplemnotnn0  41047  dvsinexp  42540  dvxpaek  42569  dvnxpaek  42571  itgsinexplem1  42583  itgsinexp  42584  wallispilem5  42698  stirlinglem5  42707  fourierdlem48  42783  fourierdlem49  42784  fourierdlem52  42787  fourierdlem54  42789  fourierdlem103  42838  fourierdlem104  42839  etransclem1  42864  etransclem4  42867  etransclem8  42871  etransclem10  42873  etransclem14  42877  etransclem15  42878  etransclem17  42880  etransclem18  42881  etransclem19  42882  etransclem20  42883  etransclem21  42884  etransclem22  42885  etransclem23  42886  etransclem24  42887  etransclem27  42890  etransclem28  42891  etransclem32  42895  etransclem35  42898  etransclem37  42900  etransclem38  42901  etransclem41  42904  etransclem44  42907  etransclem45  42908  etransclem46  42909  etransclem47  42910  etransclem48  42911  lswn0  43948  fmtnoodd  44037  sqrtpwpw2p  44042  fmtnosqrt  44043  fmtnodvds  44048  fmtnorec3  44052  fmtnorec4  44053  2pwp1prm  44093  lighneallem3  44112  lighneallem4a  44113  lighneallem4  44115  oexpnegALTV  44182  perfectALTV  44228  fpprmod  44232  fppr2odd  44236  fpprwppr  44244  fpprwpprb  44245  bgoldbtbndlem4  44313  bcpascm1  44740  altgsumbcALT  44742  pw2m1lepw2m1  44916  nnpw2even  44930  logbpw2m1  44968  nnpw2blenfzo  44982  nnpw2pmod  44984  nnpw2p  44987  nnolog2flm1  44991  dignn0fr  45002  dig2nn1st  45006  digexp  45008  dignn0flhalflem1  45016
  Copyright terms: Public domain W3C validator