Theorem dquartlem1

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

	Ref	Expression
Hypotheses	dquart.b	|- ( ph -> B e. CC )
	dquart.c	|- ( ph -> C e. CC )
	dquart.x	|- ( ph -> X e. CC )
	dquart.s	|- ( ph -> S e. CC )
	dquart.m	|- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )
	dquart.m0	|- ( ph -> M =/= 0 )
	dquart.i	|- ( ph -> I e. CC )
	dquart.i2	|- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )
Assertion	dquartlem1	|- ( ph -> ( ( ( ( X ^ 2 ) + ( ( M + B ) / 2 ) ) + ( ( ( ( M / 2 ) x. X ) - ( C / 4 ) ) / S ) ) = 0 <-> ( X = ( -u S + I ) \/ X = ( -u S - I ) ) ) )

Proof

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