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

Theorem nnm1nn0 12324
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 12044 . . . 4 (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2 oveq1 7314 . . . . . 6 (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3 1m1e0 12095 . . . . . 6 (1 − 1) = 0
42, 3eqtrdi 2792 . . . . 5 (𝑁 = 1 → (𝑁 − 1) = 0)
54orim1i 908 . . . 4 ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
61, 5syl 17 . . 3 (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
76orcomd 869 . 2 (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8 elnn0 12285 . 2 ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
97, 8sylibr 233 1 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845   = wceq 1539  wcel 2104  (class class class)co 7307  0cc0 10921  1c1 10922  cmin 11255  cn 12023  0cn0 12283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10978  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-addrcl 10982  ax-mulcl 10983  ax-mulrcl 10984  ax-mulcom 10985  ax-addass 10986  ax-mulass 10987  ax-distr 10988  ax-i2m1 10989  ax-1ne0 10990  ax-1rid 10991  ax-rnegex 10992  ax-rrecex 10993  ax-cnre 10994  ax-pre-lttri 10995  ax-pre-lttrn 10996  ax-pre-ltadd 10997
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3332  df-rab 3333  df-v 3439  df-sbc 3722  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 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11061  df-mnf 11062  df-ltxr 11064  df-sub 11257  df-nn 12024  df-n0 12284
This theorem is referenced by:  elnn0nn  12325  nn0n0n1ge2  12350  nnaddm1cl  12427  fseq1m1p1  13381  elfznelfzo  13542  nn0ennn  13749  expm1t  13861  expgt1  13871  digit1  14002  bcn1  14077  bcm1k  14079  bcn2m1  14088  cshwidxn  14571  isercoll2  15429  iseralt  15445  binomlem  15590  incexc  15598  incexc2  15599  arisum  15621  arisum2  15622  pwdif  15629  mertenslem2  15646  risefallfac  15783  fallfacfwd  15795  0fallfac  15796  bpolydiflem  15813  ruclem12  15999  iddvdsexp  16038  dvdsfac  16084  oexpneg  16103  pwp1fsum  16149  bitsfzolem  16190  bitsf1  16202  phibnd  16521  phiprmpw  16526  prmdiv  16535  oddprm  16560  iserodd  16585  fldivp1  16647  prmpwdvds  16654  4sqlem12  16706  4sqlem19  16713  vdwapid1  16725  vdwlem1  16731  vdwlem3  16733  vdwlem5  16735  vdwlem6  16736  vdwlem9  16739  0ram  16770  ram0  16772  ramub1lem1  16776  ramub1lem2  16777  ramcl  16779  prmonn2  16789  1259lem5  16885  2503lem3  16889  4001lem4  16894  gsumwsubmcl  18524  gsumsgrpccat  18527  gsumccatOLD  18528  gsumwmhm  18533  sylow1lem1  19252  efgsrel  19389  efgredlem  19402  srgbinomlem4  19828  chfacfisf  22052  chfacfisfcpmat  22053  cpmadugsumlemF  22074  lebnumii  24178  ovolunlem1  24710  dvexp  25166  dgreq0  25475  dvply1  25493  vieta1lem2  25520  aaliou3lem8  25554  dvtaylp  25578  taylthlem1  25581  pserdvlem2  25636  pserdv2  25638  abelthlem6  25644  logtayl  25864  logtayl2  25866  cxpeq  25959  gamfac  26265  wilthlem1  26266  wilthlem2  26267  wilthlem3  26268  wilth  26269  wilthimp  26270  ftalem1  26271  basellem5  26283  1sgm2ppw  26397  chtublem  26408  perfect1  26425  perfect  26428  bcmono  26474  lgslem1  26494  lgsquadlem1  26577  lgsquad2lem2  26582  m1lgs  26585  selberg2lem  26747  logdivbnd  26753  pntrsumo1  26762  cusgrsize2inds  27869  cusgrrusgr  27997  pthdlem2  28185  crctcshwlkn0lem4  28227  wlkiswwlks2lem1  28283  wlkiswwlksupgr2  28291  clwwlkccatlem  28402  clwlkclwwlklem2a2  28406  clwwlknwwlksn  28451  clwwlkel  28459  clwwlkwwlksb  28467  wwlksubclwwlk  28471  freshmansdream  31533  fibp1  32417  plymulx0  32575  plymulx  32576  signstfvn  32597  signsvtn0  32598  subfacp1lem6  33196  erdszelem10  33211  erdsze2lem1  33214  erdsze2lem2  33215  cvmliftlem2  33297  bcprod  33753  poimirlem5  35830  poimirlem6  35831  poimirlem7  35832  poimirlem10  35835  poimirlem11  35836  poimirlem13  35838  poimirlem14  35839  poimirlem20  35845  poimirlem21  35846  poimirlem22  35847  poimirlem23  35848  poimirlem25  35850  poimirlem26  35851  poimirlem31  35856  lcmfunnnd  40220  lcmineqlem2  40238  lcmineqlem3  40239  lcmineqlem8  40244  lcmineqlem10  40246  lcmineqlem12  40248  dvrelogpow2b  40276  sticksstones12a  40313  sticksstones16  40318  sticksstones22  40324  fltnltalem  40694  irrapxlem1  40839  rmspecsqrtnq  40923  jm2.24nn  40977  jm2.17a  40978  acongeq  41001  jm2.18  41006  jm2.22  41013  jm2.23  41014  jm2.20nn  41015  jm2.27c  41025  bccm1k  42173  binomcxplemwb  42179  binomcxplemnotnn0  42187  dvsinexp  43681  dvxpaek  43710  dvnxpaek  43712  itgsinexplem1  43724  itgsinexp  43725  wallispilem5  43839  stirlinglem5  43848  fourierdlem48  43924  fourierdlem49  43925  fourierdlem52  43928  fourierdlem54  43930  fourierdlem103  43979  fourierdlem104  43980  etransclem1  44005  etransclem4  44008  etransclem8  44012  etransclem10  44014  etransclem14  44018  etransclem15  44019  etransclem17  44021  etransclem18  44022  etransclem19  44023  etransclem20  44024  etransclem21  44025  etransclem22  44026  etransclem23  44027  etransclem24  44028  etransclem27  44031  etransclem28  44032  etransclem32  44036  etransclem35  44039  etransclem37  44041  etransclem38  44042  etransclem41  44045  etransclem44  44048  etransclem45  44049  etransclem46  44050  etransclem47  44051  etransclem48  44052  lswn0  45140  fmtnoodd  45229  sqrtpwpw2p  45234  fmtnosqrt  45235  fmtnodvds  45240  fmtnorec3  45244  fmtnorec4  45245  2pwp1prm  45285  lighneallem3  45303  lighneallem4a  45304  lighneallem4  45306  oexpnegALTV  45373  perfectALTV  45419  fpprmod  45423  fppr2odd  45427  fpprwppr  45435  fpprwpprb  45436  bgoldbtbndlem4  45504  bcpascm1  45931  altgsumbcALT  45933  pw2m1lepw2m1  46105  nnpw2even  46119  logbpw2m1  46157  nnpw2blenfzo  46171  nnpw2pmod  46173  nnpw2p  46176  nnolog2flm1  46180  dignn0fr  46191  dig2nn1st  46195  digexp  46197  dignn0flhalflem1  46205
  Copyright terms: Public domain W3C validator