MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnm1nn0 Structured version   Visualization version   GIF version

Theorem nnm1nn0 11603
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
StepHypRef Expression
1 nn1m1nn 11328 . . . 4 (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ))
2 oveq1 6884 . . . . . 6 (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
3 1m1e0 11376 . . . . . 6 (1 − 1) = 0
42, 3syl6eq 2863 . . . . 5 (𝑁 = 1 → (𝑁 − 1) = 0)
54orim1i 924 . . . 4 ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
61, 5syl 17 . . 3 (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈ ℕ))
76orcomd 889 . 2 (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
8 elnn0 11564 . 2 ((𝑁 − 1) ∈ ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) = 0))
97, 8sylibr 225 1 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 865   = wceq 1637  wcel 2157  (class class class)co 6877  0cc0 10224  1c1 10225  cmin 10554  cn 11308  0cn0 11562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-ltxr 10367  df-sub 10556  df-nn 11309  df-n0 11563
This theorem is referenced by:  elnn0nn  11604  nn0n0n1ge2  11627  nnaddm1cl  11703  fseq1m1p1  12641  elfznelfzo  12800  nn0ennn  13005  expm1t  13114  expgt1  13124  digit1  13224  bcn1  13323  bcm1k  13325  bcn2m1  13334  swrdccatwrd  13695  cshwidxn  13782  isercoll2  14625  iseralt  14641  binomlem  14786  incexc  14794  incexc2  14795  arisum  14817  arisum2  14818  mertenslem2  14841  risefallfac  14978  fallfacfwd  14990  0fallfac  14991  bpolydiflem  15008  ruclem12  15193  iddvdsexp  15231  dvdsfac  15274  oexpneg  15292  pwp1fsum  15337  bitsfzolem  15378  bitsf1  15390  phibnd  15696  phiprmpw  15701  prmdiv  15710  oddprm  15735  iserodd  15760  fldivp1  15821  prmpwdvds  15828  4sqlem12  15880  4sqlem19  15887  vdwapid1  15899  vdwlem1  15905  vdwlem3  15907  vdwlem5  15909  vdwlem6  15910  vdwlem9  15913  0ram  15944  ram0  15946  ramub1lem1  15950  ramub1lem2  15951  ramcl  15953  prmonn2  15963  1259lem5  16056  2503lem3  16060  4001lem4  16065  gsumwsubmcl  17583  gsumccat  17586  gsumwmhm  17590  sylow1lem1  18217  efgsrel  18351  efgredlem  18364  srgbinomlem4  18748  chfacfisf  20876  chfacfisfcpmat  20877  cpmadugsumlemF  20898  lebnumii  22982  ovolunlem1  23484  dvexp  23936  dgreq0  24241  dvply1  24259  vieta1lem2  24286  aaliou3lem8  24320  dvtaylp  24344  taylthlem1  24347  pserdvlem2  24402  pserdv2  24404  abelthlem6  24410  logtayl  24626  logtayl2  24628  cxpeq  24718  leibpilem1  24887  gamfac  25013  wilthlem1  25014  wilthlem2  25015  wilthlem3  25016  wilth  25017  wilthimp  25018  ftalem1  25019  basellem5  25031  1sgm2ppw  25145  chtublem  25156  perfect1  25173  perfect  25176  bcmono  25222  lgslem1  25242  lgsquadlem1  25325  lgsquad2lem2  25330  m1lgs  25333  selberg2lem  25459  logdivbnd  25465  pntrsumo1  25474  cusgrsize2inds  26583  cusgrrusgr  26711  pthdlem2  26898  crctcshwlkn0lem4  26940  wlkiswwlks2lem1  27002  wlkiswwlksupgr2  27010  clwwlkccatlem  27138  clwlkclwwlklem2a2  27142  clwwlknwwlksn  27192  clwwlknwwlksnOLD  27193  clwwlkel  27201  clwwlkwwlksb  27210  wwlksubclwwlk  27215  fibp1  30794  plymulx0  30955  plymulx  30956  signstfvn  30977  signsvtn0  30978  subfacp1lem6  31495  erdszelem10  31510  erdsze2lem1  31513  erdsze2lem2  31514  cvmliftlem2  31596  bcprod  31951  poimirlem5  33729  poimirlem6  33730  poimirlem7  33731  poimirlem10  33734  poimirlem11  33735  poimirlem13  33737  poimirlem14  33738  poimirlem20  33744  poimirlem21  33745  poimirlem22  33746  poimirlem23  33747  poimirlem25  33749  poimirlem26  33750  poimirlem31  33755  irrapxlem1  37889  rmspecsqrtnq  37973  jm2.24nn  38028  jm2.17a  38029  acongeq  38052  jm2.18  38057  jm2.22  38064  jm2.23  38065  jm2.20nn  38066  jm2.27c  38076  bccm1k  39042  binomcxplemwb  39048  binomcxplemnotnn0  39056  dvsinexp  40606  dvxpaek  40636  dvnxpaek  40638  itgsinexplem1  40650  itgsinexp  40651  wallispilem5  40766  stirlinglem5  40775  fourierdlem48  40851  fourierdlem49  40852  fourierdlem52  40855  fourierdlem54  40857  fourierdlem103  40906  fourierdlem104  40907  etransclem1  40932  etransclem4  40935  etransclem8  40939  etransclem10  40941  etransclem14  40945  etransclem15  40946  etransclem17  40948  etransclem18  40949  etransclem19  40950  etransclem20  40951  etransclem21  40952  etransclem22  40953  etransclem23  40954  etransclem24  40955  etransclem27  40958  etransclem28  40959  etransclem32  40963  etransclem35  40966  etransclem37  40968  etransclem38  40969  etransclem41  40972  etransclem44  40975  etransclem45  40976  etransclem46  40977  etransclem47  40978  etransclem48  40979  lswn0  41956  fmtnoodd  42021  sqrtpwpw2p  42026  fmtnosqrt  42027  fmtnodvds  42032  fmtnorec3  42036  fmtnorec4  42037  pwdif  42077  2pwp1prm  42079  lighneallem3  42100  lighneallem4a  42101  lighneallem4  42103  oexpnegALTV  42164  perfectALTV  42208  bgoldbtbndlem4  42272  bcpascm1  42698  altgsumbcALT  42700  pw2m1lepw2m1  42879  nnpw2even  42892  logbpw2m1  42930  nnpw2blenfzo  42944  nnpw2pmod  42946  nnpw2p  42949  nnolog2flm1  42953  dignn0fr  42964  dig2nn1st  42968  digexp  42970  dignn0flhalflem1  42978
  Copyright terms: Public domain W3C validator