Theorem absge0d 15404

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6494  ℂcc 11031  0cc0 11033   ≤ cle 11175  abscabs 15191

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-pre-sup 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7813  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-sup 9350  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-nn 12170  df-2 12239  df-3 12240  df-n0 12433  df-z 12520  df-uz 12784  df-rp 12938  df-seq 13959  df-exp 14019  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193

This theorem is referenced by:  lo1bddrp  15482  mulcn2  15553  o1mul  15572  o1rlimmul  15576  o1fsum  15771  cvgcmpce  15776  explecnv  15825  cvgrat  15843  mertenslem1  15844  mertenslem2  15845  efcllem  16037  eftlub  16071  sqnprm  16667  gzrngunitlem  21426  blcvx  24777  cnheibor  24936  cphsqrtcl2  25167  ipcau2  25215  trirn  25381  rrxdstprj1  25390  mbfi1fseqlem6  25701  iblabs  25810  iblabsr  25811  iblmulc2  25812  itgabs  25816  bddmulibl  25820  bddiblnc  25823  itgcn  25826  dvlip  25974  dvlipcn  25975  dveq0  25981  dv11cn  25982  plyeq0lem  26189  aalioulem3  26315  mtest  26386  radcnvlem1  26395  radcnvlem2  26396  radcnvlt1  26400  dvradcnv  26403  pserulm  26404  psercnlem2  26406  psercnlem1  26407  pserdvlem1  26409  pserdv  26411  abelthlem5  26417  abelthlem7  26420  abelthlem8  26421  tanregt0  26520  efif1olem3  26525  argregt0  26591  argrege0  26592  logtayllem  26640  logtayl  26641  abscxpbnd  26734  heron  26819  efrlim  26950  efrlimOLD  26951  rlimcxp  26955  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  ftalem1  27054  ftalem4  27057  ftalem5  27058  lgsdirprm  27312  lgsdilem2  27314  lgsne0  27316  2sqblem  27412  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0lem2a  27498  mudivsum  27511  mulogsumlem  27512  mulog2sumlem2  27516  selberglem2  27527  selberg3lem2  27539  pntrsumbnd  27547  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntleml  27592  smcnlem  30787  nmoub3i  30863  nmfnge0  32017  iconstr  33930  constrinvcl  33937  constrabscl  33942  constrsqrtcl  33943  sqsscirc2  34073  dnibndlem11  36768  knoppcnlem4  36776  unblimceq0lem  36786  unblimceq0  36787  knoppndvlem11  36802  knoppndvlem18  36809  mblfinlem2  37997  iblabsnc  38023  iblmulc2nc  38024  itgabsnc  38028  ftc1anclem2  38033  ftc1anclem4  38035  ftc1anclem5  38036  ftc1anclem6  38037  ftc1anclem7  38038  ftc1anclem8  38039  ftc1anc  38040  ftc2nc  38041  dvasin  38043  areacirclem1  38047  areacirclem2  38048  areacirclem4  38050  areacirclem5  38051  areacirc  38052  cntotbnd  38135  rrndstprj1  38169  rrndstprj2  38170  ismrer1  38177  pell14qrgt0  43309  radcnvrat  44763  dvconstbi  44783  binomcxplemnotnn0  44805  abslt2sqd  45812  dvdivbd  46373  dvbdfbdioolem1  46378  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  fourierdlem30  46587  fourierdlem39  46596  fourierdlem47  46603  fourierdlem73  46629  fourierdlem77  46633  fourierdlem87  46643  etransclem23  46707  rrndistlt  46740  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243