Theorem nnm1nn0 12204

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 11924	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7262	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 11975	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2795	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 906	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 867	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12165	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 233	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  0cc0 10802  1c1 10803   − cmin 11135  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137  df-nn 11904  df-n0 12164

This theorem is referenced by:  elnn0nn  12205  nn0n0n1ge2  12230  nnaddm1cl  12307  fseq1m1p1  13260  elfznelfzo  13420  nn0ennn  13627  expm1t  13739  expgt1  13749  digit1  13880  bcn1  13955  bcm1k  13957  bcn2m1  13966  cshwidxn  14450  isercoll2  15308  iseralt  15324  binomlem  15469  incexc  15477  incexc2  15478  arisum  15500  arisum2  15501  pwdif  15508  mertenslem2  15525  risefallfac  15662  fallfacfwd  15674  0fallfac  15675  bpolydiflem  15692  ruclem12  15878  iddvdsexp  15917  dvdsfac  15963  oexpneg  15982  pwp1fsum  16028  bitsfzolem  16069  bitsf1  16081  phibnd  16400  phiprmpw  16405  prmdiv  16414  oddprm  16439  iserodd  16464  fldivp1  16526  prmpwdvds  16533  4sqlem12  16585  4sqlem19  16592  vdwapid1  16604  vdwlem1  16610  vdwlem3  16612  vdwlem5  16614  vdwlem6  16615  vdwlem9  16618  0ram  16649  ram0  16651  ramub1lem1  16655  ramub1lem2  16656  ramcl  16658  prmonn2  16668  1259lem5  16764  2503lem3  16768  4001lem4  16773  gsumwsubmcl  18390  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  sylow1lem1  19118  efgsrel  19255  efgredlem  19268  srgbinomlem4  19694  chfacfisf  21911  chfacfisfcpmat  21912  cpmadugsumlemF  21933  lebnumii  24035  ovolunlem1  24566  dvexp  25022  dgreq0  25331  dvply1  25349  vieta1lem2  25376  aaliou3lem8  25410  dvtaylp  25434  taylthlem1  25437  pserdvlem2  25492  pserdv2  25494  abelthlem6  25500  logtayl  25720  logtayl2  25722  cxpeq  25815  gamfac  26121  wilthlem1  26122  wilthlem2  26123  wilthlem3  26124  wilth  26125  wilthimp  26126  ftalem1  26127  basellem5  26139  1sgm2ppw  26253  chtublem  26264  perfect1  26281  perfect  26284  bcmono  26330  lgslem1  26350  lgsquadlem1  26433  lgsquad2lem2  26438  m1lgs  26441  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  cusgrsize2inds  27723  cusgrrusgr  27851  pthdlem2  28037  crctcshwlkn0lem4  28079  wlkiswwlks2lem1  28135  wlkiswwlksupgr2  28143  clwwlkccatlem  28254  clwlkclwwlklem2a2  28258  clwwlknwwlksn  28303  clwwlkel  28311  clwwlkwwlksb  28319  wwlksubclwwlk  28323  freshmansdream  31386  fibp1  32268  plymulx0  32426  plymulx  32427  signstfvn  32448  signsvtn0  32449  subfacp1lem6  33047  erdszelem10  33062  erdsze2lem1  33065  erdsze2lem2  33066  cvmliftlem2  33148  bcprod  33610  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem13  35717  poimirlem14  35718  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem25  35729  poimirlem26  35730  poimirlem31  35735  lcmfunnnd  39948  lcmineqlem2  39966  lcmineqlem3  39967  lcmineqlem8  39972  lcmineqlem10  39974  lcmineqlem12  39976  dvrelogpow2b  40004  sticksstones12a  40041  sticksstones16  40046  sticksstones22  40052  fltnltalem  40415  irrapxlem1  40560  rmspecsqrtnq  40644  jm2.24nn  40697  jm2.17a  40698  acongeq  40721  jm2.18  40726  jm2.22  40733  jm2.23  40734  jm2.20nn  40735  jm2.27c  40745  bccm1k  41849  binomcxplemwb  41855  binomcxplemnotnn0  41863  dvsinexp  43342  dvxpaek  43371  dvnxpaek  43373  itgsinexplem1  43385  itgsinexp  43386  wallispilem5  43500  stirlinglem5  43509  fourierdlem48  43585  fourierdlem49  43586  fourierdlem52  43589  fourierdlem54  43591  fourierdlem103  43640  fourierdlem104  43641  etransclem1  43666  etransclem4  43669  etransclem8  43673  etransclem10  43675  etransclem14  43679  etransclem15  43680  etransclem17  43682  etransclem18  43683  etransclem19  43684  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem23  43688  etransclem24  43689  etransclem27  43692  etransclem28  43693  etransclem32  43697  etransclem35  43700  etransclem37  43702  etransclem38  43703  etransclem41  43706  etransclem44  43709  etransclem45  43710  etransclem46  43711  etransclem47  43712  etransclem48  43713  lswn0  44784  fmtnoodd  44873  sqrtpwpw2p  44878  fmtnosqrt  44879  fmtnodvds  44884  fmtnorec3  44888  fmtnorec4  44889  2pwp1prm  44929  lighneallem3  44947  lighneallem4a  44948  lighneallem4  44950  oexpnegALTV  45017  perfectALTV  45063  fpprmod  45067  fppr2odd  45071  fpprwppr  45079  fpprwpprb  45080  bgoldbtbndlem4  45148  bcpascm1  45575  altgsumbcALT  45577  pw2m1lepw2m1  45749  nnpw2even  45763  logbpw2m1  45801  nnpw2blenfzo  45815  nnpw2pmod  45817  nnpw2p  45820  nnolog2flm1  45824  dignn0fr  45835  dig2nn1st  45839  digexp  45841  dignn0flhalflem1  45849