Theorem nnm1nn0 12096

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 11816	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7198	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 11867	. . . . . 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 871	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12057	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1543   ∈ wcel 2112  (class class class)co 7191  0cc0 10694  1c1 10695   − cmin 11027  ℕcn 11795  ℕ₀cn0 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837  df-sub 11029  df-nn 11796  df-n0 12056

This theorem is referenced by:  elnn0nn  12097  nn0n0n1ge2  12122  nnaddm1cl  12199  fseq1m1p1  13152  elfznelfzo  13312  nn0ennn  13517  expm1t  13628  expgt1  13638  digit1  13769  bcn1  13844  bcm1k  13846  bcn2m1  13855  cshwidxn  14339  isercoll2  15197  iseralt  15213  binomlem  15356  incexc  15364  incexc2  15365  arisum  15387  arisum2  15388  pwdif  15395  mertenslem2  15412  risefallfac  15549  fallfacfwd  15561  0fallfac  15562  bpolydiflem  15579  ruclem12  15765  iddvdsexp  15804  dvdsfac  15850  oexpneg  15869  pwp1fsum  15915  bitsfzolem  15956  bitsf1  15968  phibnd  16287  phiprmpw  16292  prmdiv  16301  oddprm  16326  iserodd  16351  fldivp1  16413  prmpwdvds  16420  4sqlem12  16472  4sqlem19  16479  vdwapid1  16491  vdwlem1  16497  vdwlem3  16499  vdwlem5  16501  vdwlem6  16502  vdwlem9  16505  0ram  16536  ram0  16538  ramub1lem1  16542  ramub1lem2  16543  ramcl  16545  prmonn2  16555  1259lem5  16651  2503lem3  16655  4001lem4  16660  gsumwsubmcl  18217  gsumsgrpccat  18220  gsumccatOLD  18221  gsumwmhm  18226  sylow1lem1  18941  efgsrel  19078  efgredlem  19091  srgbinomlem4  19512  chfacfisf  21705  chfacfisfcpmat  21706  cpmadugsumlemF  21727  lebnumii  23817  ovolunlem1  24348  dvexp  24804  dgreq0  25113  dvply1  25131  vieta1lem2  25158  aaliou3lem8  25192  dvtaylp  25216  taylthlem1  25219  pserdvlem2  25274  pserdv2  25276  abelthlem6  25282  logtayl  25502  logtayl2  25504  cxpeq  25597  gamfac  25903  wilthlem1  25904  wilthlem2  25905  wilthlem3  25906  wilth  25907  wilthimp  25908  ftalem1  25909  basellem5  25921  1sgm2ppw  26035  chtublem  26046  perfect1  26063  perfect  26066  bcmono  26112  lgslem1  26132  lgsquadlem1  26215  lgsquad2lem2  26220  m1lgs  26223  selberg2lem  26385  logdivbnd  26391  pntrsumo1  26400  cusgrsize2inds  27495  cusgrrusgr  27623  pthdlem2  27809  crctcshwlkn0lem4  27851  wlkiswwlks2lem1  27907  wlkiswwlksupgr2  27915  clwwlkccatlem  28026  clwlkclwwlklem2a2  28030  clwwlknwwlksn  28075  clwwlkel  28083  clwwlkwwlksb  28091  wwlksubclwwlk  28095  freshmansdream  31157  fibp1  32034  plymulx0  32192  plymulx  32193  signstfvn  32214  signsvtn0  32215  subfacp1lem6  32814  erdszelem10  32829  erdsze2lem1  32832  erdsze2lem2  32833  cvmliftlem2  32915  bcprod  33373  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem10  35473  poimirlem11  35474  poimirlem13  35476  poimirlem14  35477  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem25  35488  poimirlem26  35489  poimirlem31  35494  lcmfunnnd  39703  lcmineqlem2  39721  lcmineqlem3  39722  lcmineqlem8  39727  lcmineqlem10  39729  lcmineqlem12  39731  dvrelogpow2b  39758  sticksstones12a  39782  sticksstones16  39787  fltnltalem  40143  irrapxlem1  40288  rmspecsqrtnq  40372  jm2.24nn  40425  jm2.17a  40426  acongeq  40449  jm2.18  40454  jm2.22  40461  jm2.23  40462  jm2.20nn  40463  jm2.27c  40473  bccm1k  41574  binomcxplemwb  41580  binomcxplemnotnn0  41588  dvsinexp  43070  dvxpaek  43099  dvnxpaek  43101  itgsinexplem1  43113  itgsinexp  43114  wallispilem5  43228  stirlinglem5  43237  fourierdlem48  43313  fourierdlem49  43314  fourierdlem52  43317  fourierdlem54  43319  fourierdlem103  43368  fourierdlem104  43369  etransclem1  43394  etransclem4  43397  etransclem8  43401  etransclem10  43403  etransclem14  43407  etransclem15  43408  etransclem17  43410  etransclem18  43411  etransclem19  43412  etransclem20  43413  etransclem21  43414  etransclem22  43415  etransclem23  43416  etransclem24  43417  etransclem27  43420  etransclem28  43421  etransclem32  43425  etransclem35  43428  etransclem37  43430  etransclem38  43431  etransclem41  43434  etransclem44  43437  etransclem45  43438  etransclem46  43439  etransclem47  43440  etransclem48  43441  lswn0  44512  fmtnoodd  44601  sqrtpwpw2p  44606  fmtnosqrt  44607  fmtnodvds  44612  fmtnorec3  44616  fmtnorec4  44617  2pwp1prm  44657  lighneallem3  44675  lighneallem4a  44676  lighneallem4  44678  oexpnegALTV  44745  perfectALTV  44791  fpprmod  44795  fppr2odd  44799  fpprwppr  44807  fpprwpprb  44808  bgoldbtbndlem4  44876  bcpascm1  45303  altgsumbcALT  45305  pw2m1lepw2m1  45477  nnpw2even  45491  logbpw2m1  45529  nnpw2blenfzo  45543  nnpw2pmod  45545  nnpw2p  45548  nnolog2flm1  45552  dignn0fr  45563  dig2nn1st  45567  digexp  45569  dignn0flhalflem1  45577