Theorem absidd 15379

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493  ℝcr 11031  0cc0 11032   ≤ cle 11174  abscabs 15190

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-sup 9349  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-n0 12432  df-z 12519  df-uz 12783  df-rp 12937  df-seq 13958  df-exp 14018  df-cj 15055  df-re 15056  df-im 15057  df-sqrt 15191  df-abs 15192

This theorem is referenced by:  nn0absid  15386  rlimno1  15610  iseralt  15641  cvgcmpce  15775  divrcnv  15811  geomulcvg  15835  cvgrat  15842  mertenslem2  15844  eftabs  16034  efcllem  16036  efaddlem  16052  eftlub  16070  eflegeo  16082  ef01bndlem  16145  absef  16158  efieq1re  16160  dvdseq  16277  divalg2  16368  nn0gcdid0  16484  absmulgcd  16512  nn0rppwr  16524  nn0expgcd  16527  lcmgcdlem  16569  mulgcddvds  16618  phibndlem  16734  dfphi2  16738  mul4sqlem  16918  4sqlem11  16920  prmirredlem  21465  prmirred  21467  blcvx  24776  reperflem  24797  reconnlem2  24806  nmoleub2lem3  25095  nmoleub3  25099  tcphcphlem1  25215  iscmet3lem3  25270  pjthlem1  25417  lhop1lem  25993  ftc1lem4  26019  plyeq0lem  26188  aalioulem4  26315  mtest  26385  radcnvlem1  26394  radcnvlt1  26399  radcnvle  26401  dvradcnv  26402  pserdvlem2  26409  abelth2  26423  tanabsge  26486  sineq0  26504  divlogrlim  26615  logcnlem3  26624  logcnlem4  26625  logtayllem  26639  logtayl  26640  abscxp2  26673  logbgcd1irr  26774  chordthmlem4  26815  rlimcnp  26945  lgamgulmlem2  27010  lgamgulmlem5  27013  lgamcvg2  27035  ftalem5  27057  lgsval2lem  27287  lgsval4a  27299  2sqlem3  27400  chebbnd1  27452  chtppilimlem2  27454  chto1ub  27456  vmadivsum  27462  vmadivsumb  27463  rpvmasumlem  27467  dchrisumlem2  27470  dchrisumlem3  27471  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0fno1  27491  dchrisum0re  27493  rplogsum  27507  mulog2sumlem1  27514  mulog2sumlem2  27515  2vmadivsumlem  27520  selbergb  27529  selberg2lem  27530  selberg2b  27532  selberg3lem1  27537  selberg3lem2  27538  selberg4lem1  27540  pntrsumo1  27545  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd1  27566  pntibndlem2  27571  ostth2  27617  htthlem  31006  bcsiALT  31268  norm1  31338  pjhthlem1  31480  nmbdoplbi  32113  nmcexi  32115  nmcopexi  32116  nmcoplbi  32117  nmbdfnlbi  32138  nmcfnexi  32140  nmcfnlbi  32141  cnlnadjlem7  32162  nmopcoi  32184  nmopcoadji  32190  branmfn  32194  strlem1  32339  sgnval2  32826  constrdircl  33928  iconstr  33929  constrinvcl  33936  constrresqrtcl  33940  constrabscl  33941  constrsqrtcl  33942  cos9thpinconstrlem1  33952  subfaclim  35389  dnizphlfeqhlf  36755  dnibndlem6  36762  dnibndlem9  36765  knoppndvlem11  36801  knoppndvlem14  36804  poimirlem29  37987  ftc1cnnclem  38029  ftc1anclem5  38035  lmclim2  38096  geomcau  38097  cntotbnd  38134  gcdnn0id  42778  readvrec  42811  irrapxlem2  43272  irrapxlem5  43275  pellexlem2  43279  oddcomabszz  43393  jm2.19  43442  jm2.26lem3  43450  absmulrposd  44607  nzprmdif  44767  0ellimcdiv  46098  stoweidlem7  46456  fourierdlem30  46586  fourierdlem39  46595  etransclem23  46706  etransclem41  46724  hoiqssbllem2  47072  modlt0b  47832  blenre  49065  blennn  49066