Theorem absge0d 14857

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 14700	. 2 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ (abs‘𝐴))

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5035  ‘cfv 6339  ℂcc 10578  0cc0 10580   ≤ cle 10719  abscabs 14646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657  ax-pre-sup 10658

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-sup 8944  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-nn 11680  df-2 11742  df-3 11743  df-n0 11940  df-z 12026  df-uz 12288  df-rp 12436  df-seq 13424  df-exp 13485  df-cj 14511  df-re 14512  df-im 14513  df-sqrt 14647  df-abs 14648

This theorem is referenced by:  lo1bddrp  14935  mulcn2  15005  o1mul  15024  o1rlimmul  15028  o1fsum  15221  cvgcmpce  15226  explecnv  15273  cvgrat  15292  mertenslem1  15293  mertenslem2  15294  efcllem  15484  eftlub  15515  sqnprm  16103  gzrngunitlem  20236  blcvx  23504  cnheibor  23661  cphsqrtcl2  23892  ipcau2  23939  trirn  24105  rrxdstprj1  24114  mbfi1fseqlem6  24425  iblabs  24533  iblabsr  24534  iblmulc2  24535  itgabs  24539  bddmulibl  24543  bddiblnc  24546  itgcn  24549  dvlip  24697  dvlipcn  24698  dveq0  24704  dv11cn  24705  plyeq0lem  24911  aalioulem3  25034  mtest  25103  radcnvlem1  25112  radcnvlem2  25113  radcnvlt1  25117  dvradcnv  25120  pserulm  25121  psercnlem2  25123  psercnlem1  25124  pserdvlem1  25126  pserdv  25128  abelthlem5  25134  abelthlem7  25137  abelthlem8  25138  tanregt0  25235  efif1olem3  25240  argregt0  25305  argrege0  25306  logtayllem  25354  logtayl  25355  abscxpbnd  25446  heron  25528  efrlim  25659  rlimcxp  25663  lgamgulmlem2  25719  lgamgulmlem3  25720  lgamgulmlem5  25722  ftalem1  25762  ftalem4  25765  ftalem5  25766  lgsdirprm  26019  lgsdilem2  26021  lgsne0  26023  2sqblem  26119  dchrisumlem2  26178  dchrmusum2  26182  dchrvmasumlem2  26186  dchrvmasumlem3  26187  dchrvmasumiflem1  26189  dchrisum0flblem1  26196  dchrisum0lem2a  26205  mudivsum  26218  mulogsumlem  26219  mulog2sumlem2  26223  selberglem2  26234  selberg3lem2  26246  pntrsumbnd  26254  pntrlog2bndlem1  26265  pntrlog2bndlem2  26266  pntrlog2bndlem3  26267  pntrlog2bndlem5  26269  pntrlog2bndlem6  26271  pntrlog2bnd  26272  pntleml  26299  smcnlem  28584  nmoub3i  28660  nmfnge0  29814  sqsscirc2  31384  dnibndlem11  34243  knoppcnlem4  34251  unblimceq0lem  34261  unblimceq0  34262  knoppndvlem11  34277  knoppndvlem18  34284  mblfinlem2  35401  iblabsnc  35427  iblmulc2nc  35428  itgabsnc  35432  ftc1anclem2  35437  ftc1anclem4  35439  ftc1anclem5  35440  ftc1anclem6  35441  ftc1anclem7  35442  ftc1anclem8  35443  ftc1anc  35444  ftc2nc  35445  dvasin  35447  areacirclem1  35451  areacirclem2  35452  areacirclem4  35454  areacirclem5  35455  areacirc  35456  cntotbnd  35540  rrndstprj1  35574  rrndstprj2  35575  ismrer1  35582  pell14qrgt0  40201  radcnvrat  41419  dvconstbi  41439  binomcxplemnotnn0  41461  abslt2sqd  42388  dvdivbd  42959  dvbdfbdioolem1  42964  dvbdfbdioolem2  42965  ioodvbdlimc1lem1  42967  ioodvbdlimc1lem2  42968  ioodvbdlimc2lem  42970  fourierdlem30  43173  fourierdlem39  43182  fourierdlem47  43189  fourierdlem73  43215  fourierdlem77  43219  fourierdlem87  43229  etransclem23  43293  rrndistlt  43326  smfmullem1  43817  smfmullem2  43818  smfmullem3  43819