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	eqtr2id	⊢ ( 𝜑 → ( ( 𝑀 ↑ 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 ) / 𝑀 ) ) = 𝐷 )