Theorem nnm1nn0 12483

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 12207	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7394	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12258	. . . . . 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 12444	. 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 7387  0cc0 11068  1c1 11069   − cmin 11405  ℕcn 12186  ℕ₀cn0 12442

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407  df-nn 12187  df-n0 12443

This theorem is referenced by:  elnn0nn  12484  nn0n0n1ge2  12510  nnaddm1cl  12591  fseq1m1p1  13560  elfznelfzo  13733  nn0ennn  13944  expm1t  14055  expgt1  14065  digit1  14202  bcn1  14278  bcm1k  14280  bcn2m1  14289  cshwidxn  14774  isercoll2  15635  iseralt  15651  binomlem  15795  incexc  15803  incexc2  15804  arisum  15826  arisum2  15827  pwdif  15834  mertenslem2  15851  risefallfac  15990  fallfacfwd  16002  0fallfac  16003  bpolydiflem  16020  ruclem12  16209  iddvdsexp  16249  dvdsfac  16296  oexpneg  16315  pwp1fsum  16361  bitsfzolem  16404  bitsf1  16416  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  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  finodsubmsubg  19497  sylow1lem1  19528  efgsrel  19664  efgredlem  19677  srgbinomlem4  20138  freshmansdream  21484  psdpw  22057  chfacfisf  22741  chfacfisfcpmat  22742  cpmadugsumlemF  22763  lebnumii  24865  ovolunlem1  25398  dvexp  25857  dgreq0  26171  dvply1  26191  vieta1lem2  26219  aaliou3lem8  26253  dvtaylp  26278  taylthlem1  26281  pserdvlem2  26338  pserdv2  26340  abelthlem6  26346  logtayl  26569  logtayl2  26571  cxpeq  26667  gamfac  26977  wilthlem1  26978  wilthlem2  26979  wilthlem3  26980  wilth  26981  wilthimp  26982  ftalem1  26983  basellem5  26995  1sgm2ppw  27111  chtublem  27122  perfect1  27139  perfect  27142  bcmono  27188  lgslem1  27208  lgsquadlem1  27291  lgsquad2lem2  27296  m1lgs  27299  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  cusgrsize2inds  29381  cusgrrusgr  29509  pthdlem2  29698  crctcshwlkn0lem4  29743  wlkiswwlks2lem1  29799  wlkiswwlksupgr2  29807  clwwlkccatlem  29918  clwlkclwwlklem2a2  29922  clwwlknwwlksn  29967  clwwlkel  29975  clwwlkwwlksb  29983  wwlksubclwwlk  29987  oexpled  32772  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  fibp1  34392  plymulx0  34538  plymulx  34539  signstfvn  34560  signsvtn0  34561  subfacp1lem6  35172  erdszelem10  35187  erdsze2lem1  35190  erdsze2lem2  35191  cvmliftlem2  35273  bcprod  35725  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem13  37627  poimirlem14  37628  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem25  37639  poimirlem26  37640  poimirlem31  37645  lcmfunnnd  42000  lcmineqlem2  42018  lcmineqlem3  42019  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem12  42028  dvrelogpow2b  42056  primrootsunit1  42085  sticksstones12a  42145  sticksstones16  42150  sticksstones22  42156  fltnltalem  42650  irrapxlem1  42810  rmspecsqrtnq  42894  jm2.24nn  42948  jm2.17a  42949  acongeq  42972  jm2.18  42977  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.27c  42996  bccm1k  44331  binomcxplemwb  44337  binomcxplemnotnn0  44345  dvsinexp  45909  dvxpaek  45938  dvnxpaek  45940  itgsinexplem1  45952  itgsinexp  45953  wallispilem5  46067  stirlinglem5  46076  fourierdlem48  46152  fourierdlem49  46153  fourierdlem52  46156  fourierdlem54  46158  fourierdlem103  46207  fourierdlem104  46208  etransclem1  46233  etransclem4  46236  etransclem8  46240  etransclem10  46242  etransclem14  46246  etransclem15  46247  etransclem17  46249  etransclem18  46250  etransclem19  46251  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem27  46259  etransclem28  46260  etransclem32  46264  etransclem35  46267  etransclem37  46269  etransclem38  46270  etransclem41  46273  etransclem44  46276  etransclem45  46277  etransclem46  46278  etransclem47  46279  etransclem48  46280  lswn0  47445  fmtnoodd  47534  sqrtpwpw2p  47539  fmtnosqrt  47540  fmtnodvds  47545  fmtnorec3  47549  fmtnorec4  47550  2pwp1prm  47590  lighneallem3  47608  lighneallem4a  47609  lighneallem4  47611  oexpnegALTV  47678  perfectALTV  47724  fpprmod  47728  fppr2odd  47732  fpprwppr  47740  fpprwpprb  47741  bgoldbtbndlem4  47809  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