Theorem nnm1nn0 12685

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 12394	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7456	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12453	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2814	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 923	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 18	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 885	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12646	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2147  (class class class)co 7449  0cc0 11237  1c1 11238   − cmin 11578  ℕcn 12373  ℕ₀cn0 12644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-2nd 8034  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-er 8753  df-en 9010  df-dom 9011  df-sdom 9012  df-pnf 11382  df-mnf 11383  df-ltxr 11385  df-sub 11580  df-nn 12374  df-n0 12645

This theorem is used by:  elnn0nn  12686  nn0n0n1ge2  12712  nnaddm1cl  12794  fseq1m1p1  13771  elfznelfzo  13946  nn0ennn  14160  expm1t  14271  expgt1  14281  digit1  14420  bcn1  14496  bcm1k  14498  bcn2m1  14507  cshwidxn  15000  isercoll2  15877  iseralt  15893  binomlem  16039  incexc  16047  incexc2  16048  arisum  16070  arisum2  16071  pwdif  16078  mertenslem2  16095  risefallfac  16232  fallfacfwd  16243  0fallfac  16244  bpolydiflem  16261  ruclem12  16450  iddvdsexp  16490  dvdsfac  16537  oexpneg  16556  pwp1fsum  16602  bitsfzolem  16645  bitsf1  16657  phibnd  16989  phiprmpw  16994  prmdiv  17003  oddprm  17029  iserodd  17054  fldivp1  17116  prmpwdvds  17123  4sqlem12  17175  4sqlem19  17182  vdwapid1  17194  vdwlem1  17200  vdwlem3  17202  vdwlem5  17204  vdwlem6  17205  vdwlem9  17208  0ram  17239  ram0  17241  ramub1lem1  17245  ramub1lem2  17246  ramcl  17248  prmonn2  17258  1259lem5  17354  2503lem3  17358  4001lem4  17363  chnrev  18842  gsumwsubmcl  19074  gsumsgrpccat  19077  gsumwmhm  19082  finodsubmsubg  19823  sylow1lem1  19854  efgsrel  19990  efgredlem  20003  srgbinomlem4  20497  freshmansdream  21924  psdpw  22535  chfacfisf  23216  chfacfisfcpmat  23217  cpmadugsumlemF  23238  lebnumii  25331  ovolunlem1  25862  dvexp  26317  dgreq0  26628  plyn0mulidp  26646  plymulidp  26647  dvply1  26649  vieta1lem2  26678  aaliou3lem8  26718  dvtaylp  26743  taylthlem1  26746  pserdvlem2  26801  pserdv2  26803  abelthlem6  26809  logtayl  27034  logtayl2  27036  cxpeq  27131  gamfac  27440  wilthlem1  27441  wilthlem2  27442  wilthlem3  27443  wilth  27444  wilthimp  27445  ftalem1  27446  basellem5  27458  1sgm2ppw  27573  chtublem  27584  perfect1  27601  perfect  27604  bcmono  27650  lgslem1  27670  lgsquadlem1  27753  lgsquad2lem2  27758  m1lgs  27761  selberg2lem  27923  logdivbnd  27929  pntrsumo1  27938  cusgrsize2inds  30080  cusgrrusgr  30208  pthdlem2  30400  crctcshwlkn0lem4  30448  wlkiswwlks2lem1  30504  wlkiswwlksupgr2  30512  clwwlkccatlem  30626  clwlkclwwlklem2a2  30630  clwwlknwwlksn  30675  clwwlkel  30683  clwwlkwwlksb  30691  wwlksubclwwlk  30695  oexpled  33513  1arithidomlem1  34164  1arithidomlem2  34165  1arithidom  34166  esplyind  34311  fibp1  35137  signstfvn  35302  signsvtn0  35303  subfacp1lem6  36151  erdszelem10  36166  erdsze2lem1  36169  erdsze2lem2  36170  cvmliftlem2  36252  bcprod  36711  poimirlem5  38804  poimirlem6  38805  poimirlem7  38806  poimirlem10  38809  poimirlem11  38810  poimirlem13  38812  poimirlem14  38813  poimirlem20  38819  poimirlem21  38820  poimirlem22  38821  poimirlem23  38822  poimirlem25  38824  poimirlem26  38825  poimirlem31  38830  lcmfunnnd  43321  lcmineqlem2  43339  lcmineqlem3  43340  lcmineqlem8  43345  lcmineqlem10  43347  lcmineqlem12  43349  dvrelogpow2b  43377  primrootsunit1  43406  sticksstones12a  43466  sticksstones16  43471  sticksstones22  43477  fltnltalem  43933  irrapxlem1  44089  rmspecsqrtnq  44173  jm2.24nn  44226  jm2.17a  44227  acongeq  44250  jm2.18  44255  jm2.22  44262  jm2.23  44263  jm2.20nn  44264  jm2.27c  44274  bccm1k  45581  binomcxplemwb  45587  binomcxplemnotnn0  45595  dvsinexp  47188  dvxpaek  47217  dvnxpaek  47219  itgsinexplem1  47231  itgsinexp  47232  wallispilem5  47346  stirlinglem5  47355  fourierdlem48  47431  fourierdlem49  47432  fourierdlem52  47435  fourierdlem54  47437  fourierdlem103  47486  fourierdlem104  47487  etransclem1  47512  etransclem4  47515  etransclem8  47519  etransclem10  47521  etransclem14  47525  etransclem15  47526  etransclem17  47528  etransclem18  47529  etransclem19  47530  etransclem20  47531  etransclem21  47532  etransclem22  47533  etransclem23  47534  etransclem24  47535  etransclem27  47538  etransclem28  47539  etransclem32  47543  etransclem35  47546  etransclem37  47548  etransclem38  47549  etransclem41  47552  etransclem44  47555  etransclem45  47556  etransclem46  47557  etransclem47  47558  etransclem48  47559  muldvdsfacgt  48723  muldvdsfacm1  48724  lswn0  48793  fmtnoodd  48885  sqrtpwpw2p  48890  fmtnosqrt  48891  fmtnodvds  48896  fmtnorec3  48900  fmtnorec4  48901  2pwp1prm  48941  lighneallem3  48959  lighneallem4a  48960  lighneallem4  48962  nprmdvdsfacm1lem4  48975  ppivalnnprm  48977  ppivalnnnprmge6  48978  oexpnegALTV  49042  perfectALTV  49088  fpprmod  49092  fppr2odd  49096  fpprwppr  49104  fpprwpprb  49105  bgoldbtbndlem4  49173  bcpascm1  49788  altgsumbcALT  49790  pw2m1lepw2m1  49957  nnpw2even  49966  logbpw2m1  50004  nnpw2blenfzo  50018  nnpw2pmod  50020  nnpw2p  50023  nnolog2flm1  50027  dignn0fr  50038  dig2nn1st  50042  digexp  50044  dignn0flhalflem1  50052