Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Square root; absolute value
absvalsqi
Next ⟩
absvalsq2i
Metamath Proof Explorer
Ascii
Unicode
Theorem
absvalsqi
Description:
Square of value of absolute value function.
(Contributed by
NM
, 2-Oct-1999)
Ref
Expression
Hypothesis
absvalsqi.1
⊢
A
∈
ℂ
Assertion
absvalsqi
⊢
A
2
=
A
⁢
A
‾
Proof
Step
Hyp
Ref
Expression
1
absvalsqi.1
⊢
A
∈
ℂ
2
absvalsq
⊢
A
∈
ℂ
→
A
2
=
A
⁢
A
‾
3
1
2
ax-mp
⊢
A
2
=
A
⁢
A
‾