Theorem nnm1nn0 12443

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 12167	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7360	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12218	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2780	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 909	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 871	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12404	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  0cc0 11028  1c1 11029   − cmin 11365  ℕcn 12146  ℕ₀cn0 12402

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11367  df-nn 12147  df-n0 12403

This theorem is referenced by:  elnn0nn  12444  nn0n0n1ge2  12470  nnaddm1cl  12551  fseq1m1p1  13520  elfznelfzo  13693  nn0ennn  13904  expm1t  14015  expgt1  14025  digit1  14162  bcn1  14238  bcm1k  14240  bcn2m1  14249  cshwidxn  14733  isercoll2  15594  iseralt  15610  binomlem  15754  incexc  15762  incexc2  15763  arisum  15785  arisum2  15786  pwdif  15793  mertenslem2  15810  risefallfac  15949  fallfacfwd  15961  0fallfac  15962  bpolydiflem  15979  ruclem12  16168  iddvdsexp  16208  dvdsfac  16255  oexpneg  16274  pwp1fsum  16320  bitsfzolem  16363  bitsf1  16375  phibnd  16700  phiprmpw  16705  prmdiv  16714  oddprm  16740  iserodd  16765  fldivp1  16827  prmpwdvds  16834  4sqlem12  16886  4sqlem19  16893  vdwapid1  16905  vdwlem1  16911  vdwlem3  16913  vdwlem5  16915  vdwlem6  16916  vdwlem9  16919  0ram  16950  ram0  16952  ramub1lem1  16956  ramub1lem2  16957  ramcl  16959  prmonn2  16969  1259lem5  17064  2503lem3  17068  4001lem4  17073  gsumwsubmcl  18729  gsumsgrpccat  18732  gsumwmhm  18737  finodsubmsubg  19464  sylow1lem1  19495  efgsrel  19631  efgredlem  19644  srgbinomlem4  20132  freshmansdream  21499  psdpw  22073  chfacfisf  22757  chfacfisfcpmat  22758  cpmadugsumlemF  22779  lebnumii  24881  ovolunlem1  25414  dvexp  25873  dgreq0  26187  dvply1  26207  vieta1lem2  26235  aaliou3lem8  26269  dvtaylp  26294  taylthlem1  26297  pserdvlem2  26354  pserdv2  26356  abelthlem6  26362  logtayl  26585  logtayl2  26587  cxpeq  26683  gamfac  26993  wilthlem1  26994  wilthlem2  26995  wilthlem3  26996  wilth  26997  wilthimp  26998  ftalem1  26999  basellem5  27011  1sgm2ppw  27127  chtublem  27138  perfect1  27155  perfect  27158  bcmono  27204  lgslem1  27224  lgsquadlem1  27307  lgsquad2lem2  27312  m1lgs  27315  selberg2lem  27477  logdivbnd  27483  pntrsumo1  27492  cusgrsize2inds  29417  cusgrrusgr  29545  pthdlem2  29731  crctcshwlkn0lem4  29776  wlkiswwlks2lem1  29832  wlkiswwlksupgr2  29840  clwwlkccatlem  29951  clwlkclwwlklem2a2  29955  clwwlknwwlksn  30000  clwwlkel  30008  clwwlkwwlksb  30016  wwlksubclwwlk  30020  oexpled  32805  1arithidomlem1  33485  1arithidomlem2  33486  1arithidom  33487  fibp1  34371  plymulx0  34517  plymulx  34518  signstfvn  34539  signsvtn0  34540  subfacp1lem6  35160  erdszelem10  35175  erdsze2lem1  35178  erdsze2lem2  35179  cvmliftlem2  35261  bcprod  35713  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  poimirlem13  37615  poimirlem14  37616  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem25  37627  poimirlem26  37628  poimirlem31  37633  lcmfunnnd  41988  lcmineqlem2  42006  lcmineqlem3  42007  lcmineqlem8  42012  lcmineqlem10  42014  lcmineqlem12  42016  dvrelogpow2b  42044  primrootsunit1  42073  sticksstones12a  42133  sticksstones16  42138  sticksstones22  42144  fltnltalem  42638  irrapxlem1  42798  rmspecsqrtnq  42882  jm2.24nn  42935  jm2.17a  42936  acongeq  42959  jm2.18  42964  jm2.22  42971  jm2.23  42972  jm2.20nn  42973  jm2.27c  42983  bccm1k  44318  binomcxplemwb  44324  binomcxplemnotnn0  44332  dvsinexp  45896  dvxpaek  45925  dvnxpaek  45927  itgsinexplem1  45939  itgsinexp  45940  wallispilem5  46054  stirlinglem5  46063  fourierdlem48  46139  fourierdlem49  46140  fourierdlem52  46143  fourierdlem54  46145  fourierdlem103  46194  fourierdlem104  46195  etransclem1  46220  etransclem4  46223  etransclem8  46227  etransclem10  46229  etransclem14  46233  etransclem15  46234  etransclem17  46236  etransclem18  46237  etransclem19  46238  etransclem20  46239  etransclem21  46240  etransclem22  46241  etransclem23  46242  etransclem24  46243  etransclem27  46246  etransclem28  46247  etransclem32  46251  etransclem35  46254  etransclem37  46256  etransclem38  46257  etransclem41  46260  etransclem44  46263  etransclem45  46264  etransclem46  46265  etransclem47  46266  etransclem48  46267  lswn0  47432  fmtnoodd  47521  sqrtpwpw2p  47526  fmtnosqrt  47527  fmtnodvds  47532  fmtnorec3  47536  fmtnorec4  47537  2pwp1prm  47577  lighneallem3  47595  lighneallem4a  47596  lighneallem4  47598  oexpnegALTV  47665  perfectALTV  47711  fpprmod  47715  fppr2odd  47719  fpprwppr  47727  fpprwpprb  47728  bgoldbtbndlem4  47796  bcpascm1  48339  altgsumbcALT  48341  pw2m1lepw2m1  48509  nnpw2even  48518  logbpw2m1  48556  nnpw2blenfzo  48570  nnpw2pmod  48572  nnpw2p  48575  nnolog2flm1  48579  dignn0fr  48590  dig2nn1st  48594  digexp  48596  dignn0flhalflem1  48604