Theorem nnm1nn0 12433

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 12157	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7362	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12208	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2784	. . . . 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 12394	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 234	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  0cc0 11017  1c1 11018   − cmin 11355  ℕcn 12136  ℕ₀cn0 12392

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162  df-sub 11357  df-nn 12137  df-n0 12393

This theorem is referenced by:  elnn0nn  12434  nn0n0n1ge2  12460  nnaddm1cl  12540  fseq1m1p1  13506  elfznelfzo  13680  nn0ennn  13893  expm1t  14004  expgt1  14014  digit1  14151  bcn1  14227  bcm1k  14229  bcn2m1  14238  cshwidxn  14723  isercoll2  15583  iseralt  15599  binomlem  15743  incexc  15751  incexc2  15752  arisum  15774  arisum2  15775  pwdif  15782  mertenslem2  15799  risefallfac  15938  fallfacfwd  15950  0fallfac  15951  bpolydiflem  15968  ruclem12  16157  iddvdsexp  16197  dvdsfac  16244  oexpneg  16263  pwp1fsum  16309  bitsfzolem  16352  bitsf1  16364  phibnd  16689  phiprmpw  16694  prmdiv  16703  oddprm  16729  iserodd  16754  fldivp1  16816  prmpwdvds  16823  4sqlem12  16875  4sqlem19  16882  vdwapid1  16894  vdwlem1  16900  vdwlem3  16902  vdwlem5  16904  vdwlem6  16905  vdwlem9  16908  0ram  16939  ram0  16941  ramub1lem1  16945  ramub1lem2  16946  ramcl  16948  prmonn2  16958  1259lem5  17053  2503lem3  17057  4001lem4  17062  chnrev  18541  gsumwsubmcl  18753  gsumsgrpccat  18756  gsumwmhm  18761  finodsubmsubg  19487  sylow1lem1  19518  efgsrel  19654  efgredlem  19667  srgbinomlem4  20155  freshmansdream  21520  psdpw  22104  chfacfisf  22789  chfacfisfcpmat  22790  cpmadugsumlemF  22811  lebnumii  24912  ovolunlem1  25445  dvexp  25904  dgreq0  26218  dvply1  26238  vieta1lem2  26266  aaliou3lem8  26300  dvtaylp  26325  taylthlem1  26328  pserdvlem2  26385  pserdv2  26387  abelthlem6  26393  logtayl  26616  logtayl2  26618  cxpeq  26714  gamfac  27024  wilthlem1  27025  wilthlem2  27026  wilthlem3  27027  wilth  27028  wilthimp  27029  ftalem1  27030  basellem5  27042  1sgm2ppw  27158  chtublem  27169  perfect1  27186  perfect  27189  bcmono  27235  lgslem1  27255  lgsquadlem1  27338  lgsquad2lem2  27343  m1lgs  27346  selberg2lem  27508  logdivbnd  27514  pntrsumo1  27523  cusgrsize2inds  29453  cusgrrusgr  29581  pthdlem2  29767  crctcshwlkn0lem4  29812  wlkiswwlks2lem1  29868  wlkiswwlksupgr2  29876  clwwlkccatlem  29990  clwlkclwwlklem2a2  29994  clwwlknwwlksn  30039  clwwlkel  30047  clwwlkwwlksb  30055  wwlksubclwwlk  30059  oexpled  32856  1arithidomlem1  33544  1arithidomlem2  33545  1arithidom  33546  esplyind  33659  fibp1  34486  plymulx0  34632  plymulx  34633  signstfvn  34654  signsvtn0  34655  subfacp1lem6  35301  erdszelem10  35316  erdsze2lem1  35319  erdsze2lem2  35320  cvmliftlem2  35402  bcprod  35854  poimirlem5  37738  poimirlem6  37739  poimirlem7  37740  poimirlem10  37743  poimirlem11  37744  poimirlem13  37746  poimirlem14  37747  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem23  37756  poimirlem25  37758  poimirlem26  37759  poimirlem31  37764  lcmfunnnd  42178  lcmineqlem2  42196  lcmineqlem3  42197  lcmineqlem8  42202  lcmineqlem10  42204  lcmineqlem12  42206  dvrelogpow2b  42234  primrootsunit1  42263  sticksstones12a  42323  sticksstones16  42328  sticksstones22  42334  fltnltalem  42820  irrapxlem1  42979  rmspecsqrtnq  43063  jm2.24nn  43116  jm2.17a  43117  acongeq  43140  jm2.18  43145  jm2.22  43152  jm2.23  43153  jm2.20nn  43154  jm2.27c  43164  bccm1k  44499  binomcxplemwb  44505  binomcxplemnotnn0  44513  dvsinexp  46071  dvxpaek  46100  dvnxpaek  46102  itgsinexplem1  46114  itgsinexp  46115  wallispilem5  46229  stirlinglem5  46238  fourierdlem48  46314  fourierdlem49  46315  fourierdlem52  46318  fourierdlem54  46320  fourierdlem103  46369  fourierdlem104  46370  etransclem1  46395  etransclem4  46398  etransclem8  46402  etransclem10  46404  etransclem14  46408  etransclem15  46409  etransclem17  46411  etransclem18  46412  etransclem19  46413  etransclem20  46414  etransclem21  46415  etransclem22  46416  etransclem23  46417  etransclem24  46418  etransclem27  46421  etransclem28  46422  etransclem32  46426  etransclem35  46429  etransclem37  46431  etransclem38  46432  etransclem41  46435  etransclem44  46438  etransclem45  46439  etransclem46  46440  etransclem47  46441  etransclem48  46442  lswn0  47606  fmtnoodd  47695  sqrtpwpw2p  47700  fmtnosqrt  47701  fmtnodvds  47706  fmtnorec3  47710  fmtnorec4  47711  2pwp1prm  47751  lighneallem3  47769  lighneallem4a  47770  lighneallem4  47772  oexpnegALTV  47839  perfectALTV  47885  fpprmod  47889  fppr2odd  47893  fpprwppr  47901  fpprwpprb  47902  bgoldbtbndlem4  47970  bcpascm1  48513  altgsumbcALT  48515  pw2m1lepw2m1  48682  nnpw2even  48691  logbpw2m1  48729  nnpw2blenfzo  48743  nnpw2pmod  48745  nnpw2p  48748  nnolog2flm1  48752  dignn0fr  48763  dig2nn1st  48767  digexp  48769  dignn0flhalflem1  48777