Theorem nn0ge0d 9333

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

Syntax hints:   → wi 4   ∈ wcel 2175   class class class wbr 4043  0cc0 7907   ≤ cle 8090  ℕ₀cn0 9277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1cn 8000  ax-1re 8001  ax-icn 8002  ax-addcl 8003  ax-addrcl 8004  ax-mulcl 8005  ax-i2m1 8012  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-xp 4679  df-cnv 4681  df-iota 5229  df-fv 5276  df-ov 5937  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-inn 9019  df-n0 9278

This theorem is referenced by:  flqmulnn0  10423  zmodfz  10472  addmodid  10498  modifeq2int  10512  modaddmodlo  10514  modsumfzodifsn  10522  addmodlteq  10524  expnnval  10668  nn0le2msqd  10845  facwordi  10866  faclbnd  10867  faclbnd6  10870  facavg  10872  geolim2  11742  mertenslemi1  11765  eftabs  11886  efcllemp  11888  efaddlem  11904  eftlub  11920  oexpneg  12107  divalglemnn  12148  divalglemnqt  12150  divalglemeunn  12151  divalg2  12156  bitsfzolem  12184  bitsmod  12186  dfgcd2  12254  gcdmultiple  12260  gcdmultiplez  12261  dvdssqlem  12270  nn0seqcvgd  12282  mulgcddvds  12335  isprm5lem  12382  nn0sqrtelqelz  12447  nonsq  12448  phibndlem  12457  dfphi2  12461  modprm0  12496  pythagtriplem3  12509  pythagtriplem10  12511  pythagtriplem6  12512  pythagtriplem7  12513  pythagtriplem12  12517  pythagtriplem14  12519  pcge0  12555  pcprmpw2  12575  pcmptdvds  12587  fldivp1  12590  pcbc  12593  qexpz  12594  pockthlem  12598  pockthg  12599  mul4sqlem  12635  4sqlem12  12644  4sqlem14  12646  4sqlem16  12648  2expltfac  12681  ennnfoneleminc  12701  logbgcd1irraplemexp  15358  wilthlem1  15370  perfectlem2  15390  lgsval2lem  15405  lgsval4a  15417  gausslemma2dlem0c  15446  gausslemma2dlem0d  15447  lgseisenlem1  15465  lgseisenlem2  15466  lgsquadlem1  15472  2lgslem1a1  15481  2sqlem3  15512  2sqlem7  15516  2sqlem8  15518