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  21358  prmirred  21360  blcvx  24662  reperflem  24683  reconnlem2  24692  nmoleub2lem3  24991  nmoleub3  24995  tcphcphlem1  25111  iscmet3lem3  25166  pjthlem1  25313  lhop1lem  25894  ftc1lem4  25922  plyeq0lem  26091  aalioulem4  26219  mtest  26289  radcnvlem1  26298  radcnvlt1  26303  radcnvle  26305  dvradcnv  26306  pserdvlem2  26314  abelth2  26328  tanabsge  26391  sineq0  26409  divlogrlim  26520  logcnlem3  26529  logcnlem4  26530  logtayllem  26544  logtayl  26545  abscxp2  26578  logbgcd1irr  26680  chordthmlem4  26721  rlimcnp  26851  lgamgulmlem2  26916  lgamgulmlem5  26919  lgamcvg2  26941  ftalem5  26963  lgsval2lem  27194  lgsval4a  27206  2sqlem3  27307  chebbnd1  27359  chtppilimlem2  27361  chto1ub  27363  vmadivsum  27369  vmadivsumb  27370  rpvmasumlem  27374  dchrisumlem2  27377  dchrisumlem3  27378  dchrvmasumlem2  27385  dchrvmasumiflem1  27388  dchrisum0fno1  27398  dchrisum0re  27400  rplogsum  27414  mulog2sumlem1  27421  mulog2sumlem2  27422  2vmadivsumlem  27427  selbergb  27436  selberg2lem  27437  selberg2b  27439  selberg3lem1  27444  selberg3lem2  27445  selberg4lem1  27447  pntrsumo1  27452  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntpbnd1a  27472  pntpbnd1  27473  pntibndlem2  27478  ostth2  27524  htthlem  30819  bcsiALT  31081  norm1  31151  pjhthlem1  31293  nmbdoplbi  31926  nmcexi  31928  nmcopexi  31929  nmcoplbi  31930  nmbdfnlbi  31951  nmcfnexi  31953  nmcfnlbi  31954  cnlnadjlem7  31975  nmopcoi  31997  nmopcoadji  32003  branmfn  32007  strlem1  32152  sgnval2  32631  constrdircl  33728  iconstr  33729  constrinvcl  33736  constrresqrtcl  33740  constrabscl  33741  constrsqrtcl  33742  cos9thpinconstrlem1  33752  subfaclim  35148  dnizphlfeqhlf  36437  dnibndlem6  36444  dnibndlem9  36447  knoppndvlem11  36483  knoppndvlem14  36486  poimirlem29  37616  ftc1cnnclem  37658  ftc1anclem5  37664  lmclim2  37725  geomcau  37726  cntotbnd  37763  gcdnn0id  42290  readvrec  42323  irrapxlem2  42784  irrapxlem5  42787  pellexlem2  42791  oddcomabszz  42906  jm2.19  42955  jm2.26lem3  42963  absmulrposd  44121  nzprmdif  44281  0ellimcdiv  45620  stoweidlem7  45978  fourierdlem30  46108  fourierdlem39  46117  etransclem23  46228  etransclem41  46246  hoiqssbllem2  46594  modlt0b  47337  blenre  48536  blennn  48537