Theorem nnm1nn0 12640

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 12349	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7425	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12408	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2812	. . . . 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 12601	. 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 2145  (class class class)co 7418  0cc0 11193  1c1 11194   − cmin 11534  ℕcn 12328  ℕ₀cn0 12599

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-sub 11536  df-nn 12329  df-n0 12600

This theorem is used by:  elnn0nn  12641  nn0n0n1ge2  12667  nnaddm1cl  12749  fseq1m1p1  13726  elfznelfzo  13901  nn0ennn  14115  expm1t  14226  expgt1  14236  digit1  14374  bcn1  14450  bcm1k  14452  bcn2m1  14461  cshwidxn  14953  isercoll2  15829  iseralt  15845  binomlem  15991  incexc  15999  incexc2  16000  arisum  16022  arisum2  16023  pwdif  16030  mertenslem2  16047  risefallfac  16184  fallfacfwd  16195  0fallfac  16196  bpolydiflem  16213  ruclem12  16402  iddvdsexp  16442  dvdsfac  16489  oexpneg  16508  pwp1fsum  16554  bitsfzolem  16597  bitsf1  16609  phibnd  16941  phiprmpw  16946  prmdiv  16955  oddprm  16981  iserodd  17006  fldivp1  17068  prmpwdvds  17075  4sqlem12  17127  4sqlem19  17134  vdwapid1  17146  vdwlem1  17152  vdwlem3  17154  vdwlem5  17156  vdwlem6  17157  vdwlem9  17160  0ram  17191  ram0  17193  ramub1lem1  17197  ramub1lem2  17198  ramcl  17200  prmonn2  17210  1259lem5  17306  2503lem3  17310  4001lem4  17315  chnrev  18794  gsumwsubmcl  19026  gsumsgrpccat  19029  gsumwmhm  19034  finodsubmsubg  19774  sylow1lem1  19805  efgsrel  19941  efgredlem  19954  srgbinomlem4  20448  freshmansdream  21873  psdpw  22484  chfacfisf  23165  chfacfisfcpmat  23166  cpmadugsumlemF  23187  lebnumii  25280  ovolunlem1  25811  dvexp  26266  dgreq0  26577  plyn0mulidp  26595  plymulidp  26596  dvply1  26598  vieta1lem2  26627  aaliou3lem8  26665  dvtaylp  26690  taylthlem1  26693  pserdvlem2  26748  pserdv2  26750  abelthlem6  26756  logtayl  26981  logtayl2  26983  cxpeq  27078  gamfac  27387  wilthlem1  27388  wilthlem2  27389  wilthlem3  27390  wilth  27391  wilthimp  27392  ftalem1  27393  basellem5  27405  1sgm2ppw  27520  chtublem  27531  perfect1  27548  perfect  27551  bcmono  27597  lgslem1  27617  lgsquadlem1  27700  lgsquad2lem2  27705  m1lgs  27708  selberg2lem  27870  logdivbnd  27876  pntrsumo1  27885  cusgrsize2inds  30027  cusgrrusgr  30155  pthdlem2  30347  crctcshwlkn0lem4  30395  wlkiswwlks2lem1  30451  wlkiswwlksupgr2  30459  clwwlkccatlem  30573  clwlkclwwlklem2a2  30577  clwwlknwwlksn  30622  clwwlkel  30630  clwwlkwwlksb  30638  wwlksubclwwlk  30642  oexpled  33420  1arithidomlem1  34060  1arithidomlem2  34061  1arithidom  34062  esplyind  34200  fibp1  35026  signstfvn  35191  signsvtn0  35192  subfacp1lem6  35929  erdszelem10  35944  erdsze2lem1  35947  erdsze2lem2  35948  cvmliftlem2  36030  bcprod  36482  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  poimirlem13  38531  poimirlem14  38532  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem23  38541  poimirlem25  38543  poimirlem26  38544  poimirlem31  38549  lcmfunnnd  43042  lcmineqlem2  43060  lcmineqlem3  43061  lcmineqlem8  43066  lcmineqlem10  43068  lcmineqlem12  43070  dvrelogpow2b  43098  primrootsunit1  43127  sticksstones12a  43187  sticksstones16  43192  sticksstones22  43198  fltnltalem  43653  irrapxlem1  43808  rmspecsqrtnq  43892  jm2.24nn  43945  jm2.17a  43946  acongeq  43969  jm2.18  43974  jm2.22  43981  jm2.23  43982  jm2.20nn  43983  jm2.27c  43993  bccm1k  45311  binomcxplemwb  45317  binomcxplemnotnn0  45325  dvsinexp  46890  dvxpaek  46919  dvnxpaek  46921  itgsinexplem1  46933  itgsinexp  46934  wallispilem5  47048  stirlinglem5  47057  fourierdlem48  47133  fourierdlem49  47134  fourierdlem52  47137  fourierdlem54  47139  fourierdlem103  47188  fourierdlem104  47189  etransclem1  47214  etransclem4  47217  etransclem8  47221  etransclem10  47223  etransclem14  47227  etransclem15  47228  etransclem17  47230  etransclem18  47231  etransclem19  47232  etransclem20  47233  etransclem21  47234  etransclem22  47235  etransclem23  47236  etransclem24  47237  etransclem27  47240  etransclem28  47241  etransclem32  47245  etransclem35  47248  etransclem37  47250  etransclem38  47251  etransclem41  47254  etransclem44  47257  etransclem45  47258  etransclem46  47259  etransclem47  47260  etransclem48  47261  muldvdsfacgt  48425  muldvdsfacm1  48426  lswn0  48495  fmtnoodd  48587  sqrtpwpw2p  48592  fmtnosqrt  48593  fmtnodvds  48598  fmtnorec3  48602  fmtnorec4  48603  2pwp1prm  48643  lighneallem3  48661  lighneallem4a  48662  lighneallem4  48664  nprmdvdsfacm1lem4  48677  ppivalnnprm  48679  ppivalnnnprmge6  48680  oexpnegALTV  48744  perfectALTV  48790  fpprmod  48794  fppr2odd  48798  fpprwppr  48806  fpprwpprb  48807  bgoldbtbndlem4  48875  bcpascm1  49432  altgsumbcALT  49434  pw2m1lepw2m1  49601  nnpw2even  49610  logbpw2m1  49648  nnpw2blenfzo  49662  nnpw2pmod  49664  nnpw2p  49667  nnolog2flm1  49671  dignn0fr  49682  dig2nn1st  49686  digexp  49688  dignn0flhalflem1  49696