Theorem nnm1nn0 12594

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 12314	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7455	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12365	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2796	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 908	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 870	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12555	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  0cc0 11184  1c1 11185   − cmin 11520  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522  df-nn 12294  df-n0 12554

This theorem is referenced by:  elnn0nn  12595  nn0n0n1ge2  12620  nnaddm1cl  12700  fseq1m1p1  13659  elfznelfzo  13822  nn0ennn  14030  expm1t  14141  expgt1  14151  digit1  14286  bcn1  14362  bcm1k  14364  bcn2m1  14373  cshwidxn  14857  isercoll2  15717  iseralt  15733  binomlem  15877  incexc  15885  incexc2  15886  arisum  15908  arisum2  15909  pwdif  15916  mertenslem2  15933  risefallfac  16072  fallfacfwd  16084  0fallfac  16085  bpolydiflem  16102  ruclem12  16289  iddvdsexp  16328  dvdsfac  16374  oexpneg  16393  pwp1fsum  16439  bitsfzolem  16480  bitsf1  16492  phibnd  16818  phiprmpw  16823  prmdiv  16832  oddprm  16857  iserodd  16882  fldivp1  16944  prmpwdvds  16951  4sqlem12  17003  4sqlem19  17010  vdwapid1  17022  vdwlem1  17028  vdwlem3  17030  vdwlem5  17032  vdwlem6  17033  vdwlem9  17036  0ram  17067  ram0  17069  ramub1lem1  17073  ramub1lem2  17074  ramcl  17076  prmonn2  17086  1259lem5  17182  2503lem3  17186  4001lem4  17191  gsumwsubmcl  18872  gsumsgrpccat  18875  gsumwmhm  18880  finodsubmsubg  19609  sylow1lem1  19640  efgsrel  19776  efgredlem  19789  srgbinomlem4  20256  freshmansdream  21616  chfacfisf  22881  chfacfisfcpmat  22882  cpmadugsumlemF  22903  lebnumii  25017  ovolunlem1  25551  dvexp  26011  dgreq0  26325  dvply1  26343  vieta1lem2  26371  aaliou3lem8  26405  dvtaylp  26430  taylthlem1  26433  pserdvlem2  26490  pserdv2  26492  abelthlem6  26498  logtayl  26720  logtayl2  26722  cxpeq  26818  gamfac  27128  wilthlem1  27129  wilthlem2  27130  wilthlem3  27131  wilth  27132  wilthimp  27133  ftalem1  27134  basellem5  27146  1sgm2ppw  27262  chtublem  27273  perfect1  27290  perfect  27293  bcmono  27339  lgslem1  27359  lgsquadlem1  27442  lgsquad2lem2  27447  m1lgs  27450  selberg2lem  27612  logdivbnd  27618  pntrsumo1  27627  cusgrsize2inds  29489  cusgrrusgr  29617  pthdlem2  29804  crctcshwlkn0lem4  29846  wlkiswwlks2lem1  29902  wlkiswwlksupgr2  29910  clwwlkccatlem  30021  clwlkclwwlklem2a2  30025  clwwlknwwlksn  30070  clwwlkel  30078  clwwlkwwlksb  30086  wwlksubclwwlk  30090  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  fibp1  34366  plymulx0  34524  plymulx  34525  signstfvn  34546  signsvtn0  34547  subfacp1lem6  35153  erdszelem10  35168  erdsze2lem1  35171  erdsze2lem2  35172  cvmliftlem2  35254  bcprod  35700  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem13  37593  poimirlem14  37594  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem25  37605  poimirlem26  37606  poimirlem31  37611  lcmfunnnd  41969  lcmineqlem2  41987  lcmineqlem3  41988  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem12  41997  dvrelogpow2b  42025  primrootsunit1  42054  sticksstones12a  42114  sticksstones16  42119  sticksstones22  42125  fltnltalem  42617  irrapxlem1  42778  rmspecsqrtnq  42862  jm2.24nn  42916  jm2.17a  42917  acongeq  42940  jm2.18  42945  jm2.22  42952  jm2.23  42953  jm2.20nn  42954  jm2.27c  42964  bccm1k  44311  binomcxplemwb  44317  binomcxplemnotnn0  44325  dvsinexp  45832  dvxpaek  45861  dvnxpaek  45863  itgsinexplem1  45875  itgsinexp  45876  wallispilem5  45990  stirlinglem5  45999  fourierdlem48  46075  fourierdlem49  46076  fourierdlem52  46079  fourierdlem54  46081  fourierdlem103  46130  fourierdlem104  46131  etransclem1  46156  etransclem4  46159  etransclem8  46163  etransclem10  46165  etransclem14  46169  etransclem15  46170  etransclem17  46172  etransclem18  46173  etransclem19  46174  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem27  46182  etransclem28  46183  etransclem32  46187  etransclem35  46190  etransclem37  46192  etransclem38  46193  etransclem41  46196  etransclem44  46199  etransclem45  46200  etransclem46  46201  etransclem47  46202  etransclem48  46203  lswn0  47318  fmtnoodd  47407  sqrtpwpw2p  47412  fmtnosqrt  47413  fmtnodvds  47418  fmtnorec3  47422  fmtnorec4  47423  2pwp1prm  47463  lighneallem3  47481  lighneallem4a  47482  lighneallem4  47484  oexpnegALTV  47551  perfectALTV  47597  fpprmod  47601  fppr2odd  47605  fpprwppr  47613  fpprwpprb  47614  bgoldbtbndlem4  47682  bcpascm1  48076  altgsumbcALT  48078  pw2m1lepw2m1  48249  nnpw2even  48263  logbpw2m1  48301  nnpw2blenfzo  48315  nnpw2pmod  48317  nnpw2p  48320  nnolog2flm1  48324  dignn0fr  48335  dig2nn1st  48339  digexp  48341  dignn0flhalflem1  48349