Theorem absidd 15365

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 15238	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (abs‘𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499  ℝcr 11043  0cc0 11044   ≤ cle 11185  abscabs 15176

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9369  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-z 12506  df-uz 12770  df-rp 12928  df-seq 13943  df-exp 14003  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178

This theorem is referenced by:  nn0absid  15372  rlimno1  15596  iseralt  15627  cvgcmpce  15760  divrcnv  15794  geomulcvg  15818  cvgrat  15825  mertenslem2  15827  eftabs  16017  efcllem  16019  efaddlem  16035  eftlub  16053  eflegeo  16065  ef01bndlem  16128  absef  16141  efieq1re  16143  dvdseq  16260  divalg2  16351  nn0gcdid0  16467  absmulgcd  16495  nn0rppwr  16507  nn0expgcd  16510  lcmgcdlem  16552  mulgcddvds  16601  phibndlem  16716  dfphi2  16720  mul4sqlem  16900  4sqlem11  16902  prmirredlem  21414  prmirred  21416  blcvx  24719  reperflem  24740  reconnlem2  24749  nmoleub2lem3  25048  nmoleub3  25052  tcphcphlem1  25168  iscmet3lem3  25223  pjthlem1  25370  lhop1lem  25951  ftc1lem4  25979  plyeq0lem  26148  aalioulem4  26276  mtest  26346  radcnvlem1  26355  radcnvlt1  26360  radcnvle  26362  dvradcnv  26363  pserdvlem2  26371  abelth2  26385  tanabsge  26448  sineq0  26466  divlogrlim  26577  logcnlem3  26586  logcnlem4  26587  logtayllem  26601  logtayl  26602  abscxp2  26635  logbgcd1irr  26737  chordthmlem4  26778  rlimcnp  26908  lgamgulmlem2  26973  lgamgulmlem5  26976  lgamcvg2  26998  ftalem5  27020  lgsval2lem  27251  lgsval4a  27263  2sqlem3  27364  chebbnd1  27416  chtppilimlem2  27418  chto1ub  27420  vmadivsum  27426  vmadivsumb  27427  rpvmasumlem  27431  dchrisumlem2  27434  dchrisumlem3  27435  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0fno1  27455  dchrisum0re  27457  rplogsum  27471  mulog2sumlem1  27478  mulog2sumlem2  27479  2vmadivsumlem  27484  selbergb  27493  selberg2lem  27494  selberg2b  27496  selberg3lem1  27501  selberg3lem2  27502  selberg4lem1  27504  pntrsumo1  27509  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntibndlem2  27535  ostth2  27581  htthlem  30896  bcsiALT  31158  norm1  31228  pjhthlem1  31370  nmbdoplbi  32003  nmcexi  32005  nmcopexi  32006  nmcoplbi  32007  nmbdfnlbi  32028  nmcfnexi  32030  nmcfnlbi  32031  cnlnadjlem7  32052  nmopcoi  32074  nmopcoadji  32080  branmfn  32084  strlem1  32229  sgnval2  32708  constrdircl  33748  iconstr  33749  constrinvcl  33756  constrresqrtcl  33760  constrabscl  33761  constrsqrtcl  33762  cos9thpinconstrlem1  33772  subfaclim  35168  dnizphlfeqhlf  36457  dnibndlem6  36464  dnibndlem9  36467  knoppndvlem11  36503  knoppndvlem14  36506  poimirlem29  37636  ftc1cnnclem  37678  ftc1anclem5  37684  lmclim2  37745  geomcau  37746  cntotbnd  37783  gcdnn0id  42310  readvrec  42343  irrapxlem2  42804  irrapxlem5  42807  pellexlem2  42811  oddcomabszz  42926  jm2.19  42975  jm2.26lem3  42983  absmulrposd  44141  nzprmdif  44301  0ellimcdiv  45640  stoweidlem7  45998  fourierdlem30  46128  fourierdlem39  46137  etransclem23  46248  etransclem41  46266  hoiqssbllem2  46614  modlt0b  47357  blenre  48556  blennn  48557