Theorem nnm1nn0 12469

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 12186	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2		oveq1 7363	. . . . . 6 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3		1m1e0 12244	. . . . . 6 ⊢ (1 − 1) = 0
4	2, 3	eqtrdi 2790	. . . . 5 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
5	4	orim1i 915	. . . 4 ⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
6	1, 5	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
7	6	orcomd 877	. 2 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8		elnn0 12430	. 2 ⊢ ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
9	7, 8	sylibr 235	1 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  0cc0 11029  1c1 11030   − cmin 11368  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-nn 12166  df-n0 12429

This theorem is referenced by:  elnn0nn  12470  nn0n0n1ge2  12496  nnaddm1cl  12577  fseq1m1p1  13544  elfznelfzo  13719  nn0ennn  13932  expm1t  14043  expgt1  14053  digit1  14190  bcn1  14266  bcm1k  14268  bcn2m1  14277  cshwidxn  14762  isercoll2  15622  iseralt  15638  binomlem  15785  incexc  15793  incexc2  15794  arisum  15816  arisum2  15817  pwdif  15824  mertenslem2  15841  risefallfac  15980  fallfacfwd  15992  0fallfac  15993  bpolydiflem  16010  ruclem12  16199  iddvdsexp  16239  dvdsfac  16286  oexpneg  16305  pwp1fsum  16351  bitsfzolem  16394  bitsf1  16406  phibnd  16732  phiprmpw  16737  prmdiv  16746  oddprm  16772  iserodd  16797  fldivp1  16859  prmpwdvds  16866  4sqlem12  16918  4sqlem19  16925  vdwapid1  16937  vdwlem1  16943  vdwlem3  16945  vdwlem5  16947  vdwlem6  16948  vdwlem9  16951  0ram  16982  ram0  16984  ramub1lem1  16988  ramub1lem2  16989  ramcl  16991  prmonn2  17001  1259lem5  17096  2503lem3  17100  4001lem4  17105  chnrev  18584  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  finodsubmsubg  19533  sylow1lem1  19564  efgsrel  19700  efgredlem  19713  srgbinomlem4  20201  freshmansdream  21549  psdpw  22158  chfacfisf  22837  chfacfisfcpmat  22838  cpmadugsumlemF  22859  lebnumii  24951  ovolunlem1  25482  dvexp  25938  dgreq0  26248  dvply1  26268  vieta1lem2  26295  aaliou3lem8  26329  dvtaylp  26353  taylthlem1  26356  pserdvlem2  26411  pserdv2  26413  abelthlem6  26419  logtayl  26642  logtayl2  26644  cxpeq  26739  gamfac  27048  wilthlem1  27049  wilthlem2  27050  wilthlem3  27051  wilth  27052  wilthimp  27053  ftalem1  27054  basellem5  27066  1sgm2ppw  27181  chtublem  27192  perfect1  27209  perfect  27212  bcmono  27258  lgslem1  27278  lgsquadlem1  27361  lgsquad2lem2  27366  m1lgs  27369  selberg2lem  27531  logdivbnd  27537  pntrsumo1  27546  cusgrsize2inds  29540  cusgrrusgr  29668  pthdlem2  29854  crctcshwlkn0lem4  29899  wlkiswwlks2lem1  29955  wlkiswwlksupgr2  29963  clwwlkccatlem  30077  clwlkclwwlklem2a2  30081  clwwlknwwlksn  30126  clwwlkel  30134  clwwlkwwlksb  30142  wwlksubclwwlk  30146  oexpled  32939  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  esplyind  33759  fibp1  34585  plymulx0  34731  plymulx  34732  signstfvn  34753  signsvtn0  34754  subfacp1lem6  35413  erdszelem10  35428  erdsze2lem1  35431  erdsze2lem2  35432  cvmliftlem2  35514  bcprod  35966  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem10  37997  poimirlem11  37998  poimirlem13  38000  poimirlem14  38001  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem23  38010  poimirlem25  38012  poimirlem26  38013  poimirlem31  38018  lcmfunnnd  42497  lcmineqlem2  42515  lcmineqlem3  42516  lcmineqlem8  42521  lcmineqlem10  42523  lcmineqlem12  42525  dvrelogpow2b  42553  primrootsunit1  42582  sticksstones12a  42642  sticksstones16  42647  sticksstones22  42653  fltnltalem  43112  irrapxlem1  43267  rmspecsqrtnq  43351  jm2.24nn  43404  jm2.17a  43405  acongeq  43428  jm2.18  43433  jm2.22  43440  jm2.23  43441  jm2.20nn  43442  jm2.27c  43452  bccm1k  44786  binomcxplemwb  44792  binomcxplemnotnn0  44800  dvsinexp  46354  dvxpaek  46383  dvnxpaek  46385  itgsinexplem1  46397  itgsinexp  46398  wallispilem5  46512  stirlinglem5  46521  fourierdlem48  46597  fourierdlem49  46598  fourierdlem52  46601  fourierdlem54  46603  fourierdlem103  46652  fourierdlem104  46653  etransclem1  46678  etransclem4  46681  etransclem8  46685  etransclem10  46687  etransclem14  46691  etransclem15  46692  etransclem17  46694  etransclem18  46695  etransclem19  46696  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem23  46700  etransclem24  46701  etransclem27  46704  etransclem28  46705  etransclem32  46709  etransclem35  46712  etransclem37  46714  etransclem38  46715  etransclem41  46718  etransclem44  46721  etransclem45  46722  etransclem46  46723  etransclem47  46724  etransclem48  46725  muldvdsfacgt  47849  muldvdsfacm1  47850  lswn0  47919  fmtnoodd  48011  sqrtpwpw2p  48016  fmtnosqrt  48017  fmtnodvds  48022  fmtnorec3  48026  fmtnorec4  48027  2pwp1prm  48067  lighneallem3  48085  lighneallem4a  48086  lighneallem4  48088  nprmdvdsfacm1lem4  48101  ppivalnnprm  48103  ppivalnnnprmge6  48104  oexpnegALTV  48168  perfectALTV  48214  fpprmod  48218  fppr2odd  48222  fpprwppr  48230  fpprwpprb  48231  bgoldbtbndlem4  48299  bcpascm1  48842  altgsumbcALT  48844  pw2m1lepw2m1  49011  nnpw2even  49020  logbpw2m1  49058  nnpw2blenfzo  49072  nnpw2pmod  49074  nnpw2p  49077  nnolog2flm1  49081  dignn0fr  49092  dig2nn1st  49096  digexp  49098  dignn0flhalflem1  49106