Theorem nnm1nn0 12478

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 12195	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7374	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12253	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2787	. . . . 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 12439	. 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 7367  0cc0 11038  1c1 11039   − cmin 11377  ℕcn 12174  ℕ₀cn0 12437

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379  df-nn 12175  df-n0 12438

This theorem is referenced by:  elnn0nn  12479  nn0n0n1ge2  12505  nnaddm1cl  12586  fseq1m1p1  13553  elfznelfzo  13728  nn0ennn  13941  expm1t  14052  expgt1  14062  digit1  14199  bcn1  14275  bcm1k  14277  bcn2m1  14286  cshwidxn  14771  isercoll2  15631  iseralt  15647  binomlem  15794  incexc  15802  incexc2  15803  arisum  15825  arisum2  15826  pwdif  15833  mertenslem2  15850  risefallfac  15989  fallfacfwd  16001  0fallfac  16002  bpolydiflem  16019  ruclem12  16208  iddvdsexp  16248  dvdsfac  16295  oexpneg  16314  pwp1fsum  16360  bitsfzolem  16403  bitsf1  16415  phibnd  16741  phiprmpw  16746  prmdiv  16755  oddprm  16781  iserodd  16806  fldivp1  16868  prmpwdvds  16875  4sqlem12  16927  4sqlem19  16934  vdwapid1  16946  vdwlem1  16952  vdwlem3  16954  vdwlem5  16956  vdwlem6  16957  vdwlem9  16960  0ram  16991  ram0  16993  ramub1lem1  16997  ramub1lem2  16998  ramcl  17000  prmonn2  17010  1259lem5  17105  2503lem3  17109  4001lem4  17114  chnrev  18593  gsumwsubmcl  18805  gsumsgrpccat  18808  gsumwmhm  18813  finodsubmsubg  19542  sylow1lem1  19573  efgsrel  19709  efgredlem  19722  srgbinomlem4  20210  freshmansdream  21554  psdpw  22136  chfacfisf  22819  chfacfisfcpmat  22820  cpmadugsumlemF  22841  lebnumii  24933  ovolunlem1  25464  dvexp  25920  dgreq0  26230  dvply1  26250  vieta1lem2  26277  aaliou3lem8  26311  dvtaylp  26335  taylthlem1  26338  pserdvlem2  26393  pserdv2  26395  abelthlem6  26401  logtayl  26624  logtayl2  26626  cxpeq  26721  gamfac  27030  wilthlem1  27031  wilthlem2  27032  wilthlem3  27033  wilth  27034  wilthimp  27035  ftalem1  27036  basellem5  27048  1sgm2ppw  27163  chtublem  27174  perfect1  27191  perfect  27194  bcmono  27240  lgslem1  27260  lgsquadlem1  27343  lgsquad2lem2  27348  m1lgs  27351  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  cusgrsize2inds  29522  cusgrrusgr  29650  pthdlem2  29836  crctcshwlkn0lem4  29881  wlkiswwlks2lem1  29937  wlkiswwlksupgr2  29945  clwwlkccatlem  30059  clwlkclwwlklem2a2  30063  clwwlknwwlksn  30108  clwwlkel  30116  clwwlkwwlksb  30124  wwlksubclwwlk  30128  oexpled  32920  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  esplyind  33719  fibp1  34545  plymulx0  34691  plymulx  34692  signstfvn  34713  signsvtn0  34714  subfacp1lem6  35367  erdszelem10  35382  erdsze2lem1  35385  erdsze2lem2  35386  cvmliftlem2  35468  bcprod  35920  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem13  37954  poimirlem14  37955  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem25  37966  poimirlem26  37967  poimirlem31  37972  lcmfunnnd  42451  lcmineqlem2  42469  lcmineqlem3  42470  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem12  42479  dvrelogpow2b  42507  primrootsunit1  42536  sticksstones12a  42596  sticksstones16  42601  sticksstones22  42607  fltnltalem  43095  irrapxlem1  43250  rmspecsqrtnq  43334  jm2.24nn  43387  jm2.17a  43388  acongeq  43411  jm2.18  43416  jm2.22  43423  jm2.23  43424  jm2.20nn  43425  jm2.27c  43435  bccm1k  44769  binomcxplemwb  44775  binomcxplemnotnn0  44783  dvsinexp  46339  dvxpaek  46368  dvnxpaek  46370  itgsinexplem1  46382  itgsinexp  46383  wallispilem5  46497  stirlinglem5  46506  fourierdlem48  46582  fourierdlem49  46583  fourierdlem52  46586  fourierdlem54  46588  fourierdlem103  46637  fourierdlem104  46638  etransclem1  46663  etransclem4  46666  etransclem8  46670  etransclem10  46672  etransclem14  46676  etransclem15  46677  etransclem17  46679  etransclem18  46680  etransclem19  46681  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem27  46689  etransclem28  46690  etransclem32  46694  etransclem35  46697  etransclem37  46699  etransclem38  46700  etransclem41  46703  etransclem44  46706  etransclem45  46707  etransclem46  46708  etransclem47  46709  etransclem48  46710  muldvdsfacgt  47834  muldvdsfacm1  47835  lswn0  47904  fmtnoodd  47996  sqrtpwpw2p  48001  fmtnosqrt  48002  fmtnodvds  48007  fmtnorec3  48011  fmtnorec4  48012  2pwp1prm  48052  lighneallem3  48070  lighneallem4a  48071  lighneallem4  48073  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  ppivalnnnprmge6  48089  oexpnegALTV  48153  perfectALTV  48199  fpprmod  48203  fppr2odd  48207  fpprwppr  48215  fpprwpprb  48216  bgoldbtbndlem4  48284  bcpascm1  48827  altgsumbcALT  48829  pw2m1lepw2m1  48996  nnpw2even  49005  logbpw2m1  49043  nnpw2blenfzo  49057  nnpw2pmod  49059  nnpw2p  49062  nnolog2flm1  49066  dignn0fr  49077  dig2nn1st  49081  digexp  49083  dignn0flhalflem1  49091