Theorem absge0d 15387

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  ‘cfv 6540  ℂcc 11104  0cc0 11106   ≤ cle 11245  abscabs 15177

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-sup 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179

This theorem is referenced by:  lo1bddrp  15465  mulcn2  15536  o1mul  15555  o1rlimmul  15559  o1fsum  15755  cvgcmpce  15760  explecnv  15807  cvgrat  15825  mertenslem1  15826  mertenslem2  15827  efcllem  16017  eftlub  16048  sqnprm  16635  gzrngunitlem  21002  blcvx  24305  cnheibor  24462  cphsqrtcl2  24694  ipcau2  24742  trirn  24908  rrxdstprj1  24917  mbfi1fseqlem6  25229  iblabs  25337  iblabsr  25338  iblmulc2  25339  itgabs  25343  bddmulibl  25347  bddiblnc  25350  itgcn  25353  dvlip  25501  dvlipcn  25502  dveq0  25508  dv11cn  25509  plyeq0lem  25715  aalioulem3  25838  mtest  25907  radcnvlem1  25916  radcnvlem2  25917  radcnvlt1  25921  dvradcnv  25924  pserulm  25925  psercnlem2  25927  psercnlem1  25928  pserdvlem1  25930  pserdv  25932  abelthlem5  25938  abelthlem7  25941  abelthlem8  25942  tanregt0  26039  efif1olem3  26044  argregt0  26109  argrege0  26110  logtayllem  26158  logtayl  26159  abscxpbnd  26250  heron  26332  efrlim  26463  rlimcxp  26467  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamgulmlem5  26526  ftalem1  26566  ftalem4  26569  ftalem5  26570  lgsdirprm  26823  lgsdilem2  26825  lgsne0  26827  2sqblem  26923  dchrisumlem2  26982  dchrmusum2  26986  dchrvmasumlem2  26990  dchrvmasumlem3  26991  dchrvmasumiflem1  26993  dchrisum0flblem1  27000  dchrisum0lem2a  27009  mudivsum  27022  mulogsumlem  27023  mulog2sumlem2  27027  selberglem2  27038  selberg3lem2  27050  pntrsumbnd  27058  pntrlog2bndlem1  27069  pntrlog2bndlem2  27070  pntrlog2bndlem3  27071  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  pntrlog2bnd  27076  pntleml  27103  smcnlem  29937  nmoub3i  30013  nmfnge0  31167  sqsscirc2  32877  dnibndlem11  35352  knoppcnlem4  35360  unblimceq0lem  35370  unblimceq0  35371  knoppndvlem11  35386  knoppndvlem18  35393  mblfinlem2  36514  iblabsnc  36540  iblmulc2nc  36541  itgabsnc  36545  ftc1anclem2  36550  ftc1anclem4  36552  ftc1anclem5  36553  ftc1anclem6  36554  ftc1anclem7  36555  ftc1anclem8  36556  ftc1anc  36557  ftc2nc  36558  dvasin  36560  areacirclem1  36564  areacirclem2  36565  areacirclem4  36567  areacirclem5  36568  areacirc  36569  cntotbnd  36652  rrndstprj1  36686  rrndstprj2  36687  ismrer1  36694  pell14qrgt0  41582  radcnvrat  43058  dvconstbi  43078  binomcxplemnotnn0  43100  abslt2sqd  44056  dvdivbd  44625  dvbdfbdioolem1  44630  dvbdfbdioolem2  44631  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  fourierdlem30  44839  fourierdlem39  44848  fourierdlem47  44855  fourierdlem73  44881  fourierdlem77  44885  fourierdlem87  44895  etransclem23  44959  rrndistlt  44992  smfmullem1  45493  smfmullem2  45494  smfmullem3  45495