Theorem nnm1nn0 11211

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 10917	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 6556	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 10966	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	syl6eq 2660	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 538	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 402	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 11171	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 223	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  0cc0 9815  1c1 9816   − cmin 10145  ℕcn 10897  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-sub 10147  df-nn 10898  df-n0 11170

This theorem is referenced by:  elnn0nn  11212  nn0n0n1ge2  11235  nnaddm1cl  11311  fseq1m1p1  12284  elfznelfzo  12439  nn0ennn  12640  expm1t  12750  expgt1  12760  digit1  12860  bcn1  12962  bcm1k  12964  bcn2m1  12973  swrdccatwrd  13320  cshwidxn  13406  isercoll2  14247  iseralt  14263  binomlem  14400  incexc  14408  incexc2  14409  arisum  14431  arisum2  14432  mertenslem2  14456  risefallfac  14594  fallfacfwd  14606  0fallfac  14607  bpolydiflem  14624  ruclem12  14809  iddvdsexp  14843  dvdsfac  14886  oexpneg  14907  pwp1fsum  14952  bitsfzolem  14994  bitsf1  15006  phibnd  15314  phiprmpw  15319  prmdiv  15328  oddprm  15353  iserodd  15378  fldivp1  15439  prmpwdvds  15446  4sqlem12  15498  4sqlem19  15505  vdwapid1  15517  vdwlem1  15523  vdwlem3  15525  vdwlem5  15527  vdwlem6  15528  vdwlem9  15531  0ram  15562  ram0  15564  ramub1lem1  15568  ramub1lem2  15569  ramcl  15571  prmonn2  15581  1259lem5  15680  2503lem3  15684  4001lem4  15689  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  sylow1lem1  17836  efgsrel  17970  efgredlem  17983  srgbinomlem4  18366  chfacfisf  20478  chfacfisfcpmat  20479  cpmadugsumlemF  20500  lebnumii  22573  ovolunlem1  23072  dvexp  23522  dgreq0  23825  dvply1  23843  vieta1lem2  23870  aaliou3lem8  23904  dvtaylp  23928  taylthlem1  23931  pserdvlem2  23986  pserdv2  23988  abelthlem6  23994  logtayl  24206  logtayl2  24208  cxpeq  24298  leibpilem1  24467  gamfac  24593  wilthlem1  24594  wilthlem2  24595  wilthlem3  24596  wilth  24597  wilthimp  24598  ftalem1  24599  basellem5  24611  1sgm2ppw  24725  chtublem  24736  perfect1  24753  perfect  24756  bcmono  24802  lgslem1  24822  lgsquadlem1  24905  lgsquad2lem2  24910  m1lgs  24913  selberg2lem  25039  logdivbnd  25045  pntrsumo1  25054  cusgrasize2inds  26005  wlkiswwlk2lem1  26219  clwlkisclwwlklem2a2  26308  clwwlkel  26321  wwlksubclwwlk  26332  cusgraisrusgra  26465  eupares  26502  frghash2spot  26590  fibp1  29790  plymulx0  29950  plymulx  29951  signstfvn  29972  signsvtn0  29973  subfacp1lem6  30421  erdszelem10  30436  erdsze2lem1  30439  erdsze2lem2  30440  cvmliftlem2  30522  bcprod  30877  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem13  32592  poimirlem14  32593  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem25  32604  poimirlem26  32605  poimirlem31  32610  irrapxlem1  36404  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  jm2.24nn  36544  jm2.17a  36545  acongeq  36568  jm2.18  36573  jm2.22  36580  jm2.23  36581  jm2.20nn  36582  jm2.27c  36592  bccm1k  37563  binomcxplemwb  37569  binomcxplemnotnn0  37577  dvsinexp  38798  dvxpaek  38830  dvnxpaek  38832  itgsinexplem1  38845  itgsinexp  38846  wallispilem5  38962  stirlinglem5  38971  fourierdlem48  39047  fourierdlem49  39048  fourierdlem52  39051  fourierdlem54  39053  fourierdlem103  39102  fourierdlem104  39103  etransclem1  39128  etransclem4  39131  etransclem8  39135  etransclem10  39137  etransclem14  39141  etransclem15  39142  etransclem17  39144  etransclem18  39145  etransclem19  39146  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem23  39150  etransclem24  39151  etransclem27  39154  etransclem28  39155  etransclem32  39159  etransclem35  39162  etransclem37  39164  etransclem38  39165  etransclem41  39168  etransclem44  39171  etransclem45  39172  etransclem46  39173  etransclem47  39174  etransclem48  39175  fmtnoodd  39983  sqrtpwpw2p  39988  fmtnosqrt  39989  fmtnodvds  39994  fmtnorec3  39998  fmtnorec4  39999  pwdif  40039  2pwp1prm  40041  lighneallem3  40062  lighneallem4a  40063  lighneallem4  40065  oexpnegALTV  40126  perfectALTV  40166  bgoldbtbndlem4  40224  lswn0  40242  cusgrsize2inds  40669  cusgrrusgr  40781  pthdlem2  40974  crctcsh1wlkn0lem4  41016  1wlkiswwlks2lem1  41066  1wlkiswwlksupgr2  41074  clwlkclwwlklem2a2  41202  clwwlksel  41221  wwlksubclwwlks  41232  frgrhash2wsp  41497  bcpascm1  41922  altgsumbcALT  41924  pw2m1lepw2m1  42104  nnpw2even  42117  logbpw2m1  42159  nnpw2blenfzo  42173  nnpw2pmod  42175  nnpw2p  42178  nnolog2flm1  42182  dignn0fr  42193  dig2nn1st  42197  digexp  42199  dignn0flhalflem1  42207