Theorem nnm1nn0 12567

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 12287	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7438	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12338	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2793	. . . . 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 12528	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  0cc0 11155  1c1 11156   − cmin 11492  ℕcn 12266  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494  df-nn 12267  df-n0 12527

This theorem is referenced by:  elnn0nn  12568  nn0n0n1ge2  12594  nnaddm1cl  12675  fseq1m1p1  13639  elfznelfzo  13811  nn0ennn  14020  expm1t  14131  expgt1  14141  digit1  14276  bcn1  14352  bcm1k  14354  bcn2m1  14363  cshwidxn  14847  isercoll2  15705  iseralt  15721  binomlem  15865  incexc  15873  incexc2  15874  arisum  15896  arisum2  15897  pwdif  15904  mertenslem2  15921  risefallfac  16060  fallfacfwd  16072  0fallfac  16073  bpolydiflem  16090  ruclem12  16277  iddvdsexp  16317  dvdsfac  16363  oexpneg  16382  pwp1fsum  16428  bitsfzolem  16471  bitsf1  16483  phibnd  16808  phiprmpw  16813  prmdiv  16822  oddprm  16848  iserodd  16873  fldivp1  16935  prmpwdvds  16942  4sqlem12  16994  4sqlem19  17001  vdwapid1  17013  vdwlem1  17019  vdwlem3  17021  vdwlem5  17023  vdwlem6  17024  vdwlem9  17027  0ram  17058  ram0  17060  ramub1lem1  17064  ramub1lem2  17065  ramcl  17067  prmonn2  17077  1259lem5  17172  2503lem3  17176  4001lem4  17181  gsumwsubmcl  18850  gsumsgrpccat  18853  gsumwmhm  18858  finodsubmsubg  19585  sylow1lem1  19616  efgsrel  19752  efgredlem  19765  srgbinomlem4  20226  freshmansdream  21593  psdpw  22174  chfacfisf  22860  chfacfisfcpmat  22861  cpmadugsumlemF  22882  lebnumii  24998  ovolunlem1  25532  dvexp  25991  dgreq0  26305  dvply1  26325  vieta1lem2  26353  aaliou3lem8  26387  dvtaylp  26412  taylthlem1  26415  pserdvlem2  26472  pserdv2  26474  abelthlem6  26480  logtayl  26702  logtayl2  26704  cxpeq  26800  gamfac  27110  wilthlem1  27111  wilthlem2  27112  wilthlem3  27113  wilth  27114  wilthimp  27115  ftalem1  27116  basellem5  27128  1sgm2ppw  27244  chtublem  27255  perfect1  27272  perfect  27275  bcmono  27321  lgslem1  27341  lgsquadlem1  27424  lgsquad2lem2  27429  m1lgs  27432  selberg2lem  27594  logdivbnd  27600  pntrsumo1  27609  cusgrsize2inds  29471  cusgrrusgr  29599  pthdlem2  29788  crctcshwlkn0lem4  29833  wlkiswwlks2lem1  29889  wlkiswwlksupgr2  29897  clwwlkccatlem  30008  clwlkclwwlklem2a2  30012  clwwlknwwlksn  30057  clwwlkel  30065  clwwlkwwlksb  30073  wwlksubclwwlk  30077  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  fibp1  34403  plymulx0  34562  plymulx  34563  signstfvn  34584  signsvtn0  34585  subfacp1lem6  35190  erdszelem10  35205  erdsze2lem1  35208  erdsze2lem2  35209  cvmliftlem2  35291  bcprod  35738  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem13  37640  poimirlem14  37641  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem25  37652  poimirlem26  37653  poimirlem31  37658  lcmfunnnd  42013  lcmineqlem2  42031  lcmineqlem3  42032  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem12  42041  dvrelogpow2b  42069  primrootsunit1  42098  sticksstones12a  42158  sticksstones16  42163  sticksstones22  42169  fltnltalem  42672  irrapxlem1  42833  rmspecsqrtnq  42917  jm2.24nn  42971  jm2.17a  42972  acongeq  42995  jm2.18  43000  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.27c  43019  bccm1k  44361  binomcxplemwb  44367  binomcxplemnotnn0  44375  dvsinexp  45926  dvxpaek  45955  dvnxpaek  45957  itgsinexplem1  45969  itgsinexp  45970  wallispilem5  46084  stirlinglem5  46093  fourierdlem48  46169  fourierdlem49  46170  fourierdlem52  46173  fourierdlem54  46175  fourierdlem103  46224  fourierdlem104  46225  etransclem1  46250  etransclem4  46253  etransclem8  46257  etransclem10  46259  etransclem14  46263  etransclem15  46264  etransclem17  46266  etransclem18  46267  etransclem19  46268  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem27  46276  etransclem28  46277  etransclem32  46281  etransclem35  46284  etransclem37  46286  etransclem38  46287  etransclem41  46290  etransclem44  46293  etransclem45  46294  etransclem46  46295  etransclem47  46296  etransclem48  46297  lswn0  47431  fmtnoodd  47520  sqrtpwpw2p  47525  fmtnosqrt  47526  fmtnodvds  47531  fmtnorec3  47535  fmtnorec4  47536  2pwp1prm  47576  lighneallem3  47594  lighneallem4a  47595  lighneallem4  47597  oexpnegALTV  47664  perfectALTV  47710  fpprmod  47714  fppr2odd  47718  fpprwppr  47726  fpprwpprb  47727  bgoldbtbndlem4  47795  bcpascm1  48267  altgsumbcALT  48269  pw2m1lepw2m1  48437  nnpw2even  48450  logbpw2m1  48488  nnpw2blenfzo  48502  nnpw2pmod  48504  nnpw2p  48507  nnolog2flm1  48511  dignn0fr  48522  dig2nn1st  48526  digexp  48528  dignn0flhalflem1  48536