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

Theorem nn0ge0d 11542
Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0ge0d (𝜑 → 0 ≤ 𝐴)

Proof of Theorem nn0ge0d
StepHypRef Expression
1 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
2 nn0ge0 11506 . 2 (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
31, 2syl 17 1 (𝜑 → 0 ≤ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2135   class class class wbr 4800  0cc0 10124  cle 10263  0cn0 11480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-nn 11209  df-n0 11481
This theorem is referenced by:  flmulnn0  12818  zmodfz  12882  modaddmodlo  12924  modsumfzodifsn  12933  addmodlteq  12935  expmulnbnd  13186  facwordi  13266  faclbnd  13267  faclbnd4lem3  13272  faclbnd6  13276  facavg  13278  hashdom  13356  repswcshw  13754  climcnds  14778  geomulcvg  14802  mertenslem1  14811  eftabs  15001  efcllem  15003  efaddlem  15018  eftlub  15034  oexpneg  15267  divalg2  15326  bitsfzolem  15354  bitsmod  15356  sadcaddlem  15377  sadaddlem  15386  sadasslem  15390  sadeq  15392  smueqlem  15410  dfgcd2  15461  gcdmultiple  15467  gcdmultiplez  15468  dvdssqlem  15477  nn0seqcvgd  15481  mulgcddvds  15567  isprm5  15617  zsqrtelqelz  15664  phibndlem  15673  dfphi2  15677  pythagtriplem3  15721  pythagtriplem10  15723  pythagtriplem6  15724  pythagtriplem7  15725  pythagtriplem12  15729  pythagtriplem14  15731  iserodd  15738  pcge0  15764  pcprmpw2  15784  pcmptdvds  15796  fldivp1  15799  pcbc  15802  qexpz  15803  pockthlem  15807  pockthg  15808  prmreclem3  15820  mul4sqlem  15855  4sqlem12  15858  4sqlem14  15860  4sqlem16  15862  0ram  15922  ram0  15924  ramcl  15931  prmolefac  15948  2expltfac  15997  odmodnn0  18155  pgpfi  18216  ablfac1c  18666  psrbaglesupp  19566  psrbagcon  19569  psrlidm  19601  coe1tmmul2  19844  prmirred  20041  lebnumii  22962  mbfi1fseqlem1  23677  mbfi1fseqlem3  23679  mbfi1fseqlem4  23680  mbfi1fseqlem5  23681  itg2cnlem2  23724  fta1g  24122  coemulhi  24205  dgradd2  24219  dgrco  24226  aareccl  24276  aaliou3lem8  24295  radcnvlem1  24362  dvradcnv  24370  leibpilem1  24862  dmlogdmgm  24945  wilthlem1  24989  sgmmul  25121  chtublem  25131  fsumvma2  25134  chpchtsum  25139  perfectlem2  25150  bcmono  25197  bposlem5  25208  lgsval2lem  25227  lgsval4a  25239  lgsqrlem2  25267  gausslemma2dlem0c  25278  gausslemma2dlem0d  25279  lgseisenlem1  25295  lgseisenlem2  25296  lgsquadlem1  25300  2lgslem1a1  25309  2sqlem3  25340  2sqlem7  25344  2sqlem8  25346  2sqblem  25351  dchrisum0re  25397  pntrlog2bndlem4  25464  pntpbnd1a  25469  ostth2lem2  25518  ostth2lem3  25519  ostth2  25521  crctcshwlkn0lem4  26912  wwlksubclwwlk  27185  nnmulge  29820  nndiffz1  29853  2sqmod  29953  submateqlem1  30178  nexple  30376  oddpwdc  30721  eulerpartlems  30727  eulerpartlemgc  30729  eulerpartlemb  30735  fsum2dsub  30990  breprexplemc  31015  circlemeth  31023  tgoldbachgtde  31043  subfaclim  31473  cvmliftlem2  31571  cvmliftlem10  31579  snmlff  31614  dfgcd3  33477  poimirlem10  33728  poimirlem23  33741  poimirlem24  33742  itg2addnclem2  33771  rrnequiv  33943  irrapxlem2  37885  irrapxlem5  37888  pellexlem1  37891  pellexlem2  37892  pellexlem5  37895  pellexlem6  37896  pell14qrgt0  37921  pell1qrge1  37932  pellfundgt1  37945  rmspecnonsq  37970  rmspecfund  37972  rmspecpos  37979  rmxypos  38012  ltrmxnn0  38014  jm2.24  38028  acongeq  38048  jm2.22  38060  jm2.23  38061  jm2.27a  38070  jm2.27c  38072  nzprmdif  39016  bccbc  39042  binomcxplemnn0  39046  fsumnncl  40302  mccllem  40328  ioodvbdlimc1lem2  40646  ioodvbdlimc2lem  40648  dvnxpaek  40656  dvnmul  40657  dvnprodlem1  40660  stoweidlem24  40740  wallispilem4  40784  wallispilem5  40785  wallispi2lem1  40787  stirlinglem4  40793  stirlinglem5  40794  stirlinglem10  40799  stirlinglem15  40804  stirlingr  40806  fourierdlem48  40870  fourierdlem49  40871  fourierdlem92  40914  sqwvfoura  40944  elaa2lem  40949  etransclem19  40969  etransclem23  40973  etransclem27  40977  etransclem44  40994  rrndistlt  41009  oexpnegALTV  42094  perfectALTVlem2  42137  blennn  42875  dignn0ldlem  42902  dig2nn1st  42905  digexp  42907  dignn0flhalf  42918
  Copyright terms: Public domain W3C validator