Theorem nnm1nn0 12516

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 12225	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7398	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12284	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2812	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 920	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 882	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12477	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 236	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1559   ∈ wcel 2141  (class class class)co 7391  0cc0 11067  1c1 11068   − cmin 11408  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215  df-sub 11410  df-nn 12205  df-n0 12476

This theorem is referenced by:  elnn0nn  12517  nn0n0n1ge2  12543  nnaddm1cl  12624  fseq1m1p1  13598  elfznelfzo  13773  nn0ennn  13986  expm1t  14097  expgt1  14107  digit1  14244  bcn1  14320  bcm1k  14322  bcn2m1  14331  cshwidxn  14816  isercoll2  15687  iseralt  15703  binomlem  15850  incexc  15858  incexc2  15859  arisum  15881  arisum2  15882  pwdif  15889  mertenslem2  15906  risefallfac  16045  fallfacfwd  16057  0fallfac  16058  bpolydiflem  16075  ruclem12  16264  iddvdsexp  16304  dvdsfac  16351  oexpneg  16370  pwp1fsum  16416  bitsfzolem  16459  bitsf1  16471  phibnd  16797  phiprmpw  16802  prmdiv  16811  oddprm  16837  iserodd  16862  fldivp1  16924  prmpwdvds  16931  4sqlem12  16983  4sqlem19  16990  vdwapid1  17002  vdwlem1  17008  vdwlem3  17010  vdwlem5  17012  vdwlem6  17013  vdwlem9  17016  0ram  17047  ram0  17049  ramub1lem1  17053  ramub1lem2  17054  ramcl  17056  prmonn2  17066  1259lem5  17162  2503lem3  17166  4001lem4  17171  chnrev  18650  gsumwsubmcl  18862  gsumsgrpccat  18865  gsumwmhm  18870  finodsubmsubg  19598  sylow1lem1  19629  efgsrel  19765  efgredlem  19778  srgbinomlem4  20266  freshmansdream  21614  psdpw  22223  chfacfisf  22902  chfacfisfcpmat  22903  cpmadugsumlemF  22924  lebnumii  25016  ovolunlem1  25547  dvexp  26003  dgreq0  26313  plyn0mulidp  26333  plymulidp  26334  dvply1  26336  vieta1lem2  26363  aaliou3lem8  26397  dvtaylp  26421  taylthlem1  26424  pserdvlem2  26479  pserdv2  26481  abelthlem6  26487  logtayl  26713  logtayl2  26715  cxpeq  26810  gamfac  27119  wilthlem1  27120  wilthlem2  27121  wilthlem3  27122  wilth  27123  wilthimp  27124  ftalem1  27125  basellem5  27137  1sgm2ppw  27252  chtublem  27263  perfect1  27280  perfect  27283  bcmono  27329  lgslem1  27349  lgsquadlem1  27432  lgsquad2lem2  27437  m1lgs  27440  selberg2lem  27602  logdivbnd  27608  pntrsumo1  27617  cusgrsize2inds  29611  cusgrrusgr  29739  pthdlem2  29925  crctcshwlkn0lem4  29970  wlkiswwlks2lem1  30026  wlkiswwlksupgr2  30034  clwwlkccatlem  30148  clwlkclwwlklem2a2  30152  clwwlknwwlksn  30197  clwwlkel  30205  clwwlkwwlksb  30213  wwlksubclwwlk  30217  oexpled  32999  1arithidomlem1  33692  1arithidomlem2  33693  1arithidom  33694  esplyind  33833  fibp1  34659  signstfvn  34824  signsvtn0  34825  subfacp1lem6  35496  erdszelem10  35511  erdsze2lem1  35514  erdsze2lem2  35515  cvmliftlem2  35597  bcprod  36049  poimirlem5  38085  poimirlem6  38086  poimirlem7  38087  poimirlem10  38090  poimirlem11  38091  poimirlem13  38093  poimirlem14  38094  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem23  38103  poimirlem25  38105  poimirlem26  38106  poimirlem31  38111  lcmfunnnd  42590  lcmineqlem2  42608  lcmineqlem3  42609  lcmineqlem8  42614  lcmineqlem10  42616  lcmineqlem12  42618  dvrelogpow2b  42646  primrootsunit1  42675  sticksstones12a  42735  sticksstones16  42740  sticksstones22  42746  fltnltalem  43205  irrapxlem1  43360  rmspecsqrtnq  43444  jm2.24nn  43497  jm2.17a  43498  acongeq  43521  jm2.18  43526  jm2.22  43533  jm2.23  43534  jm2.20nn  43535  jm2.27c  43545  bccm1k  44879  binomcxplemwb  44885  binomcxplemnotnn0  44893  dvsinexp  46446  dvxpaek  46475  dvnxpaek  46477  itgsinexplem1  46489  itgsinexp  46490  wallispilem5  46604  stirlinglem5  46613  fourierdlem48  46689  fourierdlem49  46690  fourierdlem52  46693  fourierdlem54  46695  fourierdlem103  46744  fourierdlem104  46745  etransclem1  46770  etransclem4  46773  etransclem8  46777  etransclem10  46779  etransclem14  46783  etransclem15  46784  etransclem17  46786  etransclem18  46787  etransclem19  46788  etransclem20  46789  etransclem21  46790  etransclem22  46791  etransclem23  46792  etransclem24  46793  etransclem27  46796  etransclem28  46797  etransclem32  46801  etransclem35  46804  etransclem37  46806  etransclem38  46807  etransclem41  46810  etransclem44  46813  etransclem45  46814  etransclem46  46815  etransclem47  46816  etransclem48  46817  muldvdsfacgt  47941  muldvdsfacm1  47942  lswn0  48011  fmtnoodd  48103  sqrtpwpw2p  48108  fmtnosqrt  48109  fmtnodvds  48114  fmtnorec3  48118  fmtnorec4  48119  2pwp1prm  48159  lighneallem3  48177  lighneallem4a  48178  lighneallem4  48180  nprmdvdsfacm1lem4  48193  ppivalnnprm  48195  ppivalnnnprmge6  48196  oexpnegALTV  48260  perfectALTV  48306  fpprmod  48310  fppr2odd  48314  fpprwppr  48322  fpprwpprb  48323  bgoldbtbndlem4  48391  bcpascm1  48934  altgsumbcALT  48936  pw2m1lepw2m1  49103  nnpw2even  49112  logbpw2m1  49150  nnpw2blenfzo  49164  nnpw2pmod  49166  nnpw2p  49169  nnolog2flm1  49173  dignn0fr  49184  dig2nn1st  49188  digexp  49190  dignn0flhalflem1  49198