This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqdivi

Description: Distribution of squaring over division. (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypotheses sqval.1 ⊢ A ∈ ℂ
sqmul.2 ⊢ B ∈ ℂ
sqdiv.3 ⊢ B ≠ 0
Assertion sqdivi ⊢ A B 2 = A 2 B 2

Proof

Step Hyp Ref Expression
1 sqval.1 ⊢ A ∈ ℂ
2 sqmul.2 ⊢ B ∈ ℂ
3 sqdiv.3 ⊢ B ≠ 0
4 1 2 1 2 3 3 divmuldivi ⊢ A B ⁢ A B = A ⁢ A B ⁢ B
5 1 2 3 divcli ⊢ A B ∈ ℂ
6 5 sqvali ⊢ A B 2 = A B ⁢ A B
7 1 sqvali ⊢ A 2 = A ⁢ A
8 2 sqvali ⊢ B 2 = B ⁢ B
9 7 8 oveq12i ⊢ A 2 B 2 = A ⁢ A B ⁢ B
10 4 6 9 3eqtr4i ⊢ A B 2 = A 2 B 2