Theorem nnm1nn0 11775

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 11495	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7014	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 11546	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	syl6eq 2845	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 902	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 866	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 11736	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 235	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 842   = wceq 1520   ∈ wcel 2079  (class class class)co 7007  0cc0 10372  1c1 10373   − cmin 10706  ℕcn 11475  ℕ₀cn0 11734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-om 7428  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-ltxr 10515  df-sub 10708  df-nn 11476  df-n0 11735

This theorem is referenced by:  elnn0nn  11776  nn0n0n1ge2  11799  nnaddm1cl  11877  fseq1m1p1  12821  elfznelfzo  12980  nn0ennn  13185  expm1t  13295  expgt1  13305  digit1  13436  bcn1  13511  bcm1k  13513  bcn2m1  13522  cshwidxn  13995  isercoll2  14847  iseralt  14863  binomlem  15005  incexc  15013  incexc2  15014  arisum  15036  arisum2  15037  pwdif  15044  mertenslem2  15062  risefallfac  15199  fallfacfwd  15211  0fallfac  15212  bpolydiflem  15229  ruclem12  15415  iddvdsexp  15454  dvdsfac  15497  oexpneg  15515  pwp1fsum  15563  bitsfzolem  15604  bitsf1  15616  phibnd  15925  phiprmpw  15930  prmdiv  15939  oddprm  15964  iserodd  15989  fldivp1  16050  prmpwdvds  16057  4sqlem12  16109  4sqlem19  16116  vdwapid1  16128  vdwlem1  16134  vdwlem3  16136  vdwlem5  16138  vdwlem6  16139  vdwlem9  16142  0ram  16173  ram0  16175  ramub1lem1  16179  ramub1lem2  16180  ramcl  16182  prmonn2  16192  1259lem5  16285  2503lem3  16289  4001lem4  16294  gsumwsubmcl  17802  gsumccat  17805  gsumwmhm  17809  sylow1lem1  18441  efgsrel  18575  efgredlem  18588  srgbinomlem4  18971  chfacfisf  21134  chfacfisfcpmat  21135  cpmadugsumlemF  21156  lebnumii  23241  ovolunlem1  23769  dvexp  24221  dgreq0  24526  dvply1  24544  vieta1lem2  24571  aaliou3lem8  24605  dvtaylp  24629  taylthlem1  24632  pserdvlem2  24687  pserdv2  24689  abelthlem6  24695  logtayl  24912  logtayl2  24914  cxpeq  25007  leibpilem1OLD  25188  gamfac  25314  wilthlem1  25315  wilthlem2  25316  wilthlem3  25317  wilth  25318  wilthimp  25319  ftalem1  25320  basellem5  25332  1sgm2ppw  25446  chtublem  25457  perfect1  25474  perfect  25477  bcmono  25523  lgslem1  25543  lgsquadlem1  25626  lgsquad2lem2  25631  m1lgs  25634  selberg2lem  25796  logdivbnd  25802  pntrsumo1  25811  cusgrsize2inds  26906  cusgrrusgr  27034  pthdlem2  27224  crctcshwlkn0lem4  27266  wlkiswwlks2lem1  27322  wlkiswwlksupgr2  27330  clwwlkccatlem  27442  clwlkclwwlklem2a2  27446  clwwlknwwlksn  27491  clwwlkel  27500  clwwlkwwlksb  27508  wwlksubclwwlk  27512  freshmansdream  30468  fibp1  31232  plymulx0  31390  plymulx  31391  signstfvn  31412  signsvtn0  31413  subfacp1lem6  31996  erdszelem10  32011  erdsze2lem1  32014  erdsze2lem2  32015  cvmliftlem2  32097  bcprod  32523  poimirlem5  34374  poimirlem6  34375  poimirlem7  34376  poimirlem10  34379  poimirlem11  34380  poimirlem13  34382  poimirlem14  34383  poimirlem20  34389  poimirlem21  34390  poimirlem22  34391  poimirlem23  34392  poimirlem25  34394  poimirlem26  34395  poimirlem31  34400  fltnltalem  38721  irrapxlem1  38855  rmspecsqrtnq  38939  jm2.24nn  38992  jm2.17a  38993  acongeq  39016  jm2.18  39021  jm2.22  39028  jm2.23  39029  jm2.20nn  39030  jm2.27c  39040  bccm1k  40164  binomcxplemwb  40170  binomcxplemnotnn0  40178  dvsinexp  41690  dvxpaek  41720  dvnxpaek  41722  itgsinexplem1  41734  itgsinexp  41735  wallispilem5  41850  stirlinglem5  41859  fourierdlem48  41935  fourierdlem49  41936  fourierdlem52  41939  fourierdlem54  41941  fourierdlem103  41990  fourierdlem104  41991  etransclem1  42016  etransclem4  42019  etransclem8  42023  etransclem10  42025  etransclem14  42029  etransclem15  42030  etransclem17  42032  etransclem18  42033  etransclem19  42034  etransclem20  42035  etransclem21  42036  etransclem22  42037  etransclem23  42038  etransclem24  42039  etransclem27  42042  etransclem28  42043  etransclem32  42047  etransclem35  42050  etransclem37  42052  etransclem38  42053  etransclem41  42056  etransclem44  42059  etransclem45  42060  etransclem46  42061  etransclem47  42062  etransclem48  42063  lswn0  43040  fmtnoodd  43131  sqrtpwpw2p  43136  fmtnosqrt  43137  fmtnodvds  43142  fmtnorec3  43146  fmtnorec4  43147  2pwp1prm  43187  lighneallem3  43208  lighneallem4a  43209  lighneallem4  43211  oexpnegALTV  43278  perfectALTV  43324  fpprmod  43328  fppr2odd  43332  fpprwppr  43340  fpprwpprb  43341  bgoldbtbndlem4  43409  bcpascm1  43831  altgsumbcALT  43833  pw2m1lepw2m1  44010  nnpw2even  44024  logbpw2m1  44062  nnpw2blenfzo  44076  nnpw2pmod  44078  nnpw2p  44081  nnolog2flm1  44085  dignn0fr  44096  dig2nn1st  44100  digexp  44102  dignn0flhalflem1  44110