Theorem absidd 15422

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099   class class class wbr 5145  ‘cfv 6546  ℝcr 11148  0cc0 11149   ≤ cle 11290  abscabs 15234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-2nd 7996  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8726  df-en 8967  df-dom 8968  df-sdom 8969  df-sup 9478  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-n0 12519  df-z 12605  df-uz 12869  df-rp 13023  df-seq 14016  df-exp 14076  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236

This theorem is referenced by:  rlimno1  15653  iseralt  15684  cvgcmpce  15817  divrcnv  15851  geomulcvg  15875  cvgrat  15882  mertenslem2  15884  eftabs  16072  efcllem  16074  efaddlem  16090  eftlub  16106  eflegeo  16118  ef01bndlem  16181  absef  16194  efieq1re  16196  dvdseq  16311  divalg2  16402  nn0gcdid0  16516  absmulgcd  16545  nn0rppwr  16557  nn0expgcd  16560  lcmgcdlem  16602  mulgcddvds  16651  phibndlem  16767  dfphi2  16771  mul4sqlem  16950  4sqlem11  16952  prmirredlem  21458  prmirred  21460  blcvx  24802  reperflem  24822  reconnlem2  24831  nmoleub2lem3  25130  nmoleub3  25134  tcphcphlem1  25251  iscmet3lem3  25306  pjthlem1  25453  lhop1lem  26034  ftc1lem4  26062  plyeq0lem  26234  aalioulem4  26360  mtest  26430  radcnvlem1  26439  radcnvlt1  26444  radcnvle  26446  dvradcnv  26447  pserdvlem2  26455  abelth2  26469  tanabsge  26531  sineq0  26548  divlogrlim  26659  logcnlem3  26668  logcnlem4  26669  logtayllem  26683  logtayl  26684  abscxp2  26717  logbgcd1irr  26819  chordthmlem4  26860  rlimcnp  26990  lgamgulmlem2  27055  lgamgulmlem5  27058  lgamcvg2  27080  ftalem5  27102  lgsval2lem  27333  lgsval4a  27345  2sqlem3  27446  chebbnd1  27498  chtppilimlem2  27500  chto1ub  27502  vmadivsum  27508  vmadivsumb  27509  rpvmasumlem  27513  dchrisumlem2  27516  dchrisumlem3  27517  dchrvmasumlem2  27524  dchrvmasumiflem1  27527  dchrisum0fno1  27537  dchrisum0re  27539  rplogsum  27553  mulog2sumlem1  27560  mulog2sumlem2  27561  2vmadivsumlem  27566  selbergb  27575  selberg2lem  27576  selberg2b  27578  selberg3lem1  27583  selberg3lem2  27584  selberg4lem1  27586  pntrsumo1  27591  pntrlog2bndlem1  27603  pntrlog2bndlem2  27604  pntrlog2bndlem3  27605  pntrlog2bndlem5  27607  pntrlog2bndlem6  27609  pntrlog2bnd  27610  pntpbnd1a  27611  pntpbnd1  27612  pntibndlem2  27617  ostth2  27663  htthlem  30847  bcsiALT  31109  norm1  31179  pjhthlem1  31321  nmbdoplbi  31954  nmcexi  31956  nmcopexi  31957  nmcoplbi  31958  nmbdfnlbi  31979  nmcfnexi  31981  nmcfnlbi  31982  cnlnadjlem7  32003  nmopcoi  32025  nmopcoadji  32031  branmfn  32035  strlem1  32180  subfaclim  35029  dnizphlfeqhlf  36192  dnibndlem6  36199  dnibndlem9  36202  knoppndvlem11  36238  knoppndvlem14  36241  poimirlem29  37363  ftc1cnnclem  37405  ftc1anclem5  37411  lmclim2  37472  geomcau  37473  cntotbnd  37510  gcdnn0id  42055  irrapxlem2  42517  irrapxlem5  42520  pellexlem2  42524  oddcomabszz  42639  jm2.19  42688  jm2.26lem3  42696  absmulrposd  43863  nzprmdif  44030  0ellimcdiv  45306  stoweidlem7  45664  fourierdlem30  45794  fourierdlem39  45803  etransclem23  45914  etransclem41  45932  hoiqssbllem2  46280  blenre  47998  blennn  47999