Theorem absge0d 15391

Description: Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

Ref	Expression
abscld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
absge0d	⊢ (𝜑 → 0 ≤ (abs‘𝐴))

Proof of Theorem absge0d

Step	Hyp	Ref	Expression
1		abscld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		absge0 15234	. 2 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ (abs‘𝐴))

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  ‘cfv 6544  ℂcc 11108  0cc0 11110   ≤ cle 11249  abscabs 15181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183

This theorem is referenced by:  lo1bddrp  15469  mulcn2  15540  o1mul  15559  o1rlimmul  15563  o1fsum  15759  cvgcmpce  15764  explecnv  15811  cvgrat  15829  mertenslem1  15830  mertenslem2  15831  efcllem  16021  eftlub  16052  sqnprm  16639  gzrngunitlem  21010  blcvx  24314  cnheibor  24471  cphsqrtcl2  24703  ipcau2  24751  trirn  24917  rrxdstprj1  24926  mbfi1fseqlem6  25238  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgabs  25352  bddmulibl  25356  bddiblnc  25359  itgcn  25362  dvlip  25510  dvlipcn  25511  dveq0  25517  dv11cn  25518  plyeq0lem  25724  aalioulem3  25847  mtest  25916  radcnvlem1  25925  radcnvlem2  25926  radcnvlt1  25930  dvradcnv  25933  pserulm  25934  psercnlem2  25936  psercnlem1  25937  pserdvlem1  25939  pserdv  25941  abelthlem5  25947  abelthlem7  25950  abelthlem8  25951  tanregt0  26048  efif1olem3  26053  argregt0  26118  argrege0  26119  logtayllem  26167  logtayl  26168  abscxpbnd  26261  heron  26343  efrlim  26474  rlimcxp  26478  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  ftalem1  26577  ftalem4  26580  ftalem5  26581  lgsdirprm  26834  lgsdilem2  26836  lgsne0  26838  2sqblem  26934  dchrisumlem2  26993  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrisum0flblem1  27011  dchrisum0lem2a  27020  mudivsum  27033  mulogsumlem  27034  mulog2sumlem2  27038  selberglem2  27049  selberg3lem2  27061  pntrsumbnd  27069  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntleml  27114  smcnlem  29981  nmoub3i  30057  nmfnge0  31211  sqsscirc2  32920  dnibndlem11  35412  knoppcnlem4  35420  unblimceq0lem  35430  unblimceq0  35431  knoppndvlem11  35446  knoppndvlem18  35453  mblfinlem2  36574  iblabsnc  36600  iblmulc2nc  36601  itgabsnc  36605  ftc1anclem2  36610  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  ftc2nc  36618  dvasin  36620  areacirclem1  36624  areacirclem2  36625  areacirclem4  36627  areacirclem5  36628  areacirc  36629  cntotbnd  36712  rrndstprj1  36746  rrndstprj2  36747  ismrer1  36754  pell14qrgt0  41645  radcnvrat  43121  dvconstbi  43141  binomcxplemnotnn0  43163  abslt2sqd  44118  dvdivbd  44687  dvbdfbdioolem1  44692  dvbdfbdioolem2  44693  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  fourierdlem30  44901  fourierdlem39  44910  fourierdlem47  44917  fourierdlem73  44943  fourierdlem77  44947  fourierdlem87  44957  etransclem23  45021  rrndistlt  45054  smfmullem1  45555  smfmullem2  45556  smfmullem3  45557