Theorem nnm1nn0 12541

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 12250	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7415	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12309	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2820	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 922	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 18	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 884	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12502	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1567   ∈ wcel 2149  (class class class)co 7408  0cc0 11096  1c1 11097   − cmin 11437  ℕcn 12229  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-ltxr 11244  df-sub 11439  df-nn 12230  df-n0 12501

This theorem is referenced by:  elnn0nn  12542  nn0n0n1ge2  12568  nnaddm1cl  12649  fseq1m1p1  13623  elfznelfzo  13798  nn0ennn  14011  expm1t  14122  expgt1  14132  digit1  14269  bcn1  14345  bcm1k  14347  bcn2m1  14356  cshwidxn  14842  isercoll2  15716  iseralt  15732  binomlem  15879  incexc  15887  incexc2  15888  arisum  15910  arisum2  15911  pwdif  15918  mertenslem2  15935  risefallfac  16074  fallfacfwd  16086  0fallfac  16087  bpolydiflem  16104  ruclem12  16293  iddvdsexp  16333  dvdsfac  16380  oexpneg  16399  pwp1fsum  16445  bitsfzolem  16488  bitsf1  16500  phibnd  16826  phiprmpw  16831  prmdiv  16840  oddprm  16866  iserodd  16891  fldivp1  16953  prmpwdvds  16960  4sqlem12  17012  4sqlem19  17019  vdwapid1  17031  vdwlem1  17037  vdwlem3  17039  vdwlem5  17041  vdwlem6  17042  vdwlem9  17045  0ram  17076  ram0  17078  ramub1lem1  17082  ramub1lem2  17083  ramcl  17085  prmonn2  17095  1259lem5  17191  2503lem3  17195  4001lem4  17200  chnrev  18679  gsumwsubmcl  18892  gsumsgrpccat  18895  gsumwmhm  18900  finodsubmsubg  19633  sylow1lem1  19664  efgsrel  19800  efgredlem  19813  srgbinomlem4  20307  freshmansdream  21689  psdpw  22298  chfacfisf  22976  chfacfisfcpmat  22977  cpmadugsumlemF  22998  lebnumii  25090  ovolunlem1  25621  dvexp  26077  dgreq0  26387  plyn0mulidp  26407  plymulidp  26408  dvply1  26410  vieta1lem2  26437  aaliou3lem8  26471  dvtaylp  26495  taylthlem1  26498  pserdvlem2  26553  pserdv2  26555  abelthlem6  26561  logtayl  26787  logtayl2  26789  cxpeq  26884  gamfac  27193  wilthlem1  27194  wilthlem2  27195  wilthlem3  27196  wilth  27197  wilthimp  27198  ftalem1  27199  basellem5  27211  1sgm2ppw  27326  chtublem  27337  perfect1  27354  perfect  27357  bcmono  27403  lgslem1  27423  lgsquadlem1  27506  lgsquad2lem2  27511  m1lgs  27514  selberg2lem  27676  logdivbnd  27682  pntrsumo1  27691  cusgrsize2inds  29740  cusgrrusgr  29868  pthdlem2  30054  crctcshwlkn0lem4  30099  wlkiswwlks2lem1  30155  wlkiswwlksupgr2  30163  clwwlkccatlem  30277  clwlkclwwlklem2a2  30281  clwwlknwwlksn  30326  clwwlkel  30334  clwwlkwwlksb  30342  wwlksubclwwlk  30346  oexpled  33117  1arithidomlem1  33766  1arithidomlem2  33767  1arithidom  33768  esplyind  33906  fibp1  34732  signstfvn  34897  signsvtn0  34898  subfacp1lem6  35572  erdszelem10  35587  erdsze2lem1  35590  erdsze2lem2  35591  cvmliftlem2  35673  bcprod  36125  poimirlem5  38159  poimirlem6  38160  poimirlem7  38161  poimirlem10  38164  poimirlem11  38165  poimirlem13  38167  poimirlem14  38168  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  poimirlem23  38177  poimirlem25  38179  poimirlem26  38180  poimirlem31  38185  lcmfunnnd  42664  lcmineqlem2  42682  lcmineqlem3  42683  lcmineqlem8  42688  lcmineqlem10  42690  lcmineqlem12  42692  dvrelogpow2b  42720  primrootsunit1  42749  sticksstones12a  42809  sticksstones16  42814  sticksstones22  42820  fltnltalem  43279  irrapxlem1  43434  rmspecsqrtnq  43518  jm2.24nn  43571  jm2.17a  43572  acongeq  43595  jm2.18  43600  jm2.22  43607  jm2.23  43608  jm2.20nn  43609  jm2.27c  43619  bccm1k  44937  binomcxplemwb  44943  binomcxplemnotnn0  44951  dvsinexp  46510  dvxpaek  46539  dvnxpaek  46541  itgsinexplem1  46553  itgsinexp  46554  wallispilem5  46668  stirlinglem5  46677  fourierdlem48  46753  fourierdlem49  46754  fourierdlem52  46757  fourierdlem54  46759  fourierdlem103  46808  fourierdlem104  46809  etransclem1  46834  etransclem4  46837  etransclem8  46841  etransclem10  46843  etransclem14  46847  etransclem15  46848  etransclem17  46850  etransclem18  46851  etransclem19  46852  etransclem20  46853  etransclem21  46854  etransclem22  46855  etransclem23  46856  etransclem24  46857  etransclem27  46860  etransclem28  46861  etransclem32  46865  etransclem35  46868  etransclem37  46870  etransclem38  46871  etransclem41  46874  etransclem44  46877  etransclem45  46878  etransclem46  46879  etransclem47  46880  etransclem48  46881  muldvdsfacgt  48005  muldvdsfacm1  48006  lswn0  48075  fmtnoodd  48167  sqrtpwpw2p  48172  fmtnosqrt  48173  fmtnodvds  48178  fmtnorec3  48182  fmtnorec4  48183  2pwp1prm  48223  lighneallem3  48241  lighneallem4a  48242  lighneallem4  48244  nprmdvdsfacm1lem4  48257  ppivalnnprm  48259  ppivalnnnprmge6  48260  oexpnegALTV  48324  perfectALTV  48370  fpprmod  48374  fppr2odd  48378  fpprwppr  48386  fpprwpprb  48387  bgoldbtbndlem4  48455  bcpascm1  49009  altgsumbcALT  49011  pw2m1lepw2m1  49178  nnpw2even  49187  logbpw2m1  49225  nnpw2blenfzo  49239  nnpw2pmod  49241  nnpw2p  49244  nnolog2flm1  49248  dignn0fr  49259  dig2nn1st  49263  digexp  49265  dignn0flhalflem1  49273