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

Metamath Proof Explorer

Theorem sqdiv

Description: Distribution of squaring over division. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqdiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B 2 = A 2 B 2

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
2 3simpc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ ∧ B ≠ 0
3 divmuldiv ⊢ A ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ A B = A ⁢ A B ⁢ B
4 1 1 2 2 3 syl22anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ A B = A ⁢ A B ⁢ B
5 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
6 sqval ⊢ A B ∈ ℂ → A B 2 = A B ⁢ A B
7 5 6 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B 2 = A B ⁢ A B
8 sqval ⊢ A ∈ ℂ → A 2 = A ⁢ A
9 sqval ⊢ B ∈ ℂ → B 2 = B ⁢ B
10 8 9 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 B 2 = A ⁢ A B ⁢ B
11 10 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A 2 B 2 = A ⁢ A B ⁢ B
12 4 7 11 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B 2 = A 2 B 2