Theorem absid 15338

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

Assertion

Ref	Expression
absid	⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)

Proof of Theorem absid

Step	Hyp	Ref	Expression
1		simpl 482	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
2	1	recnd 11293	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℂ)
3		absval 15280	. . 3 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))
4	2, 3	syl 17	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))
5	1	cjred 15268	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (∗‘𝐴) = 𝐴)
6	5	oveq2d 7451	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 · (∗‘𝐴)) = (𝐴 · 𝐴))
7	2	sqvald 14186	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴↑2) = (𝐴 · 𝐴))
8	6, 7	eqtr4d 2779	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 · (∗‘𝐴)) = (𝐴↑2))
9	8	fveq2d 6915	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · (∗‘𝐴))) = (√‘(𝐴↑2)))
10		sqrtsq 15311	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)
11	4, 9, 10	3eqtrd 2780	1 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1538   ∈ wcel 2107   class class class wbr 5149  ‘cfv 6566  (class class class)co 7435  ℂcc 11157  ℝcr 11158  0cc0 11159   · cmul 11164   ≤ cle 11300  2c2 12325  ↑cexp 14105  ∗ccj 15138  √csqrt 15275  abscabs 15276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236  ax-pre-sup 11237

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-pss 3984  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5642  df-we 5644  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-pred 6326  df-ord 6392  df-on 6393  df-lim 6394  df-suc 6395  df-iota 6519  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7392  df-ov 7438  df-oprab 7439  df-mpo 7440  df-om 7892  df-2nd 8020  df-frecs 8311  df-wrecs 8342  df-recs 8416  df-rdg 8455  df-er 8750  df-en 8991  df-dom 8992  df-sdom 8993  df-sup 9486  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11498  df-neg 11499  df-div 11925  df-nn 12271  df-2 12333  df-3 12334  df-n0 12531  df-z 12618  df-uz 12883  df-rp 13039  df-seq 14046  df-exp 14106  df-cj 15141  df-re 15142  df-im 15143  df-sqrt 15277  df-abs 15278

This theorem is referenced by:  abs1  15339  absnid  15340  leabs  15341  absor  15342  sqabs  15349  max0add  15352  absidm  15365  abssubge0  15369  fzomaxdiflem  15384  absidi  15419  absidd  15464  o1fsum  15852  geo2lim  15914  geoihalfsum  15921  ege2le3  16129  eirrlem  16243  rpnnen2lem3  16255  rpnnen2lem9  16261  6gcd4e2  16578  lcmgcdnn  16651  lcmfun  16685  lcmfass  16686  zringndrg  21503  ncvsge0  25209  iscmet3lem3  25346  minveclem2  25482  mbfi1fseqlem6  25778  dvfsumrlim  26095  aaliou3lem3  26409  pserulm  26488  pige3ALT  26585  efif1olem4  26610  cxpcn3lem  26813  log2cnv  27010  log2tlbnd  27011  cxplim  27038  cxploglim2  27045  divsqrtsumo1  27050  fsumharmonic  27078  zetacvg  27081  logfacrlim  27291  logexprlim  27292  dchrmusum2  27561  dchrvmasumlem3  27566  dchrisum0lem1  27583  dchrisum0lem2a  27584  dchrisum0lem2  27585  mudivsum  27597  mulogsumlem  27598  log2sumbnd  27611  selberglem2  27613  selberg3lem1  27624  pntpbnd2  27654  pntibndlem2  27658  pntlemn  27667  pntlemj  27670  pntlemo  27674  ex-abs  30497  ex-gcd  30499  nvsge0  30706  nmoub2i  30816  minvecolem2  30917  subfacval3  35186  knoppndvlem14  36520  poimir  37652  ftc1anclem5  37696  lcm2un  42008  rpabsid  42347  oddcomabszz  42947  reabsifneg  43636  reabsifnpos  43637  reabsifpos  43638  reabsifnneg  43639  fourierdlem68  46141  itsclc0yqsol  48635