Theorem nnm1nn0 12556

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 12265	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7423	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12324	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2816	. . . . 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 12517	. 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 2146  (class class class)co 7416  0cc0 11111  1c1 11112   − cmin 11452  ℕcn 12244  ℕ₀cn0 12515

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-ltxr 11259  df-sub 11454  df-nn 12245  df-n0 12516

This theorem is used by:  elnn0nn  12557  nn0n0n1ge2  12583  nnaddm1cl  12664  fseq1m1p1  13639  elfznelfzo  13814  nn0ennn  14028  expm1t  14139  expgt1  14149  digit1  14286  bcn1  14362  bcm1k  14364  bcn2m1  14373  cshwidxn  14865  isercoll2  15739  iseralt  15755  binomlem  15901  incexc  15909  incexc2  15910  arisum  15932  arisum2  15933  pwdif  15940  mertenslem2  15957  risefallfac  16096  fallfacfwd  16107  0fallfac  16108  bpolydiflem  16125  ruclem12  16314  iddvdsexp  16354  dvdsfac  16401  oexpneg  16420  pwp1fsum  16466  bitsfzolem  16509  bitsf1  16521  phibnd  16847  phiprmpw  16852  prmdiv  16861  oddprm  16887  iserodd  16912  fldivp1  16974  prmpwdvds  16981  4sqlem12  17033  4sqlem19  17040  vdwapid1  17052  vdwlem1  17058  vdwlem3  17060  vdwlem5  17062  vdwlem6  17063  vdwlem9  17066  0ram  17097  ram0  17099  ramub1lem1  17103  ramub1lem2  17104  ramcl  17106  prmonn2  17116  1259lem5  17212  2503lem3  17216  4001lem4  17221  chnrev  18700  gsumwsubmcl  18919  gsumsgrpccat  18922  gsumwmhm  18927  finodsubmsubg  19660  sylow1lem1  19691  efgsrel  19827  efgredlem  19840  srgbinomlem4  20334  freshmansdream  21753  psdpw  22362  chfacfisf  23040  chfacfisfcpmat  23041  cpmadugsumlemF  23062  lebnumii  25154  ovolunlem1  25685  dvexp  26141  dgreq0  26451  plyn0mulidp  26471  plymulidp  26472  dvply1  26474  vieta1lem2  26501  aaliou3lem8  26537  dvtaylp  26562  taylthlem1  26565  pserdvlem2  26620  pserdv2  26622  abelthlem6  26628  logtayl  26854  logtayl2  26856  cxpeq  26951  gamfac  27260  wilthlem1  27261  wilthlem2  27262  wilthlem3  27263  wilth  27264  wilthimp  27265  ftalem1  27266  basellem5  27278  1sgm2ppw  27393  chtublem  27404  perfect1  27421  perfect  27424  bcmono  27470  lgslem1  27490  lgsquadlem1  27573  lgsquad2lem2  27578  m1lgs  27581  selberg2lem  27743  logdivbnd  27749  pntrsumo1  27758  cusgrsize2inds  29832  cusgrrusgr  29960  pthdlem2  30146  crctcshwlkn0lem4  30191  wlkiswwlks2lem1  30247  wlkiswwlksupgr2  30255  clwwlkccatlem  30369  clwlkclwwlklem2a2  30373  clwwlknwwlksn  30418  clwwlkel  30426  clwwlkwwlksb  30434  wwlksubclwwlk  30438  oexpled  33209  1arithidomlem1  33848  1arithidomlem2  33849  1arithidom  33850  esplyind  33988  fibp1  34815  signstfvn  34980  signsvtn0  34981  subfacp1lem6  35690  erdszelem10  35705  erdsze2lem1  35708  erdsze2lem2  35709  cvmliftlem2  35791  bcprod  36243  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem10  38314  poimirlem11  38315  poimirlem13  38317  poimirlem14  38318  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem23  38327  poimirlem25  38329  poimirlem26  38330  poimirlem31  38335  lcmfunnnd  42812  lcmineqlem2  42830  lcmineqlem3  42831  lcmineqlem8  42836  lcmineqlem10  42838  lcmineqlem12  42840  dvrelogpow2b  42868  primrootsunit1  42897  sticksstones12a  42957  sticksstones16  42962  sticksstones22  42968  fltnltalem  43427  irrapxlem1  43582  rmspecsqrtnq  43666  jm2.24nn  43719  jm2.17a  43720  acongeq  43743  jm2.18  43748  jm2.22  43755  jm2.23  43756  jm2.20nn  43757  jm2.27c  43767  bccm1k  45085  binomcxplemwb  45091  binomcxplemnotnn0  45099  dvsinexp  46658  dvxpaek  46687  dvnxpaek  46689  itgsinexplem1  46701  itgsinexp  46702  wallispilem5  46816  stirlinglem5  46825  fourierdlem48  46901  fourierdlem49  46902  fourierdlem52  46905  fourierdlem54  46907  fourierdlem103  46956  fourierdlem104  46957  etransclem1  46982  etransclem4  46985  etransclem8  46989  etransclem10  46991  etransclem14  46995  etransclem15  46996  etransclem17  46998  etransclem18  46999  etransclem19  47000  etransclem20  47001  etransclem21  47002  etransclem22  47003  etransclem23  47004  etransclem24  47005  etransclem27  47008  etransclem28  47009  etransclem32  47013  etransclem35  47016  etransclem37  47018  etransclem38  47019  etransclem41  47022  etransclem44  47025  etransclem45  47026  etransclem46  47027  etransclem47  47028  etransclem48  47029  muldvdsfacgt  48156  muldvdsfacm1  48157  lswn0  48226  fmtnoodd  48318  sqrtpwpw2p  48323  fmtnosqrt  48324  fmtnodvds  48329  fmtnorec3  48333  fmtnorec4  48334  2pwp1prm  48374  lighneallem3  48392  lighneallem4a  48393  lighneallem4  48395  nprmdvdsfacm1lem4  48408  ppivalnnprm  48410  ppivalnnnprmge6  48411  oexpnegALTV  48475  perfectALTV  48521  fpprmod  48525  fppr2odd  48529  fpprwppr  48537  fpprwpprb  48538  bgoldbtbndlem4  48606  bcpascm1  49164  altgsumbcALT  49166  pw2m1lepw2m1  49333  nnpw2even  49342  logbpw2m1  49380  nnpw2blenfzo  49394  nnpw2pmod  49396  nnpw2p  49399  nnolog2flm1  49403  dignn0fr  49414  dig2nn1st  49418  digexp  49420  dignn0flhalflem1  49428