Theorem nnm1nn0 12546

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 12255	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7419	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12314	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2814	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 922	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 18	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 884	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12507	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 237	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  0cc0 11101  1c1 11102   − cmin 11442  ℕcn 12234  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11444  df-nn 12235  df-n0 12506

This theorem is referenced by:  elnn0nn  12547  nn0n0n1ge2  12573  nnaddm1cl  12654  fseq1m1p1  13629  elfznelfzo  13804  nn0ennn  14017  expm1t  14128  expgt1  14138  digit1  14275  bcn1  14351  bcm1k  14353  bcn2m1  14362  cshwidxn  14848  isercoll2  15722  iseralt  15738  binomlem  15885  incexc  15893  incexc2  15894  arisum  15916  arisum2  15917  pwdif  15924  mertenslem2  15941  risefallfac  16080  fallfacfwd  16091  0fallfac  16092  bpolydiflem  16109  ruclem12  16298  iddvdsexp  16338  dvdsfac  16385  oexpneg  16404  pwp1fsum  16450  bitsfzolem  16493  bitsf1  16505  phibnd  16831  phiprmpw  16836  prmdiv  16845  oddprm  16871  iserodd  16896  fldivp1  16958  prmpwdvds  16965  4sqlem12  17017  4sqlem19  17024  vdwapid1  17036  vdwlem1  17042  vdwlem3  17044  vdwlem5  17046  vdwlem6  17047  vdwlem9  17050  0ram  17081  ram0  17083  ramub1lem1  17087  ramub1lem2  17088  ramcl  17090  prmonn2  17100  1259lem5  17196  2503lem3  17200  4001lem4  17205  chnrev  18684  gsumwsubmcl  18897  gsumsgrpccat  18900  gsumwmhm  18905  finodsubmsubg  19638  sylow1lem1  19669  efgsrel  19805  efgredlem  19818  srgbinomlem4  20312  freshmansdream  21705  psdpw  22314  chfacfisf  22992  chfacfisfcpmat  22993  cpmadugsumlemF  23014  lebnumii  25106  ovolunlem1  25637  dvexp  26093  dgreq0  26403  plyn0mulidp  26423  plymulidp  26424  dvply1  26426  vieta1lem2  26453  aaliou3lem8  26489  dvtaylp  26514  taylthlem1  26517  pserdvlem2  26572  pserdv2  26574  abelthlem6  26580  logtayl  26806  logtayl2  26808  cxpeq  26903  gamfac  27212  wilthlem1  27213  wilthlem2  27214  wilthlem3  27215  wilth  27216  wilthimp  27217  ftalem1  27218  basellem5  27230  1sgm2ppw  27345  chtublem  27356  perfect1  27373  perfect  27376  bcmono  27422  lgslem1  27442  lgsquadlem1  27525  lgsquad2lem2  27530  m1lgs  27533  selberg2lem  27695  logdivbnd  27701  pntrsumo1  27710  cusgrsize2inds  29784  cusgrrusgr  29912  pthdlem2  30098  crctcshwlkn0lem4  30143  wlkiswwlks2lem1  30199  wlkiswwlksupgr2  30207  clwwlkccatlem  30321  clwlkclwwlklem2a2  30325  clwwlknwwlksn  30370  clwwlkel  30378  clwwlkwwlksb  30386  wwlksubclwwlk  30390  oexpled  33161  1arithidomlem1  33806  1arithidomlem2  33807  1arithidom  33808  esplyind  33946  fibp1  34772  signstfvn  34937  signsvtn0  34938  subfacp1lem6  35658  erdszelem10  35673  erdsze2lem1  35676  erdsze2lem2  35677  cvmliftlem2  35759  bcprod  36211  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem13  38265  poimirlem14  38266  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem25  38277  poimirlem26  38278  poimirlem31  38283  lcmfunnnd  42760  lcmineqlem2  42778  lcmineqlem3  42779  lcmineqlem8  42784  lcmineqlem10  42786  lcmineqlem12  42788  dvrelogpow2b  42816  primrootsunit1  42845  sticksstones12a  42905  sticksstones16  42910  sticksstones22  42916  fltnltalem  43377  irrapxlem1  43532  rmspecsqrtnq  43616  jm2.24nn  43669  jm2.17a  43670  acongeq  43693  jm2.18  43698  jm2.22  43705  jm2.23  43706  jm2.20nn  43707  jm2.27c  43717  bccm1k  45035  binomcxplemwb  45041  binomcxplemnotnn0  45049  dvsinexp  46608  dvxpaek  46637  dvnxpaek  46639  itgsinexplem1  46651  itgsinexp  46652  wallispilem5  46766  stirlinglem5  46775  fourierdlem48  46851  fourierdlem49  46852  fourierdlem52  46855  fourierdlem54  46857  fourierdlem103  46906  fourierdlem104  46907  etransclem1  46932  etransclem4  46935  etransclem8  46939  etransclem10  46941  etransclem14  46945  etransclem15  46946  etransclem17  46948  etransclem18  46949  etransclem19  46950  etransclem20  46951  etransclem21  46952  etransclem22  46953  etransclem23  46954  etransclem24  46955  etransclem27  46958  etransclem28  46959  etransclem32  46963  etransclem35  46966  etransclem37  46968  etransclem38  46969  etransclem41  46972  etransclem44  46975  etransclem45  46976  etransclem46  46977  etransclem47  46978  etransclem48  46979  muldvdsfacgt  48106  muldvdsfacm1  48107  lswn0  48176  fmtnoodd  48268  sqrtpwpw2p  48273  fmtnosqrt  48274  fmtnodvds  48279  fmtnorec3  48283  fmtnorec4  48284  2pwp1prm  48324  lighneallem3  48342  lighneallem4a  48343  lighneallem4  48345  nprmdvdsfacm1lem4  48358  ppivalnnprm  48360  ppivalnnnprmge6  48361  oexpnegALTV  48425  perfectALTV  48471  fpprmod  48475  fppr2odd  48479  fpprwppr  48487  fpprwpprb  48488  bgoldbtbndlem4  48556  bcpascm1  49114  altgsumbcALT  49116  pw2m1lepw2m1  49283  nnpw2even  49292  logbpw2m1  49330  nnpw2blenfzo  49344  nnpw2pmod  49346  nnpw2p  49349  nnolog2flm1  49353  dignn0fr  49364  dig2nn1st  49368  digexp  49370  dignn0flhalflem1  49378