Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqmul
Next ⟩
sqeq0
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqmul
Description:
Distribution of square over multiplication.
(Contributed by
NM
, 21-Mar-2008)
Ref
Expression
Assertion
sqmul
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
A
⁢
B
2
=
A
2
⁢
B
2
Proof
Step
Hyp
Ref
Expression
1
2nn0
⊢
2
∈
ℕ
0
2
mulexp
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
2
∈
ℕ
0
→
A
⁢
B
2
=
A
2
⁢
B
2
3
1
2
mp3an3
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
A
⁢
B
2
=
A
2
⁢
B
2