Theorem dquartlem2

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

	Ref	Expression
Hypotheses	dquart.b	$$⊢\phi \to B\in ℂ$$
	dquart.c	$$⊢\phi \to C\in ℂ$$
	dquart.x	$$⊢\phi \to X\in ℂ$$
	dquart.s	$$⊢\phi \to S\in ℂ$$
	dquart.m	$$⊢\phi \to M={2S}^2$$
	dquart.m0	$$⊢\phi \to M\ne 0$$
	dquart.i	$$⊢\phi \to I\in ℂ$$
	dquart.i2	$$⊢\phi \to I^2=\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)$$
	dquart.d	$$⊢\phi \to D\in ℂ$$
	dquart.3	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=0$$
Assertion	dquartlem2	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2-\left(\frac{\frac{C^2}{4}}{M}\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		dquart.b	$$⊢\phi \to B\in ℂ$$
2		dquart.c	$$⊢\phi \to C\in ℂ$$
3		dquart.x	$$⊢\phi \to X\in ℂ$$
4		dquart.s	$$⊢\phi \to S\in ℂ$$
5		dquart.m	$$⊢\phi \to M={2S}^2$$
6		dquart.m0	$$⊢\phi \to M\ne 0$$
7		dquart.i	$$⊢\phi \to I\in ℂ$$
8		dquart.i2	$$⊢\phi \to I^2=\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)$$
9		dquart.d	$$⊢\phi \to D\in ℂ$$
10		dquart.3	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=0$$
11		2cn	$$⊢2\in ℂ$$
12		mulcl	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to 2S\in ℂ$$
13	11 4 12	sylancr	$$⊢\phi \to 2S\in ℂ$$
14	13	sqcld	$$⊢\phi \to {2S}^2\in ℂ$$
15	5 14	eqeltrd	$$⊢\phi \to M\in ℂ$$
16	15 1	addcld	$$⊢\phi \to M+B\in ℂ$$
17	11	a1i	$$⊢\phi \to 2\in ℂ$$
18		2ne0	$$⊢2\ne 0$$
19	18	a1i	$$⊢\phi \to 2\ne 0$$
20	16 17 19	sqdivd	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2=\frac{{\left(M+B\right)}^2}{2^2}$$
21		sq2	$$⊢2^2=4$$
22	21	oveq2i	$$⊢\frac{{\left(M+B\right)}^2}{2^2}=\frac{{\left(M+B\right)}^2}{4}$$
23	20 22	eqtrdi	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2=\frac{{\left(M+B\right)}^2}{4}$$
24	23	oveq1d	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2-\left(\frac{\frac{C^2}{4}}{M}\right)=\left(\frac{{\left(M+B\right)}^2}{4}\right)-\left(\frac{\frac{C^2}{4}}{M}\right)$$
25	16	sqcld	$$⊢\phi \to {\left(M+B\right)}^2\in ℂ$$
26		4cn	$$⊢4\in ℂ$$
27	26	a1i	$$⊢\phi \to 4\in ℂ$$
28		4ne0	$$⊢4\ne 0$$
29	28	a1i	$$⊢\phi \to 4\ne 0$$
30	25 27 29	divcld	$$⊢\phi \to \frac{{\left(M+B\right)}^2}{4}\in ℂ$$
31	2	sqcld	$$⊢\phi \to C^2\in ℂ$$
32	31 27 29	divcld	$$⊢\phi \to \frac{C^2}{4}\in ℂ$$
33	32 15 6	divcld	$$⊢\phi \to \frac{\frac{C^2}{4}}{M}\in ℂ$$
34	30 33	subcld	$$⊢\phi \to \left(\frac{{\left(M+B\right)}^2}{4}\right)-\left(\frac{\frac{C^2}{4}}{M}\right)\in ℂ$$
35	30 33 15	subdird	$$⊢\phi \to \left(\left(\frac{{\left(M+B\right)}^2}{4}\right)-\left(\frac{\frac{C^2}{4}}{M}\right)\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(\frac{{\left(M+B\right)}^2}{4}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(\frac{\frac{C^2}{4}}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
36	25 15 27 29	div23d	$$⊢\phi \to \frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}=\left(\frac{{\left(M+B\right)}^2}{4}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
37	36	eqcomd	$$⊢\phi \to \left(\frac{{\left(M+B\right)}^2}{4}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}$$
38	32 15 6	divcan1d	$$⊢\phi \to \left(\frac{\frac{C^2}{4}}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\frac{C^2}{4}$$
39	37 38	oveq12d	$$⊢\phi \to \left(\frac{{\left(M+B\right)}^2}{4}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(\frac{\frac{C^2}{4}}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(\frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}\right)-\left(\frac{C^2}{4}\right)$$
40		binom2	$$⊢\left(M\in ℂ\wedge B\in ℂ\right)\to {\left(M+B\right)}^2=M^2+2MB+B^2$$
41	15 1 40	syl2anc	$$⊢\phi \to {\left(M+B\right)}^2=M^2+2MB+B^2$$
42	41	oveq1d	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(M^2+2MB+B^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
43	15	sqcld	$$⊢\phi \to M^2\in ℂ$$
44	15 1	mulcld	$$⊢\phi \to MB\in ℂ$$
45		mulcl	$$⊢\left(2\in ℂ\wedge MB\in ℂ\right)\to 2MB\in ℂ$$
46	11 44 45	sylancr	$$⊢\phi \to 2MB\in ℂ$$
47	43 46	addcld	$$⊢\phi \to M^2+2MB\in ℂ$$
48	1	sqcld	$$⊢\phi \to B^2\in ℂ$$
49	47 48 15	adddird	$$⊢\phi \to \left(M^2+2MB+B^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(M^2+2MB\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
50	43 46 15	adddird	$$⊢\phi \to \left(M^2+2MB\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+2MB\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
51		df-3	$$⊢3=2+1$$
52	51	oveq2i	$$⊢M^3=M^{2+1}$$
53		2nn0	$$⊢2\in {\mathbb{N}}_0$$
54		expp1	$$⊢\left(M\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to M^{2+1}=M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
55	15 53 54	sylancl	$$⊢\phi \to M^{2+1}=M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
56	52 55	eqtr2id	$$⊢\phi \to M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3$$
57		mulcl	$$⊢\left(2\in ℂ\wedge B\in ℂ\right)\to 2B\in ℂ$$
58	11 1 57	sylancr	$$⊢\phi \to 2B\in ℂ$$
59	58 15 15	mulassd	$$⊢\phi \to 2B\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2B\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
60	17 15 1	mulassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}B=2MB$$
61	17 15 1	mul32d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}B=2B\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
62	60 61	eqtr3d	$$⊢\phi \to 2MB=2B\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
63	62	oveq1d	$$⊢\phi \to 2MB\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2B\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
64	15	sqvald	$$⊢\phi \to M^2=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
65	64	oveq2d	$$⊢\phi \to 2B{M}^2=2B\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
66	59 63 65	3eqtr4d	$$⊢\phi \to 2MB\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2B{M}^2$$
67	56 66	oveq12d	$$⊢\phi \to M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+2MB\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2$$
68	50 67	eqtrd	$$⊢\phi \to \left(M^2+2MB\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2$$
69	68	oveq1d	$$⊢\phi \to \left(M^2+2MB\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
70	42 49 69	3eqtrd	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
71	70	oveq1d	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(M^3+2B{M}^2\right)+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
72		3nn0	$$⊢3\in {\mathbb{N}}_0$$
73		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
74	15 72 73	sylancl	$$⊢\phi \to M^3\in ℂ$$
75	58 43	mulcld	$$⊢\phi \to 2B{M}^2\in ℂ$$
76	74 75	addcld	$$⊢\phi \to M^3+2B{M}^2\in ℂ$$
77	48 15	mulcld	$$⊢\phi \to B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
78		mulcl	$$⊢\left(4\in ℂ\wedge D\in ℂ\right)\to 4D\in ℂ$$
79	26 9 78	sylancr	$$⊢\phi \to 4D\in ℂ$$
80	79 15	mulcld	$$⊢\phi \to 4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
81	76 77 80	addsubassd	$$⊢\phi \to \left(M^3+2B{M}^2\right)+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2+\left(B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
82	48 79 15	subdird	$$⊢\phi \to \left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
83	82	oveq2d	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2+\left(B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
84	81 83	eqtr4d	$$⊢\phi \to \left(M^3+2B{M}^2\right)+B^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
85	48 79	subcld	$$⊢\phi \to B^2-4D\in ℂ$$
86	85 15	mulcld	$$⊢\phi \to \left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
87	76 86	addcld	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
88	31	negcld	$$⊢\phi \to -C^2\in ℂ$$
89	76 86 88	addassd	$$⊢\phi \to \left(M^3+2B{M}^2\right)+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)$$
90	87 31	negsubd	$$⊢\phi \to \left(M^3+2B{M}^2\right)+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=\left(M^3+2B{M}^2\right)+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2$$
91	89 90 10	3eqtr3d	$$⊢\phi \to \left(M^3+2B{M}^2\right)+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2=0$$
92	87 31 91	subeq0d	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=C^2$$
93	71 84 92	3eqtrd	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=C^2$$
94	25 15	mulcld	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
95		subsub23	$$⊢\left({\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ\wedge 4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ\wedge C^2\in ℂ\right)\to \left({\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=C^2\leftrightarrow {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2=4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
96	94 80 31 95	syl3anc	$$⊢\phi \to \left({\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=C^2\leftrightarrow {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2=4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
97	93 96	mpbid	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2=4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
98	27 9 15	mulassd	$$⊢\phi \to 4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
99	97 98	eqtrd	$$⊢\phi \to {\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2=4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
100	99	oveq1d	$$⊢\phi \to \frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2}{4}=\frac{4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}$$
101	94 31 27 29	divsubdird	$$⊢\phi \to \frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-C^2}{4}=\left(\frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}\right)-\left(\frac{C^2}{4}\right)$$
102	9 15	mulcld	$$⊢\phi \to D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
103	102 27 29	divcan3d	$$⊢\phi \to \frac{4D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}=D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
104	100 101 103	3eqtr3d	$$⊢\phi \to \left(\frac{{\left(M+B\right)}^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{4}\right)-\left(\frac{C^2}{4}\right)=D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
105	35 39 104	3eqtrd	$$⊢\phi \to \left(\left(\frac{{\left(M+B\right)}^2}{4}\right)-\left(\frac{\frac{C^2}{4}}{M}\right)\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=D\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
106	34 9 15 6 105	mulcan2ad	$$⊢\phi \to \left(\frac{{\left(M+B\right)}^2}{4}\right)-\left(\frac{\frac{C^2}{4}}{M}\right)=D$$
107	24 106	eqtrd	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2-\left(\frac{\frac{C^2}{4}}{M}\right)=D$$