Theorem nn0ge0d 12710

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 12671	. 2 ⊢ (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → 0 ≤ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  0cc0 11239   ≤ cle 11383  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376  df-n0 12647

This theorem is used by:  flmulnn0  14007  zmodfz  14073  modaddmodlo  14118  modsumfzodifsn  14127  addmodlteq  14129  expmulnbnd  14420  facwordi  14474  faclbnd  14475  faclbnd4lem3  14480  faclbnd6  14484  facavg  14486  hashdom  14564  climcnds  16064  geomulcvg  16089  mertenslem1  16097  eftabs  16285  efcllem  16287  efaddlem  16303  eftlub  16321  oexpneg  16559  divalg2  16619  bitsfzolem  16648  bitsmod  16650  sadcaddlem  16671  sadaddlem  16680  sadasslem  16684  sadeq  16686  smueqlem  16704  dfgcd2  16763  nn0seqcvgd  16789  mulgcddvds  16874  isprm5  16927  zsqrtelqelz  16978  phibndlem  16991  dfphi2  16995  pythagtriplem3  17040  pythagtriplem10  17042  pythagtriplem6  17043  pythagtriplem7  17044  pythagtriplem12  17048  pythagtriplem14  17050  iserodd  17057  pcge0  17084  pcprmpw2  17104  pcmptdvds  17116  fldivp1  17119  pcbc  17122  qexpz  17123  pockthlem  17127  pockthg  17128  prmreclem3  17140  mul4sqlem  17175  4sqlem12  17178  4sqlem14  17180  4sqlem16  17182  0ram  17242  ram0  17244  ramcl  17251  prmolefac  17268  2expltfac  17314  odmodnn0  19805  pgpfi  19870  ablfac1c  20338  prmirred  21835  psrbaglesupp  22285  psrbagcon  22288  psrlidm  22324  psdmul  22542  coe1tmmul2  22650  lebnumii  25342  mbfi1fseqlem1  26091  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  itg2cnlem2  26138  fta1g  26543  coemulhi  26628  dgradd2  26642  dgrco  26649  aareccl  26710  aaliou3lem8  26729  radcnvlem1  26797  dvradcnv  26805  dmlogdmgm  27408  wilthlem1  27452  sgmmul  27585  chtublem  27595  fsumvma2  27598  chpchtsum  27603  perfectlem2  27614  bcmono  27661  bposlem5  27672  lgsval2lem  27691  lgsval4a  27703  lgsqrlem2  27731  gausslemma2dlem0c  27742  gausslemma2dlem0d  27743  lgseisenlem1  27759  lgseisenlem2  27760  lgsquadlem1  27764  2lgslem1a1  27773  2sqlem3  27804  2sqlem7  27808  2sqlem8  27810  2sqblem  27815  2sqmod  27820  2sqreunnlem1  27833  dchrisum0re  27897  pntrlog2bndlem4  27964  pntpbnd1a  27969  ostth2lem2  28018  ostth2lem3  28019  ostth2  28021  crctcshwlkn0lem4  30459  wwlksubclwwlk  30706  nnmulge  33427  nndiffz1  33474  fzo0opth  33491  nexple  33520  pfxlsw2ccat  33609  wrdt2ind  33612  gsumwrd2dccatlem  33737  ply1unit  34210  selvply1rhmlemb  34262  mplmulmvr  34282  esplyind  34318  constrdircl  34508  iconstr  34509  submateqlem1  34550  oddpwdc  35097  eulerpartlems  35103  eulerpartlemgc  35105  eulerpartlemb  35111  fsum2dsub  35347  breprexplemc  35372  circlemeth  35380  tgoldbachgtde  35400  usgrgt2cycl  36107  subfaclim  36161  cvmliftlem2  36259  cvmliftlem10  36267  snmlff  36302  dfgcd3  38513  poimirlem10  38816  poimirlem23  38829  poimirlem24  38830  itg2addnclem2  38858  rrnequiv  39035  bccl2d  43307  lcmineqlem18  43362  lcmineqlem19  43363  lcmineqlem20  43364  aks4d1p1p2  43386  aks4d1p1p7  43390  aks4d1p7d1  43398  posbezout  43416  aks6d1c1  43432  aks6d1c2lem4  43443  aks6d1c2  43446  deg1gprod  43456  2np3bcnp1  43460  sticksstones6  43467  sticksstones7  43468  sticksstones22  43484  aks6d1c6lem3  43488  aks6d1c6lem4  43489  bcled  43494  bcle2d  43495  aks6d1c7lem1  43496  aks6d1c7lem2  43497  unitscyglem4  43514  fltnlta  43940  irrapxlem2  44096  irrapxlem5  44099  pellexlem1  44102  pellexlem2  44103  pellexlem5  44106  pellexlem6  44107  pell14qrgt0  44132  pell1qrge1  44143  pellfundgt1  44156  rmspecnonsq  44180  rmspecfund  44182  rmspecpos  44189  rmxypos  44220  ltrmxnn0  44222  jm2.24  44236  acongeq  44256  jm2.22  44268  jm2.23  44269  jm2.27a  44278  jm2.27c  44280  nzprmdif  45564  bccbc  45590  binomcxplemnn0  45594  fsumnncl  46857  mccllem  46882  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  dvnmul  47226  dvnprodlem1  47229  stoweidlem24  47307  wallispilem4  47351  wallispilem5  47352  wallispi2lem1  47354  stirlinglem4  47360  stirlinglem5  47361  stirlinglem10  47366  stirlinglem15  47371  stirlingr  47373  fourierdlem48  47437  fourierdlem49  47438  fourierdlem92  47481  sqwvfoura  47511  elaa2lem  47516  etransclem19  47536  etransclem23  47540  etransclem27  47544  etransclem44  47561  rrndistlt  47573  chnsubseqwl  48162  modlt0b  48712  oexpnegALTV  49048  perfectALTVlem2  49093  gpgedgvtx0  49432  gpgedgvtx1  49433  blennn  50018  dignn0ldlem  50045  dig2nn1st  50048  digexp  50050  dignn0flhalf  50061  itcovalt2lem2lem1  50116