Theorem nnm1nn0 12569

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 12278	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7420	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12337	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2811	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 923	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 18	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 885	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12530	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  0cc0 11124  1c1 11125   − cmin 11465  ℕcn 12257  ℕ₀cn0 12528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  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 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11467  df-nn 12258  df-n0 12529

This theorem is used by:  elnn0nn  12570  nn0n0n1ge2  12596  nnaddm1cl  12678  fseq1m1p1  13654  elfznelfzo  13829  nn0ennn  14043  expm1t  14154  expgt1  14164  digit1  14301  bcn1  14377  bcm1k  14379  bcn2m1  14388  cshwidxn  14880  isercoll2  15756  iseralt  15772  binomlem  15918  incexc  15926  incexc2  15927  arisum  15949  arisum2  15950  pwdif  15957  mertenslem2  15974  risefallfac  16111  fallfacfwd  16122  0fallfac  16123  bpolydiflem  16140  ruclem12  16329  iddvdsexp  16369  dvdsfac  16416  oexpneg  16435  pwp1fsum  16481  bitsfzolem  16524  bitsf1  16536  phibnd  16862  phiprmpw  16867  prmdiv  16876  oddprm  16902  iserodd  16927  fldivp1  16989  prmpwdvds  16996  4sqlem12  17048  4sqlem19  17055  vdwapid1  17067  vdwlem1  17073  vdwlem3  17075  vdwlem5  17077  vdwlem6  17078  vdwlem9  17081  0ram  17112  ram0  17114  ramub1lem1  17118  ramub1lem2  17119  ramcl  17121  prmonn2  17131  1259lem5  17227  2503lem3  17231  4001lem4  17236  chnrev  18715  gsumwsubmcl  18946  gsumsgrpccat  18949  gsumwmhm  18954  finodsubmsubg  19694  sylow1lem1  19725  efgsrel  19861  efgredlem  19874  srgbinomlem4  20368  freshmansdream  21787  psdpw  22398  chfacfisf  23079  chfacfisfcpmat  23080  cpmadugsumlemF  23101  lebnumii  25194  ovolunlem1  25725  dvexp  26180  dgreq0  26491  plyn0mulidp  26511  plymulidp  26512  dvply1  26514  vieta1lem2  26543  aaliou3lem8  26581  dvtaylp  26606  taylthlem1  26609  pserdvlem2  26664  pserdv2  26666  abelthlem6  26672  logtayl  26897  logtayl2  26899  cxpeq  26994  gamfac  27303  wilthlem1  27304  wilthlem2  27305  wilthlem3  27306  wilth  27307  wilthimp  27308  ftalem1  27309  basellem5  27321  1sgm2ppw  27436  chtublem  27447  perfect1  27464  perfect  27467  bcmono  27513  lgslem1  27533  lgsquadlem1  27616  lgsquad2lem2  27621  m1lgs  27624  selberg2lem  27786  logdivbnd  27792  pntrsumo1  27801  cusgrsize2inds  29913  cusgrrusgr  30041  pthdlem2  30233  crctcshwlkn0lem4  30281  wlkiswwlks2lem1  30337  wlkiswwlksupgr2  30345  clwwlkccatlem  30459  clwlkclwwlklem2a2  30463  clwwlknwwlksn  30508  clwwlkel  30516  clwwlkwwlksb  30524  wwlksubclwwlk  30528  oexpled  33306  1arithidomlem1  33945  1arithidomlem2  33946  1arithidom  33947  esplyind  34085  fibp1  34912  signstfvn  35077  signsvtn0  35078  subfacp1lem6  35764  erdszelem10  35779  erdsze2lem1  35782  erdsze2lem2  35783  cvmliftlem2  35865  bcprod  36317  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  poimirlem13  38382  poimirlem14  38383  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem23  38392  poimirlem25  38394  poimirlem26  38395  poimirlem31  38400  lcmfunnnd  42878  lcmineqlem2  42896  lcmineqlem3  42897  lcmineqlem8  42902  lcmineqlem10  42904  lcmineqlem12  42906  dvrelogpow2b  42934  primrootsunit1  42963  sticksstones12a  43023  sticksstones16  43028  sticksstones22  43034  fltnltalem  43508  irrapxlem1  43663  rmspecsqrtnq  43747  jm2.24nn  43800  jm2.17a  43801  acongeq  43824  jm2.18  43829  jm2.22  43836  jm2.23  43837  jm2.20nn  43838  jm2.27c  43848  bccm1k  45166  binomcxplemwb  45172  binomcxplemnotnn0  45180  dvsinexp  46739  dvxpaek  46768  dvnxpaek  46770  itgsinexplem1  46782  itgsinexp  46783  wallispilem5  46897  stirlinglem5  46906  fourierdlem48  46982  fourierdlem49  46983  fourierdlem52  46986  fourierdlem54  46988  fourierdlem103  47037  fourierdlem104  47038  etransclem1  47063  etransclem4  47066  etransclem8  47070  etransclem10  47072  etransclem14  47076  etransclem15  47077  etransclem17  47079  etransclem18  47080  etransclem19  47081  etransclem20  47082  etransclem21  47083  etransclem22  47084  etransclem23  47085  etransclem24  47086  etransclem27  47089  etransclem28  47090  etransclem32  47094  etransclem35  47097  etransclem37  47099  etransclem38  47100  etransclem41  47103  etransclem44  47106  etransclem45  47107  etransclem46  47108  etransclem47  47109  etransclem48  47110  muldvdsfacgt  48274  muldvdsfacm1  48275  lswn0  48344  fmtnoodd  48436  sqrtpwpw2p  48441  fmtnosqrt  48442  fmtnodvds  48447  fmtnorec3  48451  fmtnorec4  48452  2pwp1prm  48492  lighneallem3  48510  lighneallem4a  48511  lighneallem4  48513  nprmdvdsfacm1lem4  48526  ppivalnnprm  48528  ppivalnnnprmge6  48529  oexpnegALTV  48593  perfectALTV  48639  fpprmod  48643  fppr2odd  48647  fpprwppr  48655  fpprwpprb  48656  bgoldbtbndlem4  48724  bcpascm1  49281  altgsumbcALT  49283  pw2m1lepw2m1  49450  nnpw2even  49459  logbpw2m1  49497  nnpw2blenfzo  49511  nnpw2pmod  49513  nnpw2p  49516  nnolog2flm1  49520  dignn0fr  49531  dig2nn1st  49535  digexp  49537  dignn0flhalflem1  49545