Theorem mulsubdivbinom2

Description: The square of a binomial with factor minus a number divided by a nonzero number. (Contributed by AV, 19-Jul-2021)

	Ref	Expression
Assertion	mulsubdivbinom2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐴 ∈ ℂ )
3		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ )
4		simpl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → 𝐶 ∈ ℂ )
5	4	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
6		mulbinom2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) = ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 𝐷 ) = ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) / 𝐶 ) )
9	2 3 5 8	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) / 𝐶 ) )
10	5 2	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐴 ) ∈ ℂ )
11	10	sqcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) ↑ 2 ) ∈ ℂ )
12		2cnd	⊢ ( 𝐶 ∈ ℂ → 2 ∈ ℂ )
13		id	⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ ℂ )
14	12 13	mulcld	⊢ ( 𝐶 ∈ ℂ → ( 2 · 𝐶 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 2 · 𝐶 ) ∈ ℂ )
16	15	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 2 · 𝐶 ) ∈ ℂ )
17		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
18	17	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
20	16 19	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
21	11 20	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
22		sqcl	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) ∈ ℂ )
23	22	3ad2ant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
24	23	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
25	21 24	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ )
26		simpl3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐷 ∈ ℂ )
27		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
28		divsubdir	⊢ ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) / 𝐶 ) = ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) )
29	25 26 27 28	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) / 𝐶 ) = ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) )
30		divdir	⊢ ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ ∧ ( 𝐵 ↑ 2 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) = ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) )
31	21 24 27 30	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) = ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) )
32		divdir	⊢ ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) ∈ ℂ ∧ ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) = ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) / 𝐶 ) + ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) ) )
33	11 20 27 32	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) = ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) / 𝐶 ) + ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) ) )
34		sqmul	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐶 · 𝐴 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
35	4 1 34	syl2anr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
36	35	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) / 𝐶 ) = ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) / 𝐶 ) )
37		sqcl	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 ↑ 2 ) ∈ ℂ )
38	37	adantr	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
39	38	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
40		sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
41	40	3ad2ant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
42	41	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
43		div23	⊢ ( ( ( 𝐶 ↑ 2 ) ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) / 𝐶 ) = ( ( ( 𝐶 ↑ 2 ) / 𝐶 ) · ( 𝐴 ↑ 2 ) ) )
44	39 42 27 43	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) / 𝐶 ) = ( ( ( 𝐶 ↑ 2 ) / 𝐶 ) · ( 𝐴 ↑ 2 ) ) )
45		sqdivid	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐶 ↑ 2 ) / 𝐶 ) = 𝐶 )
46	45	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 ↑ 2 ) / 𝐶 ) = 𝐶 )
47	46	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 ↑ 2 ) / 𝐶 ) · ( 𝐴 ↑ 2 ) ) = ( 𝐶 · ( 𝐴 ↑ 2 ) ) )
48	36 44 47	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) / 𝐶 ) = ( 𝐶 · ( 𝐴 ↑ 2 ) ) )
49		div23	⊢ ( ( ( 2 · 𝐶 ) ∈ ℂ ∧ ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) = ( ( ( 2 · 𝐶 ) / 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
50	16 19 27 49	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) = ( ( ( 2 · 𝐶 ) / 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
51		2cnd	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → 2 ∈ ℂ )
52		simpr	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → 𝐶 ≠ 0 )
53	51 4 52	divcan4d	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 2 · 𝐶 ) / 𝐶 ) = 2 )
54	53	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 2 · 𝐶 ) / 𝐶 ) = 2 )
55	54	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 2 · 𝐶 ) / 𝐶 ) · ( 𝐴 · 𝐵 ) ) = ( 2 · ( 𝐴 · 𝐵 ) ) )
56	50 55	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) = ( 2 · ( 𝐴 · 𝐵 ) ) )
57	48 56	oveq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) / 𝐶 ) + ( ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) / 𝐶 ) ) = ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) )
58	33 57	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) = ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) )
59	58	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) / 𝐶 ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) )
60	31 59	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) )
61	60	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) = ( ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) − ( 𝐷 / 𝐶 ) ) )
62	5 42	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
63		2cnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 2 ∈ ℂ )
64	63 17	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
65	64	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
66	65	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
67	62 66	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
68	52	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ≠ 0 )
69	24 5 68	divcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐵 ↑ 2 ) / 𝐶 ) ∈ ℂ )
70	26 5 68	divcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐷 / 𝐶 ) ∈ ℂ )
71	67 69 70	addsubassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( 𝐵 ↑ 2 ) / 𝐶 ) ) − ( 𝐷 / 𝐶 ) ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) ) )
72	29 61 71	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − 𝐷 ) / 𝐶 ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) ) )
73		divsubdir	⊢ ( ( ( 𝐵 ↑ 2 ) ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) )
74	24 26 27 73	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) )
75	74	eqcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) = ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) )
76	75	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) / 𝐶 ) − ( 𝐷 / 𝐶 ) ) ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) ) )
77	9 72 76	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 𝐷 ) / 𝐶 ) = ( ( ( 𝐶 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 𝐷 ) / 𝐶 ) ) )