Metamath Proof Explorer

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 ) − 𝐷 ) / 𝐶 ) ) )