Metamath Proof Explorer

Theorem dquartlem2

Description: Lemma for dquart . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dquart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
dquart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
dquart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
dquart.s ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
dquart.m ⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
dquart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
dquart.i ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
dquart.i2 ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) )
dquart.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
dquart.3 ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) + - ( 𝐶 ↑ 2 ) ) ) = 0 )
Assertion dquartlem2 ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) ↑ 2 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 dquart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
2 dquart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3 dquart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4 dquart.s ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
5 dquart.m ⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
6 dquart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
7 dquart.i ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
8 dquart.i2 ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) )
9 dquart.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
10 dquart.3 ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) + - ( 𝐶 ↑ 2 ) ) ) = 0 )
11 2cn ⊢ 2 ∈ ℂ
12 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 2 · 𝑆 ) ∈ ℂ )
13 11 4 12 sylancr ⊢ ( 𝜑 → ( 2 · 𝑆 ) ∈ ℂ )
14 13 sqcld ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) ∈ ℂ )
15 5 14 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
16 15 1 addcld ⊢ ( 𝜑 → ( 𝑀 + 𝐵 ) ∈ ℂ )
17 11 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
20 16 17 19 sqdivd ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) ↑ 2 ) = ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
21 sq2 ⊢ ( 2 ↑ 2 ) = 4
22 21 oveq2i ⊢ ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 )
23 20 22 eqtrdi ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) ↑ 2 ) = ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) )
24 23 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) ↑ 2 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) = ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) )
25 16 sqcld ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) ↑ 2 ) ∈ ℂ )
26 4cn ⊢ 4 ∈ ℂ
27 26 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
28 4ne0 ⊢ 4 ≠ 0
29 28 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
30 25 27 29 divcld ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) ∈ ℂ )
31 2 sqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
32 31 27 29 divcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) / 4 ) ∈ ℂ )
33 32 15 6 divcld ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ∈ ℂ )
34 30 33 subcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) ∈ ℂ )
35 30 33 15 subdird ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) · 𝑀 ) = ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) · 𝑀 ) − ( ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) · 𝑀 ) ) )
36 25 15 27 29 div23d ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) / 4 ) = ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) · 𝑀 ) )
37 36 eqcomd ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) · 𝑀 ) = ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) / 4 ) )
38 32 15 6 divcan1d ⊢ ( 𝜑 → ( ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) · 𝑀 ) = ( ( 𝐶 ↑ 2 ) / 4 ) )
39 37 38 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) · 𝑀 ) − ( ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) · 𝑀 ) ) = ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) / 4 ) − ( ( 𝐶 ↑ 2 ) / 4 ) ) )
40 binom2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑀 + 𝐵 ) ↑ 2 ) = ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
41 15 1 40 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) ↑ 2 ) = ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
42 41 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) = ( ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝑀 ) )
43 15 sqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
44 15 1 mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝐵 ) ∈ ℂ )
45 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑀 · 𝐵 ) ∈ ℂ ) → ( 2 · ( 𝑀 · 𝐵 ) ) ∈ ℂ )
46 11 44 45 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑀 · 𝐵 ) ) ∈ ℂ )
47 43 46 addcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) ∈ ℂ )
48 1 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
49 47 48 15 adddird ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝑀 ) = ( ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) · 𝑀 ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) )
50 43 46 15 adddird ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) · 𝑀 ) = ( ( ( 𝑀 ↑ 2 ) · 𝑀 ) + ( ( 2 · ( 𝑀 · 𝐵 ) ) · 𝑀 ) ) )
51 df-3 ⊢ 3 = ( 2 + 1 )
52 51 oveq2i ⊢ ( 𝑀 ↑ 3 ) = ( 𝑀 ↑ ( 2 + 1 ) )
53 2nn0 ⊢ 2 ∈ ℕ0
54 expp1 ⊢ ( ( 𝑀 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝑀 ↑ ( 2 + 1 ) ) = ( ( 𝑀 ↑ 2 ) · 𝑀 ) )
55 15 53 54 sylancl ⊢ ( 𝜑 → ( 𝑀 ↑ ( 2 + 1 ) ) = ( ( 𝑀 ↑ 2 ) · 𝑀 ) )
56 52 55 syl5req ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) · 𝑀 ) = ( 𝑀 ↑ 3 ) )
57 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) ∈ ℂ )
58 11 1 57 sylancr ⊢ ( 𝜑 → ( 2 · 𝐵 ) ∈ ℂ )
59 58 15 15 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 𝐵 ) · 𝑀 ) · 𝑀 ) = ( ( 2 · 𝐵 ) · ( 𝑀 · 𝑀 ) ) )
60 17 15 1 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · 𝐵 ) = ( 2 · ( 𝑀 · 𝐵 ) ) )
61 17 15 1 mul32d ⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · 𝐵 ) = ( ( 2 · 𝐵 ) · 𝑀 ) )
62 60 61 eqtr3d ⊢ ( 𝜑 → ( 2 · ( 𝑀 · 𝐵 ) ) = ( ( 2 · 𝐵 ) · 𝑀 ) )
63 62 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( 𝑀 · 𝐵 ) ) · 𝑀 ) = ( ( ( 2 · 𝐵 ) · 𝑀 ) · 𝑀 ) )
64 15 sqvald ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
65 64 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) = ( ( 2 · 𝐵 ) · ( 𝑀 · 𝑀 ) ) )
66 59 63 65 3eqtr4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑀 · 𝐵 ) ) · 𝑀 ) = ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) )
67 56 66 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) · 𝑀 ) + ( ( 2 · ( 𝑀 · 𝐵 ) ) · 𝑀 ) ) = ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) )
68 50 67 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) · 𝑀 ) = ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) )
69 68 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) + ( 2 · ( 𝑀 · 𝐵 ) ) ) · 𝑀 ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) )
70 42 49 69 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) )
71 70 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) )
72 3nn0 ⊢ 3 ∈ ℕ0
73 expcl ⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
74 15 72 73 sylancl ⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
75 58 43 mulcld ⊢ ( 𝜑 → ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ∈ ℂ )
76 74 75 addcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) ∈ ℂ )
77 48 15 mulcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · 𝑀 ) ∈ ℂ )
78 mulcl ⊢ ( ( 4 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 4 · 𝐷 ) ∈ ℂ )
79 26 9 78 sylancr ⊢ ( 𝜑 → ( 4 · 𝐷 ) ∈ ℂ )
80 79 15 mulcld ⊢ ( 𝜑 → ( ( 4 · 𝐷 ) · 𝑀 ) ∈ ℂ )
81 76 77 80 addsubassd ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) ) )
82 48 79 15 subdird ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) = ( ( ( 𝐵 ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) )
83 82 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) ) )
84 81 83 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝑀 ) ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) )
85 48 79 subcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) ∈ ℂ )
86 85 15 mulcld ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ∈ ℂ )
87 76 86 addcld ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) ∈ ℂ )
88 31 negcld ⊢ ( 𝜑 → - ( 𝐶 ↑ 2 ) ∈ ℂ )
89 76 86 88 addassd ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) + - ( 𝐶 ↑ 2 ) ) = ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) + - ( 𝐶 ↑ 2 ) ) ) )
90 87 31 negsubd ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) + - ( 𝐶 ↑ 2 ) ) = ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) − ( 𝐶 ↑ 2 ) ) )
91 89 90 10 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) − ( 𝐶 ↑ 2 ) ) = 0 )
92 87 31 91 subeq0d ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) ) = ( 𝐶 ↑ 2 ) )
93 71 84 92 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( 𝐶 ↑ 2 ) )
94 25 15 mulcld ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) ∈ ℂ )
95 subsub23 ⊢ ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) ∈ ℂ ∧ ( ( 4 · 𝐷 ) · 𝑀 ) ∈ ℂ ∧ ( 𝐶 ↑ 2 ) ∈ ℂ ) → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( 𝐶 ↑ 2 ) ↔ ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) = ( ( 4 · 𝐷 ) · 𝑀 ) ) )
96 94 80 31 95 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( ( 4 · 𝐷 ) · 𝑀 ) ) = ( 𝐶 ↑ 2 ) ↔ ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) = ( ( 4 · 𝐷 ) · 𝑀 ) ) )
97 93 96 mpbid ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) = ( ( 4 · 𝐷 ) · 𝑀 ) )
98 27 9 15 mulassd ⊢ ( 𝜑 → ( ( 4 · 𝐷 ) · 𝑀 ) = ( 4 · ( 𝐷 · 𝑀 ) ) )
99 97 98 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) = ( 4 · ( 𝐷 · 𝑀 ) ) )
100 99 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) / 4 ) = ( ( 4 · ( 𝐷 · 𝑀 ) ) / 4 ) )
101 94 31 27 29 divsubdird ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) − ( 𝐶 ↑ 2 ) ) / 4 ) = ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) / 4 ) − ( ( 𝐶 ↑ 2 ) / 4 ) ) )
102 9 15 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝑀 ) ∈ ℂ )
103 102 27 29 divcan3d ⊢ ( 𝜑 → ( ( 4 · ( 𝐷 · 𝑀 ) ) / 4 ) = ( 𝐷 · 𝑀 ) )
104 100 101 103 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) · 𝑀 ) / 4 ) − ( ( 𝐶 ↑ 2 ) / 4 ) ) = ( 𝐷 · 𝑀 ) )
105 35 39 104 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) · 𝑀 ) = ( 𝐷 · 𝑀 ) )
106 34 9 15 6 105 mulcan2ad ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) ↑ 2 ) / 4 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) = 𝐷 )
107 24 106 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) ↑ 2 ) − ( ( ( 𝐶 ↑ 2 ) / 4 ) / 𝑀 ) ) = 𝐷 )