Theorem nnm1nn0 12651

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

Step	Hyp	Ref	Expression
1		nn1m1nn 12360	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7428	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12419	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2811	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 923	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 18	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 885	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12612	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144  (class class class)co 7421  0cc0 11204  1c1 11205   − cmin 11545  ℕcn 12339  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-ltxr 11352  df-sub 11547  df-nn 12340  df-n0 12611

This theorem is used by:  elnn0nn  12652  nn0n0n1ge2  12678  nnaddm1cl  12760  fseq1m1p1  13737  elfznelfzo  13912  nn0ennn  14126  expm1t  14237  expgt1  14247  digit1  14385  bcn1  14461  bcm1k  14463  bcn2m1  14472  cshwidxn  14965  isercoll2  15842  iseralt  15858  binomlem  16004  incexc  16012  incexc2  16013  arisum  16035  arisum2  16036  pwdif  16043  mertenslem2  16060  risefallfac  16197  fallfacfwd  16208  0fallfac  16209  bpolydiflem  16226  ruclem12  16415  iddvdsexp  16455  dvdsfac  16502  oexpneg  16521  pwp1fsum  16567  bitsfzolem  16610  bitsf1  16622  phibnd  16954  phiprmpw  16959  prmdiv  16968  oddprm  16994  iserodd  17019  fldivp1  17081  prmpwdvds  17088  4sqlem12  17140  4sqlem19  17147  vdwapid1  17159  vdwlem1  17165  vdwlem3  17167  vdwlem5  17169  vdwlem6  17170  vdwlem9  17173  0ram  17204  ram0  17206  ramub1lem1  17210  ramub1lem2  17211  ramcl  17213  prmonn2  17223  1259lem5  17319  2503lem3  17323  4001lem4  17328  chnrev  18807  gsumwsubmcl  19039  gsumsgrpccat  19042  gsumwmhm  19047  finodsubmsubg  19787  sylow1lem1  19818  efgsrel  19954  efgredlem  19967  srgbinomlem4  20461  freshmansdream  21886  psdpw  22497  chfacfisf  23178  chfacfisfcpmat  23179  cpmadugsumlemF  23200  lebnumii  25293  ovolunlem1  25824  dvexp  26279  dgreq0  26590  plyn0mulidp  26608  plymulidp  26609  dvply1  26611  vieta1lem2  26640  aaliou3lem8  26678  dvtaylp  26703  taylthlem1  26706  pserdvlem2  26761  pserdv2  26763  abelthlem6  26769  logtayl  26994  logtayl2  26996  cxpeq  27091  gamfac  27400  wilthlem1  27401  wilthlem2  27402  wilthlem3  27403  wilth  27404  wilthimp  27405  ftalem1  27406  basellem5  27418  1sgm2ppw  27533  chtublem  27544  perfect1  27561  perfect  27564  bcmono  27610  lgslem1  27630  lgsquadlem1  27713  lgsquad2lem2  27718  m1lgs  27721  selberg2lem  27883  logdivbnd  27889  pntrsumo1  27898  cusgrsize2inds  30040  cusgrrusgr  30168  pthdlem2  30360  crctcshwlkn0lem4  30408  wlkiswwlks2lem1  30464  wlkiswwlksupgr2  30472  clwwlkccatlem  30586  clwlkclwwlklem2a2  30590  clwwlknwwlksn  30635  clwwlkel  30643  clwwlkwwlksb  30651  wwlksubclwwlk  30655  oexpled  33474  1arithidomlem1  34114  1arithidomlem2  34115  1arithidom  34116  esplyind  34254  fibp1  35080  signstfvn  35245  signsvtn0  35246  subfacp1lem6  36037  erdszelem10  36052  erdsze2lem1  36055  erdsze2lem2  36056  cvmliftlem2  36138  bcprod  36596  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  poimirlem13  38645  poimirlem14  38646  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem23  38655  poimirlem25  38657  poimirlem26  38658  poimirlem31  38663  lcmfunnnd  43156  lcmineqlem2  43174  lcmineqlem3  43175  lcmineqlem8  43180  lcmineqlem10  43182  lcmineqlem12  43184  dvrelogpow2b  43212  primrootsunit1  43241  sticksstones12a  43301  sticksstones16  43306  sticksstones22  43312  fltnltalem  43767  irrapxlem1  43923  rmspecsqrtnq  44007  jm2.24nn  44060  jm2.17a  44061  acongeq  44084  jm2.18  44089  jm2.22  44096  jm2.23  44097  jm2.20nn  44098  jm2.27c  44108  bccm1k  45420  binomcxplemwb  45426  binomcxplemnotnn0  45434  dvsinexp  47015  dvxpaek  47044  dvnxpaek  47046  itgsinexplem1  47058  itgsinexp  47059  wallispilem5  47173  stirlinglem5  47182  fourierdlem48  47258  fourierdlem49  47259  fourierdlem52  47262  fourierdlem54  47264  fourierdlem103  47313  fourierdlem104  47314  etransclem1  47339  etransclem4  47342  etransclem8  47346  etransclem10  47348  etransclem14  47352  etransclem15  47353  etransclem17  47355  etransclem18  47356  etransclem19  47357  etransclem20  47358  etransclem21  47359  etransclem22  47360  etransclem23  47361  etransclem24  47362  etransclem27  47365  etransclem28  47366  etransclem32  47370  etransclem35  47373  etransclem37  47375  etransclem38  47376  etransclem41  47379  etransclem44  47382  etransclem45  47383  etransclem46  47384  etransclem47  47385  etransclem48  47386  muldvdsfacgt  48550  muldvdsfacm1  48551  lswn0  48620  fmtnoodd  48712  sqrtpwpw2p  48717  fmtnosqrt  48718  fmtnodvds  48723  fmtnorec3  48727  fmtnorec4  48728  2pwp1prm  48768  lighneallem3  48786  lighneallem4a  48787  lighneallem4  48789  nprmdvdsfacm1lem4  48802  ppivalnnprm  48804  ppivalnnnprmge6  48805  oexpnegALTV  48869  perfectALTV  48915  fpprmod  48919  fppr2odd  48923  fpprwppr  48931  fpprwpprb  48932  bgoldbtbndlem4  49000  bcpascm1  49557  altgsumbcALT  49559  pw2m1lepw2m1  49726  nnpw2even  49735  logbpw2m1  49773  nnpw2blenfzo  49787  nnpw2pmod  49789  nnpw2p  49792  nnolog2flm1  49796  dignn0fr  49807  dig2nn1st  49811  digexp  49813  dignn0flhalflem1  49821