Theorem nnm1nn0 12572

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 12281	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7421	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12340	. . . . . 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 12533	. 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 1570   ∈ wcel 2145  (class class class)co 7414  0cc0 11127  1c1 11128   − cmin 11468  ℕcn 12260  ℕ₀cn0 12531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470  df-nn 12261  df-n0 12532

This theorem is used by:  elnn0nn  12573  nn0n0n1ge2  12599  nnaddm1cl  12681  fseq1m1p1  13657  elfznelfzo  13832  nn0ennn  14046  expm1t  14157  expgt1  14167  digit1  14304  bcn1  14380  bcm1k  14382  bcn2m1  14391  cshwidxn  14883  isercoll2  15759  iseralt  15775  binomlem  15921  incexc  15929  incexc2  15930  arisum  15952  arisum2  15953  pwdif  15960  mertenslem2  15977  risefallfac  16114  fallfacfwd  16125  0fallfac  16126  bpolydiflem  16143  ruclem12  16332  iddvdsexp  16372  dvdsfac  16419  oexpneg  16438  pwp1fsum  16484  bitsfzolem  16527  bitsf1  16539  phibnd  16865  phiprmpw  16870  prmdiv  16879  oddprm  16905  iserodd  16930  fldivp1  16992  prmpwdvds  16999  4sqlem12  17051  4sqlem19  17058  vdwapid1  17070  vdwlem1  17076  vdwlem3  17078  vdwlem5  17080  vdwlem6  17081  vdwlem9  17084  0ram  17115  ram0  17117  ramub1lem1  17121  ramub1lem2  17122  ramcl  17124  prmonn2  17134  1259lem5  17230  2503lem3  17234  4001lem4  17239  chnrev  18718  gsumwsubmcl  18949  gsumsgrpccat  18952  gsumwmhm  18957  finodsubmsubg  19697  sylow1lem1  19728  efgsrel  19864  efgredlem  19877  srgbinomlem4  20371  freshmansdream  21790  psdpw  22401  chfacfisf  23082  chfacfisfcpmat  23083  cpmadugsumlemF  23104  lebnumii  25197  ovolunlem1  25728  dvexp  26183  dgreq0  26494  plyn0mulidp  26514  plymulidp  26515  dvply1  26517  vieta1lem2  26546  aaliou3lem8  26584  dvtaylp  26609  taylthlem1  26612  pserdvlem2  26667  pserdv2  26669  abelthlem6  26675  logtayl  26900  logtayl2  26902  cxpeq  26997  gamfac  27306  wilthlem1  27307  wilthlem2  27308  wilthlem3  27309  wilth  27310  wilthimp  27311  ftalem1  27312  basellem5  27324  1sgm2ppw  27439  chtublem  27450  perfect1  27467  perfect  27470  bcmono  27516  lgslem1  27536  lgsquadlem1  27619  lgsquad2lem2  27624  m1lgs  27627  selberg2lem  27789  logdivbnd  27795  pntrsumo1  27804  cusgrsize2inds  29916  cusgrrusgr  30044  pthdlem2  30236  crctcshwlkn0lem4  30284  wlkiswwlks2lem1  30340  wlkiswwlksupgr2  30348  clwwlkccatlem  30462  clwlkclwwlklem2a2  30466  clwwlknwwlksn  30511  clwwlkel  30519  clwwlkwwlksb  30527  wwlksubclwwlk  30531  oexpled  33309  1arithidomlem1  33948  1arithidomlem2  33949  1arithidom  33950  esplyind  34088  fibp1  34915  signstfvn  35080  signsvtn0  35081  subfacp1lem6  35767  erdszelem10  35782  erdsze2lem1  35785  erdsze2lem2  35786  cvmliftlem2  35868  bcprod  36320  poimirlem5  38377  poimirlem6  38378  poimirlem7  38379  poimirlem10  38382  poimirlem11  38383  poimirlem13  38385  poimirlem14  38386  poimirlem20  38392  poimirlem21  38393  poimirlem22  38394  poimirlem23  38395  poimirlem25  38397  poimirlem26  38398  poimirlem31  38403  lcmfunnnd  42881  lcmineqlem2  42899  lcmineqlem3  42900  lcmineqlem8  42905  lcmineqlem10  42907  lcmineqlem12  42909  dvrelogpow2b  42937  primrootsunit1  42966  sticksstones12a  43026  sticksstones16  43031  sticksstones22  43037  fltnltalem  43511  irrapxlem1  43666  rmspecsqrtnq  43750  jm2.24nn  43803  jm2.17a  43804  acongeq  43827  jm2.18  43832  jm2.22  43839  jm2.23  43840  jm2.20nn  43841  jm2.27c  43851  bccm1k  45169  binomcxplemwb  45175  binomcxplemnotnn0  45183  dvsinexp  46742  dvxpaek  46771  dvnxpaek  46773  itgsinexplem1  46785  itgsinexp  46786  wallispilem5  46900  stirlinglem5  46909  fourierdlem48  46985  fourierdlem49  46986  fourierdlem52  46989  fourierdlem54  46991  fourierdlem103  47040  fourierdlem104  47041  etransclem1  47066  etransclem4  47069  etransclem8  47073  etransclem10  47075  etransclem14  47079  etransclem15  47080  etransclem17  47082  etransclem18  47083  etransclem19  47084  etransclem20  47085  etransclem21  47086  etransclem22  47087  etransclem23  47088  etransclem24  47089  etransclem27  47092  etransclem28  47093  etransclem32  47097  etransclem35  47100  etransclem37  47102  etransclem38  47103  etransclem41  47106  etransclem44  47109  etransclem45  47110  etransclem46  47111  etransclem47  47112  etransclem48  47113  muldvdsfacgt  48277  muldvdsfacm1  48278  lswn0  48347  fmtnoodd  48439  sqrtpwpw2p  48444  fmtnosqrt  48445  fmtnodvds  48450  fmtnorec3  48454  fmtnorec4  48455  2pwp1prm  48495  lighneallem3  48513  lighneallem4a  48514  lighneallem4  48516  nprmdvdsfacm1lem4  48529  ppivalnnprm  48531  ppivalnnnprmge6  48532  oexpnegALTV  48596  perfectALTV  48642  fpprmod  48646  fppr2odd  48650  fpprwppr  48658  fpprwpprb  48659  bgoldbtbndlem4  48727  bcpascm1  49284  altgsumbcALT  49286  pw2m1lepw2m1  49453  nnpw2even  49462  logbpw2m1  49500  nnpw2blenfzo  49514  nnpw2pmod  49516  nnpw2p  49519  nnolog2flm1  49523  dignn0fr  49534  dig2nn1st  49538  digexp  49540  dignn0flhalflem1  49548