Theorem dquartlem1

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)$$
Assertion	dquartlem1	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\leftrightarrow \left(X=-S+I\vee X=-S-I\right)\right)$$

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	3	sqcld	$$⊢\phi \to X^2\in ℂ$$
10		2cn	$$⊢2\in ℂ$$
11		mulcl	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to 2S\in ℂ$$
12	10 4 11	sylancr	$$⊢\phi \to 2S\in ℂ$$
13	12	sqcld	$$⊢\phi \to {2S}^2\in ℂ$$
14	5 13	eqeltrd	$$⊢\phi \to M\in ℂ$$
15	14 1	addcld	$$⊢\phi \to M+B\in ℂ$$
16	15	halfcld	$$⊢\phi \to \frac{M+B}{2}\in ℂ$$
17	9 16	addcld	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)\in ℂ$$
18	14	halfcld	$$⊢\phi \to \frac{M}{2}\in ℂ$$
19	18 3	mulcld	$$⊢\phi \to \left(\frac{M}{2}\right)X\in ℂ$$
20		4cn	$$⊢4\in ℂ$$
21	20	a1i	$$⊢\phi \to 4\in ℂ$$
22		4ne0	$$⊢4\ne 0$$
23	22	a1i	$$⊢\phi \to 4\ne 0$$
24	2 21 23	divcld	$$⊢\phi \to \frac{C}{4}\in ℂ$$
25	19 24	subcld	$$⊢\phi \to \left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\in ℂ$$
26	5 6	eqnetrrd	$$⊢\phi \to {2S}^2\ne 0$$
27		sqne0	$$⊢2S\in ℂ\to \left({2S}^2\ne 0\leftrightarrow 2S\ne 0\right)$$
28	12 27	syl	$$⊢\phi \to \left({2S}^2\ne 0\leftrightarrow 2S\ne 0\right)$$
29	26 28	mpbid	$$⊢\phi \to 2S\ne 0$$
30		mulne0b	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to \left(\left(2\ne 0\wedge S\ne 0\right)\leftrightarrow 2S\ne 0\right)$$
31	10 4 30	sylancr	$$⊢\phi \to \left(\left(2\ne 0\wedge S\ne 0\right)\leftrightarrow 2S\ne 0\right)$$
32	29 31	mpbird	$$⊢\phi \to \left(2\ne 0\wedge S\ne 0\right)$$
33	32	simprd	$$⊢\phi \to S\ne 0$$
34	25 4 33	divcld	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\in ℂ$$
35	17 34	addcld	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\in ℂ$$
36	10	a1i	$$⊢\phi \to 2\in ℂ$$
37		2ne0	$$⊢2\ne 0$$
38	37	a1i	$$⊢\phi \to 2\ne 0$$
39	35 36 38	diveq0ad	$$⊢\phi \to \left(\frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=0\leftrightarrow X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\right)$$
40	9 16 34	addassd	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)$$
41	40	oveq1d	$$⊢\phi \to \frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=\frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}$$
42	16 34	addcld	$$⊢\phi \to \left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\in ℂ$$
43	9 42 36 38	divdird	$$⊢\phi \to \frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=\left(\frac{X^2}{2}\right)+\left(\frac{\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}\right)$$
44	9 36 38	divrec2d	$$⊢\phi \to \frac{X^2}{2}=\left(\frac{1}{2}\right)X^2$$
45	19 24 4 33	divsubdird	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}=\left(\frac{\left(\frac{M}{2}\right)X}{S}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
46	18 3 4 33	div23d	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X}{S}=\left(\frac{\frac{M}{2}}{S}\right)X$$
47	4	sqvald	$$⊢\phi \to S^2=SS$$
48	47	oveq2d	$$⊢\phi \to 2S^2=2SS$$
49		sqmul	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to {2S}^2=2^2{S}^2$$
50	10 4 49	sylancr	$$⊢\phi \to {2S}^2=2^2{S}^2$$
51	10	sqvali	$$⊢2^2=2\cdot 2$$
52	51	oveq1i	$$⊢2^2{S}^2=2\cdot 2S^2$$
53	50 52	eqtrdi	$$⊢\phi \to {2S}^2=2\cdot 2S^2$$
54	4	sqcld	$$⊢\phi \to S^2\in ℂ$$
55	36 36 54	mulassd	$$⊢\phi \to 2\cdot 2S^2=22S^2$$
56	5 53 55	3eqtrd	$$⊢\phi \to M=22S^2$$
57	56	oveq1d	$$⊢\phi \to \frac{M}{2}=\frac{22S^2}{2}$$
58		mulcl	$$⊢\left(2\in ℂ\wedge S^2\in ℂ\right)\to 2S^2\in ℂ$$
59	10 54 58	sylancr	$$⊢\phi \to 2S^2\in ℂ$$
60	59 36 38	divcan3d	$$⊢\phi \to \frac{22S^2}{2}=2S^2$$
61	57 60	eqtrd	$$⊢\phi \to \frac{M}{2}=2S^2$$
62	36 4 4	mulassd	$$⊢\phi \to 2SS=2SS$$
63	48 61 62	3eqtr4d	$$⊢\phi \to \frac{M}{2}=2SS$$
64	63	oveq1d	$$⊢\phi \to \frac{\frac{M}{2}}{S}=\frac{2SS}{S}$$
65	12 4 33	divcan4d	$$⊢\phi \to \frac{2SS}{S}=2S$$
66	64 65	eqtrd	$$⊢\phi \to \frac{\frac{M}{2}}{S}=2S$$
67	66	oveq1d	$$⊢\phi \to \left(\frac{\frac{M}{2}}{S}\right)X=2SX$$
68	46 67	eqtrd	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X}{S}=2SX$$
69	68	oveq1d	$$⊢\phi \to \left(\frac{\left(\frac{M}{2}\right)X}{S}\right)-\left(\frac{\frac{C}{4}}{S}\right)=2SX-\left(\frac{\frac{C}{4}}{S}\right)$$
70	45 69	eqtrd	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}=2SX-\left(\frac{\frac{C}{4}}{S}\right)$$
71	70	oveq2d	$$⊢\phi \to \left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=\left(\frac{M+B}{2}\right)+2SX-\left(\frac{\frac{C}{4}}{S}\right)$$
72	12 3	mulcld	$$⊢\phi \to 2SX\in ℂ$$
73	24 4 33	divcld	$$⊢\phi \to \frac{\frac{C}{4}}{S}\in ℂ$$
74	16 72 73	addsub12d	$$⊢\phi \to \left(\frac{M+B}{2}\right)+2SX-\left(\frac{\frac{C}{4}}{S}\right)=2SX+\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
75	71 74	eqtrd	$$⊢\phi \to \left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=2SX+\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
76	75	oveq1d	$$⊢\phi \to \frac{\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=\frac{2SX+\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)}{2}$$
77	16 73	subcld	$$⊢\phi \to \left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)\in ℂ$$
78	72 77 36 38	divdird	$$⊢\phi \to \frac{2SX+\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)}{2}=\left(\frac{2SX}{2}\right)+\left(\frac{\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)}{2}\right)$$
79	36 4 3	mulassd	$$⊢\phi \to 2SX=2SX$$
80	79	oveq1d	$$⊢\phi \to \frac{2SX}{2}=\frac{2SX}{2}$$
81	4 3	mulcld	$$⊢\phi \to SX\in ℂ$$
82	81 36 38	divcan3d	$$⊢\phi \to \frac{2SX}{2}=SX$$
83	80 82	eqtrd	$$⊢\phi \to \frac{2SX}{2}=SX$$
84	54	negcld	$$⊢\phi \to -S^2\in ℂ$$
85	1	halfcld	$$⊢\phi \to \frac{B}{2}\in ℂ$$
86	84 85	subcld	$$⊢\phi \to -S^2-\left(\frac{B}{2}\right)\in ℂ$$
87	54 86 73	subsub4d	$$⊢\phi \to S^2-\left(-S^2-\left(\frac{B}{2}\right)\right)-\left(\frac{\frac{C}{4}}{S}\right)=S^2-\left(\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)\right)$$
88	14 1 36 38	divdird	$$⊢\phi \to \frac{M+B}{2}=\left(\frac{M}{2}\right)+\left(\frac{B}{2}\right)$$
89	54	2timesd	$$⊢\phi \to 2S^2=S^2+S^2$$
90	61 89	eqtrd	$$⊢\phi \to \frac{M}{2}=S^2+S^2$$
91	90	oveq1d	$$⊢\phi \to \left(\frac{M}{2}\right)+\left(\frac{B}{2}\right)=S^2+S^2+\left(\frac{B}{2}\right)$$
92	88 91	eqtrd	$$⊢\phi \to \frac{M+B}{2}=S^2+S^2+\left(\frac{B}{2}\right)$$
93	54 54 85	addassd	$$⊢\phi \to S^2+S^2+\left(\frac{B}{2}\right)=S^2+S^2+\left(\frac{B}{2}\right)$$
94	54 85	addcld	$$⊢\phi \to S^2+\left(\frac{B}{2}\right)\in ℂ$$
95	54 94	subnegd	$$⊢\phi \to S^2-\left(-\left(S^2+\left(\frac{B}{2}\right)\right)\right)=S^2+S^2+\left(\frac{B}{2}\right)$$
96	54 85	negdi2d	$$⊢\phi \to -\left(S^2+\left(\frac{B}{2}\right)\right)=-S^2-\left(\frac{B}{2}\right)$$
97	96	oveq2d	$$⊢\phi \to S^2-\left(-\left(S^2+\left(\frac{B}{2}\right)\right)\right)=S^2-\left(-S^2-\left(\frac{B}{2}\right)\right)$$
98	95 97	eqtr3d	$$⊢\phi \to S^2+S^2+\left(\frac{B}{2}\right)=S^2-\left(-S^2-\left(\frac{B}{2}\right)\right)$$
99	92 93 98	3eqtrd	$$⊢\phi \to \frac{M+B}{2}=S^2-\left(-S^2-\left(\frac{B}{2}\right)\right)$$
100	99	oveq1d	$$⊢\phi \to \left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)=S^2-\left(-S^2-\left(\frac{B}{2}\right)\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
101	8	oveq2d	$$⊢\phi \to S^2-I^2=S^2-\left(\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)\right)$$
102	87 100 101	3eqtr4d	$$⊢\phi \to \left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)=S^2-I^2$$
103	102	oveq1d	$$⊢\phi \to \frac{\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)}{2}=\frac{S^2-I^2}{2}$$
104	83 103	oveq12d	$$⊢\phi \to \left(\frac{2SX}{2}\right)+\left(\frac{\left(\frac{M+B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)}{2}\right)=SX+\left(\frac{S^2-I^2}{2}\right)$$
105	76 78 104	3eqtrd	$$⊢\phi \to \frac{\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=SX+\left(\frac{S^2-I^2}{2}\right)$$
106	44 105	oveq12d	$$⊢\phi \to \left(\frac{X^2}{2}\right)+\left(\frac{\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}\right)=\left(\frac{1}{2}\right)X^2+SX+\left(\frac{S^2-I^2}{2}\right)$$
107	41 43 106	3eqtrd	$$⊢\phi \to \frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=\left(\frac{1}{2}\right)X^2+SX+\left(\frac{S^2-I^2}{2}\right)$$
108	107	eqeq1d	$$⊢\phi \to \left(\frac{X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}{2}=0\leftrightarrow \left(\frac{1}{2}\right)X^2+SX+\left(\frac{S^2-I^2}{2}\right)=0\right)$$
109	39 108	bitr3d	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\leftrightarrow \left(\frac{1}{2}\right)X^2+SX+\left(\frac{S^2-I^2}{2}\right)=0\right)$$
110		ax-1cn	$$⊢1\in ℂ$$
111		halfcl	$$⊢1\in ℂ\to \frac{1}{2}\in ℂ$$
112	110 111	mp1i	$$⊢\phi \to \frac{1}{2}\in ℂ$$
113		ax-1ne0	$$⊢1\ne 0$$
114	110 10 113 37	divne0i	$$⊢\frac{1}{2}\ne 0$$
115	114	a1i	$$⊢\phi \to \frac{1}{2}\ne 0$$
116	7	sqcld	$$⊢\phi \to I^2\in ℂ$$
117	54 116	subcld	$$⊢\phi \to S^2-I^2\in ℂ$$
118	117	halfcld	$$⊢\phi \to \frac{S^2-I^2}{2}\in ℂ$$
119	110	a1i	$$⊢\phi \to 1\in ℂ$$
120		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
121	120	a1i	$$⊢\phi \to \left(2\in ℂ\wedge 2\ne 0\right)$$
122		divmuldiv	$$⊢\left(\left(1\in ℂ\wedge S^2-I^2\in ℂ\right)\wedge \left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\right)\to \left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=\frac{1\left(S^2-I^2\right)}{2\cdot 2}$$
123	119 117 121 121 122	syl22anc	$$⊢\phi \to \left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=\frac{1\left(S^2-I^2\right)}{2\cdot 2}$$
124	117	mulid2d	$$⊢\phi \to 1\left(S^2-I^2\right)=S^2-I^2$$
125		2t2e4	$$⊢2\cdot 2=4$$
126	125	a1i	$$⊢\phi \to 2\cdot 2=4$$
127	124 126	oveq12d	$$⊢\phi \to \frac{1\left(S^2-I^2\right)}{2\cdot 2}=\frac{S^2-I^2}{4}$$
128	123 127	eqtrd	$$⊢\phi \to \left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=\frac{S^2-I^2}{4}$$
129	128	oveq2d	$$⊢\phi \to 4\left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=4\left(\frac{S^2-I^2}{4}\right)$$
130	117 21 23	divcan2d	$$⊢\phi \to 4\left(\frac{S^2-I^2}{4}\right)=S^2-I^2$$
131	129 130	eqtrd	$$⊢\phi \to 4\left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=S^2-I^2$$
132	131	oveq2d	$$⊢\phi \to S^2-4\left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)=S^2-\left(S^2-I^2\right)$$
133	54 116	nncand	$$⊢\phi \to S^2-\left(S^2-I^2\right)=I^2$$
134	132 133	eqtr2d	$$⊢\phi \to I^2=S^2-4\left(\frac{1}{2}\right)\left(\frac{S^2-I^2}{2}\right)$$
135	112 115 4 118 3 7 134	quad2	$$⊢\phi \to \left(\left(\frac{1}{2}\right)X^2+SX+\left(\frac{S^2-I^2}{2}\right)=0\leftrightarrow \left(X=\frac{-S+I}{2\left(\frac{1}{2}\right)}\vee X=\frac{-S-I}{2\left(\frac{1}{2}\right)}\right)\right)$$
136	10 37	recidi	$$⊢2\left(\frac{1}{2}\right)=1$$
137	136	oveq2i	$$⊢\frac{-S+I}{2\left(\frac{1}{2}\right)}=\frac{-S+I}{1}$$
138	4	negcld	$$⊢\phi \to -S\in ℂ$$
139	138 7	addcld	$$⊢\phi \to -S+I\in ℂ$$
140	139	div1d	$$⊢\phi \to \frac{-S+I}{1}=-S+I$$
141	137 140	syl5eq	$$⊢\phi \to \frac{-S+I}{2\left(\frac{1}{2}\right)}=-S+I$$
142	141	eqeq2d	$$⊢\phi \to \left(X=\frac{-S+I}{2\left(\frac{1}{2}\right)}\leftrightarrow X=-S+I\right)$$
143	136	oveq2i	$$⊢\frac{-S-I}{2\left(\frac{1}{2}\right)}=\frac{-S-I}{1}$$
144	138 7	subcld	$$⊢\phi \to -S-I\in ℂ$$
145	144	div1d	$$⊢\phi \to \frac{-S-I}{1}=-S-I$$
146	143 145	syl5eq	$$⊢\phi \to \frac{-S-I}{2\left(\frac{1}{2}\right)}=-S-I$$
147	146	eqeq2d	$$⊢\phi \to \left(X=\frac{-S-I}{2\left(\frac{1}{2}\right)}\leftrightarrow X=-S-I\right)$$
148	142 147	orbi12d	$$⊢\phi \to \left(\left(X=\frac{-S+I}{2\left(\frac{1}{2}\right)}\vee X=\frac{-S-I}{2\left(\frac{1}{2}\right)}\right)\leftrightarrow \left(X=-S+I\vee X=-S-I\right)\right)$$
149	109 135 148	3bitrd	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\leftrightarrow \left(X=-S+I\vee X=-S-I\right)\right)$$