Theorem absge0d 15476

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

Syntax hints:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6523  ℂcc 11073  0cc0 11075   ≤ cle 11219  abscabs 15263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-sup 9390  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-n0 12484  df-z 12571  df-uz 12842  df-rp 12996  df-seq 14017  df-exp 14077  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265

This theorem is referenced by:  lo1bddrp  15554  mulcn2  15625  o1mul  15644  o1rlimmul  15648  o1fsum  15843  cvgcmpce  15848  explecnv  15897  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  efcllem  16109  eftlub  16143  sqnprm  16739  gzrngunitlem  21486  blcvx  24860  cnheibor  25019  cphsqrtcl2  25250  ipcau2  25298  trirn  25464  rrxdstprj1  25473  mbfi1fseqlem6  25784  iblabs  25893  iblabsr  25894  iblmulc2  25895  itgabs  25899  bddmulibl  25903  bddiblnc  25906  itgcn  25909  dvlip  26057  dvlipcn  26058  dveq0  26064  dv11cn  26065  plyeq0lem  26272  aalioulem3  26400  mtest  26469  radcnvlem1  26478  radcnvlem2  26479  radcnvlt1  26483  dvradcnv  26486  pserulm  26487  psercnlem2  26489  psercnlem1  26490  pserdvlem1  26492  pserdv  26494  abelthlem5  26500  abelthlem7  26503  abelthlem8  26504  tanregt0  26606  efif1olem3  26611  argregt0  26677  argrege0  26678  logtayllem  26726  logtayl  26727  abscxpbnd  26820  heron  26905  efrlim  27036  rlimcxp  27040  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamgulmlem5  27099  ftalem1  27139  ftalem4  27142  ftalem5  27143  lgsdirprm  27397  lgsdilem2  27399  lgsne0  27401  2sqblem  27497  dchrisumlem2  27556  dchrmusum2  27560  dchrvmasumlem2  27564  dchrvmasumlem3  27565  dchrvmasumiflem1  27567  dchrisum0flblem1  27574  dchrisum0lem2a  27583  mudivsum  27596  mulogsumlem  27597  mulog2sumlem2  27601  selberglem2  27612  selberg3lem2  27624  pntrsumbnd  27632  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntrlog2bnd  27650  pntleml  27677  smcnlem  30902  nmoub3i  30978  nmfnge0  32132  iconstr  34065  constrinvcl  34072  constrabscl  34077  constrsqrtcl  34078  sqsscirc2  34208  dnibndlem11  36931  knoppcnlem4  36939  unblimceq0lem  36949  unblimceq0  36950  knoppndvlem11  36965  knoppndvlem18  36972  mblfinlem2  38162  iblabsnc  38188  iblmulc2nc  38189  itgabsnc  38193  ftc1anclem2  38198  ftc1anclem4  38200  ftc1anclem5  38201  ftc1anclem6  38202  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  ftc2nc  38206  dvasin  38208  areacirclem1  38212  areacirclem2  38213  areacirclem4  38215  areacirclem5  38216  areacirc  38217  cntotbnd  38300  rrndstprj1  38334  rrndstprj2  38335  ismrer1  38342  pell14qrgt0  43441  radcnvrat  44895  dvconstbi  44915  binomcxplemnotnn0  44937  abslt2sqd  45941  dvdivbd  46502  dvbdfbdioolem1  46507  dvbdfbdioolem2  46508  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  fourierdlem30  46716  fourierdlem39  46725  fourierdlem47  46732  fourierdlem73  46758  fourierdlem77  46762  fourierdlem87  46772  etransclem23  46836  rrndistlt  46869  smfmullem1  47370  smfmullem2  47371  smfmullem3  47372