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

Theorem nn0ge0d 10651
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 10617 . 2  |-  ( A  e.  NN0  ->  0  <_  A )
31, 2syl 16 1  |-  ( ph  ->  0  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   class class class wbr 4304   0cc0 9294    <_ cle 9431   NN0cn0 10591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-iun 4185  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6489  df-recs 6844  df-rdg 6878  df-er 7113  df-en 7323  df-dom 7324  df-sdom 7325  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-nn 10335  df-n0 10592
This theorem is referenced by:  flmulnn0  11684  zmodfz  11741  modaddmodlo  11775  expmulnbnd  12008  facwordi  12077  faclbnd  12078  faclbnd4lem3  12083  faclbnd6  12087  facavg  12089  hashdom  12154  repswcshw  12458  climcnds  13326  geomulcvg  13348  mertenslem1  13356  eftabs  13373  efcllem  13375  efaddlem  13390  eftlub  13405  oexpneg  13607  divalg2  13621  bitsfzolem  13642  bitsmod  13644  sadcaddlem  13665  sadaddlem  13674  sadasslem  13678  sadeq  13680  smueqlem  13698  gcdmultiple  13746  gcdmultiplez  13747  dvdssqlem  13755  nn0seqcvgd  13757  mulgcddvds  13802  isprm5  13810  zsqrelqelz  13848  phibndlem  13857  dfphi2  13861  pythagtriplem3  13897  pythagtriplem10  13899  pythagtriplem6  13900  pythagtriplem7  13901  pythagtriplem12  13905  pythagtriplem14  13907  iserodd  13914  pcge0  13940  pcprmpw2  13960  pcmptdvds  13968  fldivp1  13971  pcbc  13974  qexpz  13975  pockthlem  13978  pockthg  13979  prmreclem3  13991  mul4sqlem  14026  4sqlem12  14029  4sqlem14  14031  4sqlem16  14033  0ram  14093  ram0  14095  ramcl  14102  2expltfac  14131  odmodnn0  16055  pgpfi  16116  ablfac1c  16584  psrbaglesupp  17447  psrbaglesuppOLD  17448  psrbagcon  17452  psrlidm  17486  psrlidmOLD  17487  coe1tmmul2  17741  prmirred  17931  prmirredOLD  17934  lebnumii  20550  mbfi1fseqlem1  21205  mbfi1fseqlem3  21207  mbfi1fseqlem4  21208  mbfi1fseqlem5  21209  itg2cnlem2  21252  fta1g  21651  coemulhi  21733  dgradd2  21747  dgrco  21754  aareccl  21804  aaliou3lem8  21823  radcnvlem1  21890  dvradcnv  21898  leibpilem1  22347  wilthlem1  22418  sgmmul  22552  chtublem  22562  fsumvma2  22565  chpchtsum  22570  perfectlem2  22581  bcmono  22628  bposlem5  22639  lgsval2lem  22657  lgsval4a  22669  lgsqrlem2  22693  lgseisenlem1  22700  lgseisenlem2  22701  lgsquadlem1  22705  2sqlem3  22717  2sqlem7  22721  2sqlem8  22723  2sqblem  22728  dchrisum0re  22774  pntrlog2bndlem4  22841  pntpbnd1a  22846  ostth2lem2  22895  ostth2lem3  22896  ostth2  22898  nndiffz1  26087  nexple  26460  oddpwdc  26749  eulerpartlems  26755  eulerpartlemgc  26757  eulerpartlemb  26763  dmlogdmgm  27022  subfaclim  27088  cvmliftlem2  27187  cvmliftlem10  27195  snmlff  27230  itg2addnclem2  28456  rrnequiv  28746  irrapxlem2  29176  irrapxlem5  29179  pellexlem1  29182  pellexlem2  29183  pellexlem5  29186  pellexlem6  29187  pell14qrgt0  29212  pell1qrge1  29223  pellfundgt1  29236  rmspecnonsq  29260  rmspecfund  29262  rmspecpos  29269  rmxypos  29302  ltrmxnn0  29304  jm2.24  29318  acongeq  29338  jm2.22  29356  jm2.23  29357  jm2.27a  29366  jm2.27c  29368  stoweidlem24  29831  wallispilem3  29874  wallispilem4  29875  wallispilem5  29876  wallispi2lem1  29878  stirlinglem4  29884  stirlinglem5  29885  stirlinglem10  29890  stirlinglem15  29895  stirlingr  29897  wwlksubclwwlk  30478
  Copyright terms: Public domain W3C validator