Theorem nn0ge0d 12492

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

Step	Hyp	Ref	Expression
1		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2		nn0ge0 12453	. 2 ⊢ (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  0cc0 11029   ≤ cle 11171  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429

This theorem is referenced by:  flmulnn0  13777  zmodfz  13843  modaddmodlo  13888  modsumfzodifsn  13897  addmodlteq  13899  expmulnbnd  14188  facwordi  14242  faclbnd  14243  faclbnd4lem3  14248  faclbnd6  14252  facavg  14254  hashdom  14332  climcnds  15807  geomulcvg  15832  mertenslem1  15840  eftabs  16031  efcllem  16033  efaddlem  16049  eftlub  16067  oexpneg  16305  divalg2  16365  bitsfzolem  16394  bitsmod  16396  sadcaddlem  16417  sadaddlem  16426  sadasslem  16430  sadeq  16432  smueqlem  16450  dfgcd2  16506  dvdssqlem  16526  nn0seqcvgd  16530  mulgcddvds  16615  isprm5  16668  zsqrtelqelz  16719  phibndlem  16731  dfphi2  16735  pythagtriplem3  16780  pythagtriplem10  16782  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem12  16788  pythagtriplem14  16790  iserodd  16797  pcge0  16824  pcprmpw2  16844  pcmptdvds  16856  fldivp1  16859  pcbc  16862  qexpz  16863  pockthlem  16867  pockthg  16868  prmreclem3  16880  mul4sqlem  16915  4sqlem12  16918  4sqlem14  16920  4sqlem16  16922  0ram  16982  ram0  16984  ramcl  16991  prmolefac  17008  2expltfac  17054  odmodnn0  19506  pgpfi  19571  ablfac1c  20039  prmirred  21449  psrbaglesupp  21897  psrbagcon  21900  psrlidm  21936  psdmul  22154  coe1tmmul2  22262  lebnumii  24951  mbfi1fseqlem1  25700  mbfi1fseqlem3  25702  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  itg2cnlem2  25747  fta1g  26153  coemulhi  26237  dgradd2  26251  dgrco  26258  aareccl  26310  aaliou3lem8  26329  radcnvlem1  26396  dvradcnv  26404  dmlogdmgm  27005  wilthlem1  27049  sgmmul  27182  chtublem  27192  fsumvma2  27195  chpchtsum  27200  perfectlem2  27211  bcmono  27258  bposlem5  27269  lgsval2lem  27288  lgsval4a  27300  lgsqrlem2  27328  gausslemma2dlem0c  27339  gausslemma2dlem0d  27340  lgseisenlem1  27356  lgseisenlem2  27357  lgsquadlem1  27361  2lgslem1a1  27370  2sqlem3  27401  2sqlem7  27405  2sqlem8  27407  2sqblem  27412  2sqmod  27417  2sqreunnlem1  27430  dchrisum0re  27494  pntrlog2bndlem4  27561  pntpbnd1a  27566  ostth2lem2  27615  ostth2lem3  27616  ostth2  27618  crctcshwlkn0lem4  29899  wwlksubclwwlk  30146  nnmulge  32831  nndiffz1  32878  fzo0opth  32895  nexple  32936  pfxlsw2ccat  33029  wrdt2ind  33032  gsumwrd2dccatlem  33158  ply1unit  33658  selvply1rhmlemb  33703  mplmulmvr  33723  esplyind  33759  constrdircl  33949  iconstr  33950  submateqlem1  33991  oddpwdc  34538  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemb  34552  fsum2dsub  34791  breprexplemc  34816  circlemeth  34824  tgoldbachgtde  34844  usgrgt2cycl  35358  subfaclim  35416  cvmliftlem2  35514  cvmliftlem10  35522  snmlff  35557  dfgcd3  37684  poimirlem10  37997  poimirlem23  38010  poimirlem24  38011  itg2addnclem2  38039  rrnequiv  38202  bccl2d  42476  lcmineqlem18  42531  lcmineqlem19  42532  lcmineqlem20  42533  aks4d1p1p2  42555  aks4d1p1p7  42559  aks4d1p7d1  42567  posbezout  42585  aks6d1c1  42601  aks6d1c2lem4  42612  aks6d1c2  42615  deg1gprod  42625  2np3bcnp1  42629  sticksstones6  42636  sticksstones7  42637  sticksstones22  42653  aks6d1c6lem3  42657  aks6d1c6lem4  42658  bcled  42663  bcle2d  42664  aks6d1c7lem1  42665  aks6d1c7lem2  42666  unitscyglem4  42683  fltnlta  43113  irrapxlem2  43268  irrapxlem5  43271  pellexlem1  43274  pellexlem2  43275  pellexlem5  43278  pellexlem6  43279  pell14qrgt0  43304  pell1qrge1  43315  pellfundgt1  43328  rmspecnonsq  43352  rmspecfund  43354  rmspecpos  43361  rmxypos  43392  ltrmxnn0  43394  jm2.24  43408  acongeq  43428  jm2.22  43440  jm2.23  43441  jm2.27a  43450  jm2.27c  43452  nzprmdif  44763  bccbc  44789  binomcxplemnn0  44793  fsumnncl  46017  mccllem  46042  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnmul  46386  dvnprodlem1  46389  stoweidlem24  46467  wallispilem4  46511  wallispilem5  46512  wallispi2lem1  46514  stirlinglem4  46520  stirlinglem5  46521  stirlinglem10  46526  stirlinglem15  46531  stirlingr  46533  fourierdlem48  46597  fourierdlem49  46598  fourierdlem92  46641  sqwvfoura  46671  elaa2lem  46676  etransclem19  46696  etransclem23  46700  etransclem27  46704  etransclem44  46721  rrndistlt  46733  chnsubseqwl  47324  modlt0b  47832  oexpnegALTV  48168  perfectALTVlem2  48213  gpgedgvtx0  48552  gpgedgvtx1  48553  blennn  49066  dignn0ldlem  49093  dig2nn1st  49096  digexp  49098  dignn0flhalf  49109  itcovalt2lem2lem1  49164