Theorem nnm1nn0 12517

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 12237	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7418	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12288	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2786	. . . . 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 12478	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 233	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  0cc0 11112  1c1 11113   − cmin 11448  ℕcn 12216  ℕ₀cn0 12476

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 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450  df-nn 12217  df-n0 12477

This theorem is referenced by:  elnn0nn  12518  nn0n0n1ge2  12543  nnaddm1cl  12623  fseq1m1p1  13580  elfznelfzo  13741  nn0ennn  13948  expm1t  14060  expgt1  14070  digit1  14204  bcn1  14277  bcm1k  14279  bcn2m1  14288  cshwidxn  14763  isercoll2  15619  iseralt  15635  binomlem  15779  incexc  15787  incexc2  15788  arisum  15810  arisum2  15811  pwdif  15818  mertenslem2  15835  risefallfac  15972  fallfacfwd  15984  0fallfac  15985  bpolydiflem  16002  ruclem12  16188  iddvdsexp  16227  dvdsfac  16273  oexpneg  16292  pwp1fsum  16338  bitsfzolem  16379  bitsf1  16391  phibnd  16708  phiprmpw  16713  prmdiv  16722  oddprm  16747  iserodd  16772  fldivp1  16834  prmpwdvds  16841  4sqlem12  16893  4sqlem19  16900  vdwapid1  16912  vdwlem1  16918  vdwlem3  16920  vdwlem5  16922  vdwlem6  16923  vdwlem9  16926  0ram  16957  ram0  16959  ramub1lem1  16963  ramub1lem2  16964  ramcl  16966  prmonn2  16976  1259lem5  17072  2503lem3  17076  4001lem4  17081  gsumwsubmcl  18754  gsumsgrpccat  18757  gsumwmhm  18762  finodsubmsubg  19476  sylow1lem1  19507  efgsrel  19643  efgredlem  19656  srgbinomlem4  20123  chfacfisf  22576  chfacfisfcpmat  22577  cpmadugsumlemF  22598  lebnumii  24712  ovolunlem1  25246  dvexp  25705  dgreq0  26015  dvply1  26033  vieta1lem2  26060  aaliou3lem8  26094  dvtaylp  26118  taylthlem1  26121  pserdvlem2  26176  pserdv2  26178  abelthlem6  26184  logtayl  26404  logtayl2  26406  cxpeq  26501  gamfac  26807  wilthlem1  26808  wilthlem2  26809  wilthlem3  26810  wilth  26811  wilthimp  26812  ftalem1  26813  basellem5  26825  1sgm2ppw  26939  chtublem  26950  perfect1  26967  perfect  26970  bcmono  27016  lgslem1  27036  lgsquadlem1  27119  lgsquad2lem2  27124  m1lgs  27127  selberg2lem  27289  logdivbnd  27295  pntrsumo1  27304  cusgrsize2inds  28977  cusgrrusgr  29105  pthdlem2  29292  crctcshwlkn0lem4  29334  wlkiswwlks2lem1  29390  wlkiswwlksupgr2  29398  clwwlkccatlem  29509  clwlkclwwlklem2a2  29513  clwwlknwwlksn  29558  clwwlkel  29566  clwwlkwwlksb  29574  wwlksubclwwlk  29578  freshmansdream  32651  fibp1  33698  plymulx0  33856  plymulx  33857  signstfvn  33878  signsvtn0  33879  subfacp1lem6  34474  erdszelem10  34489  erdsze2lem1  34492  erdsze2lem2  34493  cvmliftlem2  34575  bcprod  35012  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem10  36801  poimirlem11  36802  poimirlem13  36804  poimirlem14  36805  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem25  36816  poimirlem26  36817  poimirlem31  36822  lcmfunnnd  41183  lcmineqlem2  41201  lcmineqlem3  41202  lcmineqlem8  41207  lcmineqlem10  41209  lcmineqlem12  41211  dvrelogpow2b  41239  sticksstones12a  41279  sticksstones16  41284  sticksstones22  41290  fltnltalem  41706  irrapxlem1  41862  rmspecsqrtnq  41946  jm2.24nn  42000  jm2.17a  42001  acongeq  42024  jm2.18  42029  jm2.22  42036  jm2.23  42037  jm2.20nn  42038  jm2.27c  42048  bccm1k  43403  binomcxplemwb  43409  binomcxplemnotnn0  43417  dvsinexp  44925  dvxpaek  44954  dvnxpaek  44956  itgsinexplem1  44968  itgsinexp  44969  wallispilem5  45083  stirlinglem5  45092  fourierdlem48  45168  fourierdlem49  45169  fourierdlem52  45172  fourierdlem54  45174  fourierdlem103  45223  fourierdlem104  45224  etransclem1  45249  etransclem4  45252  etransclem8  45256  etransclem10  45258  etransclem14  45262  etransclem15  45263  etransclem17  45265  etransclem18  45266  etransclem19  45267  etransclem20  45268  etransclem21  45269  etransclem22  45270  etransclem23  45271  etransclem24  45272  etransclem27  45275  etransclem28  45276  etransclem32  45280  etransclem35  45283  etransclem37  45285  etransclem38  45286  etransclem41  45289  etransclem44  45292  etransclem45  45293  etransclem46  45294  etransclem47  45295  etransclem48  45296  lswn0  46410  fmtnoodd  46499  sqrtpwpw2p  46504  fmtnosqrt  46505  fmtnodvds  46510  fmtnorec3  46514  fmtnorec4  46515  2pwp1prm  46555  lighneallem3  46573  lighneallem4a  46574  lighneallem4  46576  oexpnegALTV  46643  perfectALTV  46689  fpprmod  46693  fppr2odd  46697  fpprwppr  46705  fpprwpprb  46706  bgoldbtbndlem4  46774  bcpascm1  47115  altgsumbcALT  47117  pw2m1lepw2m1  47288  nnpw2even  47302  logbpw2m1  47340  nnpw2blenfzo  47354  nnpw2pmod  47356  nnpw2p  47359  nnolog2flm1  47363  dignn0fr  47374  dig2nn1st  47378  digexp  47380  dignn0flhalflem1  47388