Theorem absge0d 15614

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6538  ℂcc 11198  0cc0 11200   ≤ cle 11344  abscabs 15401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-sup 9434  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-rp 13121  df-seq 14145  df-exp 14205  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403

This theorem is used by:  lo1bddrp  15692  mulcn2  15763  o1mul  15782  o1rlimmul  15786  o1fsum  15980  cvgcmpce  15985  explecnv  16034  cvgrat  16052  mertenslem1  16053  mertenslem2  16054  efcllem  16243  eftlub  16277  sqnprm  16878  gzrngunitlem  21738  blcvx  25117  cnheibor  25276  cphsqrtcl2  25507  ipcau2  25555  trirn  25721  rrxdstprj1  25730  mbfi1fseqlem6  26041  iblabs  26149  iblabsr  26150  iblmulc2  26151  itgabs  26155  bddmulibl  26159  bddiblnc  26162  itgcn  26165  dvlip  26313  dvlipcn  26314  dveq0  26320  dv11cn  26321  plyeq0lem  26529  aalioulem3  26661  mtest  26731  radcnvlem1  26740  radcnvlem2  26741  radcnvlt1  26745  dvradcnv  26748  pserulm  26749  psercnlem2  26751  psercnlem1  26752  pserdvlem1  26754  pserdv  26756  abelthlem5  26762  abelthlem7  26765  abelthlem8  26766  tanregt0  26867  efif1olem3  26872  argregt0  26938  argrege0  26939  logtayllem  26987  logtayl  26988  abscxpbnd  27081  heron  27166  efrlim  27297  rlimcxp  27301  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem5  27360  ftalem1  27400  ftalem4  27403  ftalem5  27404  lgsdirprm  27658  lgsdilem2  27660  lgsne0  27662  2sqblem  27758  dchrisumlem2  27817  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumlem3  27826  dchrvmasumiflem1  27828  dchrisum0flblem1  27835  dchrisum0lem2a  27844  mudivsum  27857  mulogsumlem  27858  mulog2sumlem2  27862  selberglem2  27873  selberg3lem2  27885  pntrsumbnd  27893  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntleml  27938  smcnlem  31299  nmoub3i  31375  nmfnge0  32529  iconstr  34398  constrinvcl  34405  constrabscl  34410  constrsqrtcl  34411  sqsscirc2  34541  dnibndlem11  37354  knoppcnlem4  37362  unblimceq0lem  37372  unblimceq0  37373  knoppndvlem11  37388  knoppndvlem18  37395  mblfinlem2  38577  iblabsnc  38603  iblmulc2nc  38604  itgabsnc  38608  ftc1anclem2  38613  ftc1anclem4  38615  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  ftc2nc  38621  dvasin  38623  areacirclem1  38627  areacirclem2  38628  areacirclem4  38630  areacirclem5  38631  areacirc  38632  cntotbnd  38731  rrndstprj1  38765  rrndstprj2  38766  ismrer1  38773  pell14qrgt0  43866  radcnvrat  45298  dvconstbi  45318  binomcxplemnotnn0  45340  abslt2sqd  46372  dvdivbd  46933  dvbdfbdioolem1  46938  dvbdfbdioolem2  46939  ioodvbdlimc1lem1  46941  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  fourierdlem30  47147  fourierdlem39  47156  fourierdlem47  47163  fourierdlem73  47189  fourierdlem77  47193  fourierdlem87  47203  etransclem23  47267  rrndistlt  47300  smfmullem1  47801  smfmullem2  47802  smfmullem3  47803