Metamath Proof Explorer

Theorem sqdiv

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

Ref Expression
Assertion sqdiv ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐴 ∈ ℂ )
2 3simpc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
3 divmuldiv ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ∧ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) ) )
4 1 1 2 2 3 syl22anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) ) )
5 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
6 sqval ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) ) )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) ) )
8 sqval ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
9 sqval ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
10 8 9 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) ) )
11 10 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) ) )
12 4 7 11 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )