Theorem sqdivi

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

	Ref	Expression
Hypotheses	sqval.1	⊢ 𝐴 ∈ ℂ
	sqmul.2	⊢ 𝐵 ∈ ℂ
	sqdiv.3	⊢ 𝐵 ≠ 0
Assertion	sqdivi	⊢ ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		sqval.1	⊢ 𝐴 ∈ ℂ
2		sqmul.2	⊢ 𝐵 ∈ ℂ
3		sqdiv.3	⊢ 𝐵 ≠ 0
4	1 2 1 2 3 3	divmuldivi	⊢ ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) )
5	1 2 3	divcli	⊢ ( 𝐴 / 𝐵 ) ∈ ℂ
6	5	sqvali	⊢ ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 / 𝐵 ) · ( 𝐴 / 𝐵 ) )
7	1	sqvali	⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
8	2	sqvali	⊢ ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 )
9	7 8	oveq12i	⊢ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 · 𝐴 ) / ( 𝐵 · 𝐵 ) )
10	4 6 9	3eqtr4i	⊢ ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) )