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

Theorem nn0ge0d 10957
Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0ge0d  |-  ( ph  ->  0  <_  A )

Proof of Theorem nn0ge0d
StepHypRef Expression
1 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
2 nn0ge0 10924 . 2  |-  ( A  e.  NN0  ->  0  <_  A )
31, 2syl 17 1  |-  ( ph  ->  0  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   class class class wbr 4416   0cc0 9565    <_ cle 9702   NN0cn0 10898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-n0 10899
This theorem is referenced by:  flmulnn0  12092  zmodfz  12150  modaddmodlo  12186  expmulnbnd  12436  facwordi  12506  faclbnd  12507  faclbnd4lem3  12512  faclbnd6  12516  facavg  12518  hashdom  12590  repswcshw  12948  climcnds  13958  geomulcvg  13981  mertenslem1  13989  eftabs  14179  efcllem  14181  efaddlem  14196  eftlub  14212  oexpneg  14417  divalg2  14435  bitsfzolem  14456  bitsfzolemOLD  14457  bitsmod  14459  sadcaddlem  14480  sadaddlem  14489  sadasslem  14493  sadeq  14495  smueqlem  14513  gcdmultiple  14567  gcdmultiplez  14568  dvdssqlem  14576  nn0seqcvgd  14578  isprm5  14700  mulgcddvds  14710  zsqrtelqelz  14756  phibndlem  14767  dfphi2  14771  pythagtriplem3  14817  pythagtriplem10  14819  pythagtriplem6  14820  pythagtriplem7  14821  pythagtriplem12  14825  pythagtriplem14  14827  iserodd  14834  pcge0  14860  pcprmpw2  14880  pcmptdvds  14888  fldivp1  14891  pcbc  14894  qexpz  14895  pockthlem  14898  pockthg  14899  prmreclem3  14911  mul4sqlem  14946  4sqlem12  14949  4sqlem14OLD  14951  4sqlem16OLD  14953  4sqlem14  14957  4sqlem16  14959  0ram  15027  ram0  15029  ramcl  15036  prmolefac  15053  prmorlefacOLD  15067  2expltfac  15112  odmodnn0  17238  pgpfi  17306  ablfac1c  17753  psrbaglesupp  18641  psrbagcon  18644  psrlidm  18676  coe1tmmul2  18918  prmirred  19115  lebnumii  22046  mbfi1fseqlem1  22722  mbfi1fseqlem3  22724  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  itg2cnlem2  22769  fta1g  23167  coemulhi  23257  dgradd2  23271  dgrco  23278  aareccl  23331  aaliou3lem8  23350  radcnvlem1  23417  dvradcnv  23425  leibpilem1  23915  dmlogdmgm  23998  wilthlem1  24042  sgmmul  24178  chtublem  24188  fsumvma2  24191  chpchtsum  24196  perfectlem2  24207  bcmono  24254  bposlem5  24265  lgsval2lem  24283  lgsval4a  24295  lgsqrlem2  24319  lgseisenlem1  24326  lgseisenlem2  24327  lgsquadlem1  24331  2sqlem3  24343  2sqlem7  24347  2sqlem8  24349  2sqblem  24354  dchrisum0re  24400  pntrlog2bndlem4  24467  pntpbnd1a  24472  ostth2lem2  24521  ostth2lem3  24522  ostth2  24524  wwlksubclwwlk  25581  nndiffz1  28415  2sqmod  28458  submateqlem1  28682  nexple  28880  oddpwdc  29236  eulerpartlems  29242  eulerpartlemgc  29244  eulerpartlemb  29250  subfaclim  29960  cvmliftlem2  30058  cvmliftlem10  30066  snmlff  30101  poimirlem10  31995  poimirlem23  32008  poimirlem24  32009  itg2addnclem2  32039  rrnequiv  32212  irrapxlem2  35712  irrapxlem5  35715  pellexlem1  35718  pellexlem2  35719  pellexlem5  35722  pellexlem6  35723  pell14qrgt0  35750  pell1qrge1  35761  pellfundgt1  35776  rmspecnonsq  35800  rmspecfund  35802  rmspecpos  35809  rmxypos  35842  ltrmxnn0  35844  jm2.24  35858  acongeq  35878  jm2.22  35895  jm2.23  35896  jm2.27a  35905  jm2.27c  35907  nzprmdif  36712  bccbc  36738  binomcxplemnn0  36742  fsumnncl  37688  mccllem  37715  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvnxpaek  37855  dvnmul  37856  dvnprodlem1  37859  stoweidlem24  37922  wallispilem4  37968  wallispilem5  37969  wallispi2lem1  37971  stirlinglem4  37977  stirlinglem5  37978  stirlinglem10  37983  stirlinglem15  37988  stirlingr  37990  fourierdlem48  38056  fourierdlem49  38057  fourierdlem92  38100  sqwvfoura  38130  elaa2lem  38135  elaa2lemOLD  38136  etransclem19  38156  etransclem23  38160  etransclem27  38164  etransclem44  38181  rrndistlt  38197  oexpnegALTV  38844  perfectALTVlem2  38882  blennn  40659  dignn0ldlem  40686  dig2nn1st  40689  digexp  40691  dignn0flhalf  40702
  Copyright terms: Public domain W3C validator