Theorem nnm1nn0 11941

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 11661	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7165	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 11712	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	syl6eq 2874	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 906	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 867	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 11902	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 236	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  0cc0 10539  1c1 10540   − cmin 10872  ℕcn 11640  ℕ₀cn0 11900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682  df-sub 10874  df-nn 11641  df-n0 11901

This theorem is referenced by:  elnn0nn  11942  nn0n0n1ge2  11965  nnaddm1cl  12042  fseq1m1p1  12985  elfznelfzo  13145  nn0ennn  13350  expm1t  13460  expgt1  13470  digit1  13601  bcn1  13676  bcm1k  13678  bcn2m1  13687  cshwidxn  14173  isercoll2  15027  iseralt  15043  binomlem  15186  incexc  15194  incexc2  15195  arisum  15217  arisum2  15218  pwdif  15225  mertenslem2  15243  risefallfac  15380  fallfacfwd  15392  0fallfac  15393  bpolydiflem  15410  ruclem12  15596  iddvdsexp  15635  dvdsfac  15678  oexpneg  15696  pwp1fsum  15744  bitsfzolem  15785  bitsf1  15797  phibnd  16110  phiprmpw  16115  prmdiv  16124  oddprm  16149  iserodd  16174  fldivp1  16235  prmpwdvds  16242  4sqlem12  16294  4sqlem19  16301  vdwapid1  16313  vdwlem1  16319  vdwlem3  16321  vdwlem5  16323  vdwlem6  16324  vdwlem9  16327  0ram  16358  ram0  16360  ramub1lem1  16364  ramub1lem2  16365  ramcl  16367  prmonn2  16377  1259lem5  16470  2503lem3  16474  4001lem4  16479  gsumwsubmcl  18003  gsumsgrpccat  18006  gsumccatOLD  18007  gsumwmhm  18012  sylow1lem1  18725  efgsrel  18862  efgredlem  18875  srgbinomlem4  19295  chfacfisf  21464  chfacfisfcpmat  21465  cpmadugsumlemF  21486  lebnumii  23572  ovolunlem1  24100  dvexp  24552  dgreq0  24857  dvply1  24875  vieta1lem2  24902  aaliou3lem8  24936  dvtaylp  24960  taylthlem1  24963  pserdvlem2  25018  pserdv2  25020  abelthlem6  25026  logtayl  25245  logtayl2  25247  cxpeq  25340  gamfac  25646  wilthlem1  25647  wilthlem2  25648  wilthlem3  25649  wilth  25650  wilthimp  25651  ftalem1  25652  basellem5  25664  1sgm2ppw  25778  chtublem  25789  perfect1  25806  perfect  25809  bcmono  25855  lgslem1  25875  lgsquadlem1  25958  lgsquad2lem2  25963  m1lgs  25966  selberg2lem  26128  logdivbnd  26134  pntrsumo1  26143  cusgrsize2inds  27237  cusgrrusgr  27365  pthdlem2  27551  crctcshwlkn0lem4  27593  wlkiswwlks2lem1  27649  wlkiswwlksupgr2  27657  clwwlkccatlem  27769  clwlkclwwlklem2a2  27773  clwwlknwwlksn  27818  clwwlkel  27827  clwwlkwwlksb  27835  wwlksubclwwlk  27839  freshmansdream  30861  fibp1  31661  plymulx0  31819  plymulx  31820  signstfvn  31841  signsvtn0  31842  subfacp1lem6  32434  erdszelem10  32449  erdsze2lem1  32452  erdsze2lem2  32453  cvmliftlem2  32535  bcprod  32972  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem10  34904  poimirlem11  34905  poimirlem13  34907  poimirlem14  34908  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem25  34919  poimirlem26  34920  poimirlem31  34925  fltnltalem  39281  irrapxlem1  39426  rmspecsqrtnq  39510  jm2.24nn  39563  jm2.17a  39564  acongeq  39587  jm2.18  39592  jm2.22  39599  jm2.23  39600  jm2.20nn  39601  jm2.27c  39611  bccm1k  40681  binomcxplemwb  40687  binomcxplemnotnn0  40695  dvsinexp  42202  dvxpaek  42232  dvnxpaek  42234  itgsinexplem1  42246  itgsinexp  42247  wallispilem5  42361  stirlinglem5  42370  fourierdlem48  42446  fourierdlem49  42447  fourierdlem52  42450  fourierdlem54  42452  fourierdlem103  42501  fourierdlem104  42502  etransclem1  42527  etransclem4  42530  etransclem8  42534  etransclem10  42536  etransclem14  42540  etransclem15  42541  etransclem17  42543  etransclem18  42544  etransclem19  42545  etransclem20  42546  etransclem21  42547  etransclem22  42548  etransclem23  42549  etransclem24  42550  etransclem27  42553  etransclem28  42554  etransclem32  42558  etransclem35  42561  etransclem37  42563  etransclem38  42564  etransclem41  42567  etransclem44  42570  etransclem45  42571  etransclem46  42572  etransclem47  42573  etransclem48  42574  lswn0  43611  fmtnoodd  43702  sqrtpwpw2p  43707  fmtnosqrt  43708  fmtnodvds  43713  fmtnorec3  43717  fmtnorec4  43718  2pwp1prm  43758  lighneallem3  43779  lighneallem4a  43780  lighneallem4  43782  oexpnegALTV  43849  perfectALTV  43895  fpprmod  43899  fppr2odd  43903  fpprwppr  43911  fpprwpprb  43912  bgoldbtbndlem4  43980  bcpascm1  44406  altgsumbcALT  44408  pw2m1lepw2m1  44582  nnpw2even  44596  logbpw2m1  44634  nnpw2blenfzo  44648  nnpw2pmod  44650  nnpw2p  44653  nnolog2flm1  44657  dignn0fr  44668  dig2nn1st  44672  digexp  44674  dignn0flhalflem1  44682