Theorem absidd 15461

Description: A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
resqrcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resqrcld.2	⊢ (𝜑 → 0 ≤ 𝐴)

Assertion

Ref	Expression
absidd	⊢ (𝜑 → (abs‘𝐴) = 𝐴)

Proof of Theorem absidd

Step	Hyp	Ref	Expression
1		resqrcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resqrcld.2	. 2 ⊢ (𝜑 → 0 ≤ 𝐴)
3		absid 15335	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (abs‘𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  ‘cfv 6561  ℝcr 11154  0cc0 11155   ≤ cle 11296  abscabs 15273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-seq 14043  df-exp 14103  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275

This theorem is referenced by:  rlimno1  15690  iseralt  15721  cvgcmpce  15854  divrcnv  15888  geomulcvg  15912  cvgrat  15919  mertenslem2  15921  eftabs  16111  efcllem  16113  efaddlem  16129  eftlub  16145  eflegeo  16157  ef01bndlem  16220  absef  16233  efieq1re  16235  dvdseq  16351  divalg2  16442  nn0gcdid0  16558  absmulgcd  16586  nn0rppwr  16598  nn0expgcd  16601  lcmgcdlem  16643  mulgcddvds  16692  phibndlem  16807  dfphi2  16811  mul4sqlem  16991  4sqlem11  16993  prmirredlem  21483  prmirred  21485  blcvx  24819  reperflem  24840  reconnlem2  24849  nmoleub2lem3  25148  nmoleub3  25152  tcphcphlem1  25269  iscmet3lem3  25324  pjthlem1  25471  lhop1lem  26052  ftc1lem4  26080  plyeq0lem  26249  aalioulem4  26377  mtest  26447  radcnvlem1  26456  radcnvlt1  26461  radcnvle  26463  dvradcnv  26464  pserdvlem2  26472  abelth2  26486  tanabsge  26548  sineq0  26566  divlogrlim  26677  logcnlem3  26686  logcnlem4  26687  logtayllem  26701  logtayl  26702  abscxp2  26735  logbgcd1irr  26837  chordthmlem4  26878  rlimcnp  27008  lgamgulmlem2  27073  lgamgulmlem5  27076  lgamcvg2  27098  ftalem5  27120  lgsval2lem  27351  lgsval4a  27363  2sqlem3  27464  chebbnd1  27516  chtppilimlem2  27518  chto1ub  27520  vmadivsum  27526  vmadivsumb  27527  rpvmasumlem  27531  dchrisumlem2  27534  dchrisumlem3  27535  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0fno1  27555  dchrisum0re  27557  rplogsum  27571  mulog2sumlem1  27578  mulog2sumlem2  27579  2vmadivsumlem  27584  selbergb  27593  selberg2lem  27594  selberg2b  27596  selberg3lem1  27601  selberg3lem2  27602  selberg4lem1  27604  pntrsumo1  27609  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntibndlem2  27635  ostth2  27681  htthlem  30936  bcsiALT  31198  norm1  31268  pjhthlem1  31410  nmbdoplbi  32043  nmcexi  32045  nmcopexi  32046  nmcoplbi  32047  nmbdfnlbi  32068  nmcfnexi  32070  nmcfnlbi  32071  cnlnadjlem7  32092  nmopcoi  32114  nmopcoadji  32120  branmfn  32124  strlem1  32269  subfaclim  35193  dnizphlfeqhlf  36477  dnibndlem6  36484  dnibndlem9  36487  knoppndvlem11  36523  knoppndvlem14  36526  poimirlem29  37656  ftc1cnnclem  37698  ftc1anclem5  37704  lmclim2  37765  geomcau  37766  cntotbnd  37803  gcdnn0id  42364  readvrec  42392  irrapxlem2  42834  irrapxlem5  42837  pellexlem2  42841  oddcomabszz  42956  jm2.19  43005  jm2.26lem3  43013  absmulrposd  44172  nzprmdif  44338  0ellimcdiv  45664  stoweidlem7  46022  fourierdlem30  46152  fourierdlem39  46161  etransclem23  46272  etransclem41  46290  hoiqssbllem2  46638  blenre  48495  blennn  48496