Theorem sqdivzi

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013)

	Ref	Expression
Hypotheses	sqdivzi.1	⊢ 𝐴 ∈ ℂ
	sqdivzi.2	⊢ 𝐵 ∈ ℂ
Assertion	sqdivzi	⊢ ( 𝐵 ≠ 0 → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sqdivzi.1	⊢ 𝐴 ∈ ℂ
2		sqdivzi.2	⊢ 𝐵 ∈ ℂ
3		oveq2	⊢ ( 𝐵 = if ( 𝐵 ≠ 0 , 𝐵 , 1 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 / if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ) )
4	3	oveq1d	⊢ ( 𝐵 = if ( 𝐵 ≠ 0 , 𝐵 , 1 ) → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 / if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ) ↑ 2 ) )
5		oveq1	⊢ ( 𝐵 = if ( 𝐵 ≠ 0 , 𝐵 , 1 ) → ( 𝐵 ↑ 2 ) = ( if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ↑ 2 ) )
6	5	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ≠ 0 , 𝐵 , 1 ) → ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) / ( if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ↑ 2 ) ) )
7	4 6	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ≠ 0 , 𝐵 , 1 ) → ( ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ↔ ( ( 𝐴 / if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ↑ 2 ) ) ) )
8		ax-1cn	⊢ 1 ∈ ℂ
9	2 8	ifcli	⊢ if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ∈ ℂ
10		elimne0	⊢ if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ≠ 0
11	1 9 10	sqdivi	⊢ ( ( 𝐴 / if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( if ( 𝐵 ≠ 0 , 𝐵 , 1 ) ↑ 2 ) )
12	7 11	dedth	⊢ ( 𝐵 ≠ 0 → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )