Theorem nnm1nn0 12469

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 12186	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7367	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12244	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2788	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 910	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 872	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12430	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  0cc0 11029  1c1 11030   − cmin 11368  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-nn 12166  df-n0 12429

This theorem is referenced by:  elnn0nn  12470  nn0n0n1ge2  12496  nnaddm1cl  12577  fseq1m1p1  13544  elfznelfzo  13719  nn0ennn  13932  expm1t  14043  expgt1  14053  digit1  14190  bcn1  14266  bcm1k  14268  bcn2m1  14277  cshwidxn  14762  isercoll2  15622  iseralt  15638  binomlem  15785  incexc  15793  incexc2  15794  arisum  15816  arisum2  15817  pwdif  15824  mertenslem2  15841  risefallfac  15980  fallfacfwd  15992  0fallfac  15993  bpolydiflem  16010  ruclem12  16199  iddvdsexp  16239  dvdsfac  16286  oexpneg  16305  pwp1fsum  16351  bitsfzolem  16394  bitsf1  16406  phibnd  16732  phiprmpw  16737  prmdiv  16746  oddprm  16772  iserodd  16797  fldivp1  16859  prmpwdvds  16866  4sqlem12  16918  4sqlem19  16925  vdwapid1  16937  vdwlem1  16943  vdwlem3  16945  vdwlem5  16947  vdwlem6  16948  vdwlem9  16951  0ram  16982  ram0  16984  ramub1lem1  16988  ramub1lem2  16989  ramcl  16991  prmonn2  17001  1259lem5  17096  2503lem3  17100  4001lem4  17105  chnrev  18584  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  finodsubmsubg  19533  sylow1lem1  19564  efgsrel  19700  efgredlem  19713  srgbinomlem4  20201  freshmansdream  21564  psdpw  22146  chfacfisf  22829  chfacfisfcpmat  22830  cpmadugsumlemF  22851  lebnumii  24943  ovolunlem1  25474  dvexp  25930  dgreq0  26240  dvply1  26260  vieta1lem2  26288  aaliou3lem8  26322  dvtaylp  26347  taylthlem1  26350  pserdvlem2  26406  pserdv2  26408  abelthlem6  26414  logtayl  26637  logtayl2  26639  cxpeq  26734  gamfac  27044  wilthlem1  27045  wilthlem2  27046  wilthlem3  27047  wilth  27048  wilthimp  27049  ftalem1  27050  basellem5  27062  1sgm2ppw  27177  chtublem  27188  perfect1  27205  perfect  27208  bcmono  27254  lgslem1  27274  lgsquadlem1  27357  lgsquad2lem2  27362  m1lgs  27365  selberg2lem  27527  logdivbnd  27533  pntrsumo1  27542  cusgrsize2inds  29537  cusgrrusgr  29665  pthdlem2  29851  crctcshwlkn0lem4  29896  wlkiswwlks2lem1  29952  wlkiswwlksupgr2  29960  clwwlkccatlem  30074  clwlkclwwlklem2a2  30078  clwwlknwwlksn  30123  clwwlkel  30131  clwwlkwwlksb  30139  wwlksubclwwlk  30143  oexpled  32935  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  esplyind  33734  fibp1  34561  plymulx0  34707  plymulx  34708  signstfvn  34729  signsvtn0  34730  subfacp1lem6  35383  erdszelem10  35398  erdsze2lem1  35401  erdsze2lem2  35402  cvmliftlem2  35484  bcprod  35936  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem13  37968  poimirlem14  37969  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem25  37980  poimirlem26  37981  poimirlem31  37986  lcmfunnnd  42465  lcmineqlem2  42483  lcmineqlem3  42484  lcmineqlem8  42489  lcmineqlem10  42491  lcmineqlem12  42493  dvrelogpow2b  42521  primrootsunit1  42550  sticksstones12a  42610  sticksstones16  42615  sticksstones22  42621  fltnltalem  43109  irrapxlem1  43268  rmspecsqrtnq  43352  jm2.24nn  43405  jm2.17a  43406  acongeq  43429  jm2.18  43434  jm2.22  43441  jm2.23  43442  jm2.20nn  43443  jm2.27c  43453  bccm1k  44787  binomcxplemwb  44793  binomcxplemnotnn0  44801  dvsinexp  46357  dvxpaek  46386  dvnxpaek  46388  itgsinexplem1  46400  itgsinexp  46401  wallispilem5  46515  stirlinglem5  46524  fourierdlem48  46600  fourierdlem49  46601  fourierdlem52  46604  fourierdlem54  46606  fourierdlem103  46655  fourierdlem104  46656  etransclem1  46681  etransclem4  46684  etransclem8  46688  etransclem10  46690  etransclem14  46694  etransclem15  46695  etransclem17  46697  etransclem18  46698  etransclem19  46699  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem27  46707  etransclem28  46708  etransclem32  46712  etransclem35  46715  etransclem37  46717  etransclem38  46718  etransclem41  46721  etransclem44  46724  etransclem45  46725  etransclem46  46726  etransclem47  46727  etransclem48  46728  muldvdsfacgt  47846  muldvdsfacm1  47847  lswn0  47916  fmtnoodd  48008  sqrtpwpw2p  48013  fmtnosqrt  48014  fmtnodvds  48019  fmtnorec3  48023  fmtnorec4  48024  2pwp1prm  48064  lighneallem3  48082  lighneallem4a  48083  lighneallem4  48085  nprmdvdsfacm1lem4  48098  ppivalnnprm  48100  ppivalnnnprmge6  48101  oexpnegALTV  48165  perfectALTV  48211  fpprmod  48215  fppr2odd  48219  fpprwppr  48227  fpprwpprb  48228  bgoldbtbndlem4  48296  bcpascm1  48839  altgsumbcALT  48841  pw2m1lepw2m1  49008  nnpw2even  49017  logbpw2m1  49055  nnpw2blenfzo  49069  nnpw2pmod  49071  nnpw2p  49074  nnolog2flm1  49078  dignn0fr  49089  dig2nn1st  49093  digexp  49095  dignn0flhalflem1  49103