Theorem nnm1nn0 12542

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 12261	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7412	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12312	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2786	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 909	. . . 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 12503	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  0cc0 11129  1c1 11130   − cmin 11466  ℕcn 12240  ℕ₀cn0 12501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-ltxr 11274  df-sub 11468  df-nn 12241  df-n0 12502

This theorem is referenced by:  elnn0nn  12543  nn0n0n1ge2  12569  nnaddm1cl  12650  fseq1m1p1  13616  elfznelfzo  13788  nn0ennn  13997  expm1t  14108  expgt1  14118  digit1  14255  bcn1  14331  bcm1k  14333  bcn2m1  14342  cshwidxn  14827  isercoll2  15685  iseralt  15701  binomlem  15845  incexc  15853  incexc2  15854  arisum  15876  arisum2  15877  pwdif  15884  mertenslem2  15901  risefallfac  16040  fallfacfwd  16052  0fallfac  16053  bpolydiflem  16070  ruclem12  16259  iddvdsexp  16299  dvdsfac  16345  oexpneg  16364  pwp1fsum  16410  bitsfzolem  16453  bitsf1  16465  phibnd  16790  phiprmpw  16795  prmdiv  16804  oddprm  16830  iserodd  16855  fldivp1  16917  prmpwdvds  16924  4sqlem12  16976  4sqlem19  16983  vdwapid1  16995  vdwlem1  17001  vdwlem3  17003  vdwlem5  17005  vdwlem6  17006  vdwlem9  17009  0ram  17040  ram0  17042  ramub1lem1  17046  ramub1lem2  17047  ramcl  17049  prmonn2  17059  1259lem5  17154  2503lem3  17158  4001lem4  17163  gsumwsubmcl  18815  gsumsgrpccat  18818  gsumwmhm  18823  finodsubmsubg  19548  sylow1lem1  19579  efgsrel  19715  efgredlem  19728  srgbinomlem4  20189  freshmansdream  21535  psdpw  22108  chfacfisf  22792  chfacfisfcpmat  22793  cpmadugsumlemF  22814  lebnumii  24916  ovolunlem1  25450  dvexp  25909  dgreq0  26223  dvply1  26243  vieta1lem2  26271  aaliou3lem8  26305  dvtaylp  26330  taylthlem1  26333  pserdvlem2  26390  pserdv2  26392  abelthlem6  26398  logtayl  26621  logtayl2  26623  cxpeq  26719  gamfac  27029  wilthlem1  27030  wilthlem2  27031  wilthlem3  27032  wilth  27033  wilthimp  27034  ftalem1  27035  basellem5  27047  1sgm2ppw  27163  chtublem  27174  perfect1  27191  perfect  27194  bcmono  27240  lgslem1  27260  lgsquadlem1  27343  lgsquad2lem2  27348  m1lgs  27351  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  cusgrsize2inds  29433  cusgrrusgr  29561  pthdlem2  29750  crctcshwlkn0lem4  29795  wlkiswwlks2lem1  29851  wlkiswwlksupgr2  29859  clwwlkccatlem  29970  clwlkclwwlklem2a2  29974  clwwlknwwlksn  30019  clwwlkel  30027  clwwlkwwlksb  30035  wwlksubclwwlk  30039  oexpled  32826  1arithidomlem1  33550  1arithidomlem2  33551  1arithidom  33552  fibp1  34433  plymulx0  34579  plymulx  34580  signstfvn  34601  signsvtn0  34602  subfacp1lem6  35207  erdszelem10  35222  erdsze2lem1  35225  erdsze2lem2  35226  cvmliftlem2  35308  bcprod  35755  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem10  37654  poimirlem11  37655  poimirlem13  37657  poimirlem14  37658  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem25  37669  poimirlem26  37670  poimirlem31  37675  lcmfunnnd  42025  lcmineqlem2  42043  lcmineqlem3  42044  lcmineqlem8  42049  lcmineqlem10  42051  lcmineqlem12  42053  dvrelogpow2b  42081  primrootsunit1  42110  sticksstones12a  42170  sticksstones16  42175  sticksstones22  42181  fltnltalem  42685  irrapxlem1  42845  rmspecsqrtnq  42929  jm2.24nn  42983  jm2.17a  42984  acongeq  43007  jm2.18  43012  jm2.22  43019  jm2.23  43020  jm2.20nn  43021  jm2.27c  43031  bccm1k  44366  binomcxplemwb  44372  binomcxplemnotnn0  44380  dvsinexp  45940  dvxpaek  45969  dvnxpaek  45971  itgsinexplem1  45983  itgsinexp  45984  wallispilem5  46098  stirlinglem5  46107  fourierdlem48  46183  fourierdlem49  46184  fourierdlem52  46187  fourierdlem54  46189  fourierdlem103  46238  fourierdlem104  46239  etransclem1  46264  etransclem4  46267  etransclem8  46271  etransclem10  46273  etransclem14  46277  etransclem15  46278  etransclem17  46280  etransclem18  46281  etransclem19  46282  etransclem20  46283  etransclem21  46284  etransclem22  46285  etransclem23  46286  etransclem24  46287  etransclem27  46290  etransclem28  46291  etransclem32  46295  etransclem35  46298  etransclem37  46300  etransclem38  46301  etransclem41  46304  etransclem44  46307  etransclem45  46308  etransclem46  46309  etransclem47  46310  etransclem48  46311  lswn0  47458  fmtnoodd  47547  sqrtpwpw2p  47552  fmtnosqrt  47553  fmtnodvds  47558  fmtnorec3  47562  fmtnorec4  47563  2pwp1prm  47603  lighneallem3  47621  lighneallem4a  47622  lighneallem4  47624  oexpnegALTV  47691  perfectALTV  47737  fpprmod  47741  fppr2odd  47745  fpprwppr  47753  fpprwpprb  47754  bgoldbtbndlem4  47822  bcpascm1  48326  altgsumbcALT  48328  pw2m1lepw2m1  48496  nnpw2even  48509  logbpw2m1  48547  nnpw2blenfzo  48561  nnpw2pmod  48563  nnpw2p  48566  nnolog2flm1  48570  dignn0fr  48581  dig2nn1st  48585  digexp  48587  dignn0flhalflem1  48595