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

Theorem nn0ge0d 11204
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 11168 . 2 (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
31, 2syl 17 1 (𝜑 → 0 ≤ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977   class class class wbr 4578  0cc0 9793  cle 9932  0cn0 11142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-n0 11143
This theorem is referenced by:  flmulnn0  12448  zmodfz  12512  modaddmodlo  12554  modsumfzodifsn  12563  addmodlteq  12565  expmulnbnd  12816  facwordi  12896  faclbnd  12897  faclbnd4lem3  12902  faclbnd6  12906  facavg  12908  hashdom  12984  repswcshw  13358  climcnds  14371  geomulcvg  14395  mertenslem1  14404  eftabs  14594  efcllem  14596  efaddlem  14611  eftlub  14627  oexpneg  14856  divalg2  14915  bitsfzolem  14943  bitsmod  14945  sadcaddlem  14966  sadaddlem  14975  sadasslem  14979  sadeq  14981  smueqlem  14999  dfgcd2  15050  gcdmultiple  15056  gcdmultiplez  15057  dvdssqlem  15066  nn0seqcvgd  15070  mulgcddvds  15156  isprm5  15206  zsqrtelqelz  15253  phibndlem  15262  dfphi2  15266  pythagtriplem3  15310  pythagtriplem10  15312  pythagtriplem6  15313  pythagtriplem7  15314  pythagtriplem12  15318  pythagtriplem14  15320  iserodd  15327  pcge0  15353  pcprmpw2  15373  pcmptdvds  15385  fldivp1  15388  pcbc  15391  qexpz  15392  pockthlem  15396  pockthg  15397  prmreclem3  15409  mul4sqlem  15444  4sqlem12  15447  4sqlem14  15449  4sqlem16  15451  0ram  15511  ram0  15513  ramcl  15520  prmolefac  15537  2expltfac  15586  odmodnn0  17731  pgpfi  17792  ablfac1c  18242  psrbaglesupp  19138  psrbagcon  19141  psrlidm  19173  coe1tmmul2  19416  prmirred  19610  lebnumii  22521  mbfi1fseqlem1  23233  mbfi1fseqlem3  23235  mbfi1fseqlem4  23236  mbfi1fseqlem5  23237  itg2cnlem2  23280  fta1g  23676  coemulhi  23759  dgradd2  23773  dgrco  23780  aareccl  23830  aaliou3lem8  23849  radcnvlem1  23916  dvradcnv  23924  leibpilem1  24412  dmlogdmgm  24495  wilthlem1  24539  sgmmul  24671  chtublem  24681  fsumvma2  24684  chpchtsum  24689  perfectlem2  24700  bcmono  24747  bposlem5  24758  lgsval2lem  24777  lgsval4a  24789  lgsqrlem2  24817  gausslemma2dlem0c  24828  gausslemma2dlem0d  24829  lgseisenlem1  24845  lgseisenlem2  24846  lgsquadlem1  24850  2lgslem1a1  24859  2sqlem3  24890  2sqlem7  24894  2sqlem8  24896  2sqblem  24901  dchrisum0re  24947  pntrlog2bndlem4  25014  pntpbnd1a  25019  ostth2lem2  25068  ostth2lem3  25069  ostth2  25071  wwlksubclwwlk  26126  nndiffz1  28730  2sqmod  28773  submateqlem1  28995  nexple  29193  oddpwdc  29537  eulerpartlems  29543  eulerpartlemgc  29545  eulerpartlemb  29551  subfaclim  30218  cvmliftlem2  30316  cvmliftlem10  30324  snmlff  30359  poimirlem10  32383  poimirlem23  32396  poimirlem24  32397  itg2addnclem2  32426  rrnequiv  32598  irrapxlem2  36199  irrapxlem5  36202  pellexlem1  36205  pellexlem2  36206  pellexlem5  36209  pellexlem6  36210  pell14qrgt0  36235  pell1qrge1  36246  pellfundgt1  36259  rmspecnonsq  36284  rmspecfund  36286  rmspecpos  36293  rmxypos  36326  ltrmxnn0  36328  jm2.24  36342  acongeq  36362  jm2.22  36374  jm2.23  36375  jm2.27a  36384  jm2.27c  36386  nzprmdif  37334  bccbc  37360  binomcxplemnn0  37364  fsumnncl  38432  mccllem  38458  ioodvbdlimc1lem2  38616  ioodvbdlimc2lem  38618  dvnxpaek  38626  dvnmul  38627  dvnprodlem1  38630  stoweidlem24  38711  wallispilem4  38755  wallispilem5  38756  wallispi2lem1  38758  stirlinglem4  38764  stirlinglem5  38765  stirlinglem10  38770  stirlinglem15  38775  stirlingr  38777  fourierdlem48  38841  fourierdlem49  38842  fourierdlem92  38885  sqwvfoura  38915  elaa2lem  38920  etransclem19  38940  etransclem23  38944  etransclem27  38948  etransclem44  38965  rrndistlt  38980  oexpnegALTV  39921  perfectALTVlem2  39960  crctcsh1wlkn0lem4  41008  wwlksubclwwlks  41224  blennn  42159  dignn0ldlem  42186  dig2nn1st  42189  digexp  42191  dignn0flhalf  42202
  Copyright terms: Public domain W3C validator