Theorem discrlem1 4713

Description: Lemma for discriminant theorem.

Hypotheses

Ref	Expression
discrlem.1	|- A e. RR
discrlem.2	|- B e. RR
discrlem.3	|- C e. RR
discrlem1.4	|- D = -u(B / (2 x. A))
discrlem1.5	|- 0 < A

Assertion

Ref	Expression
discrlem1	|- (0 <_ (((A x. (D^2)) + (B x. D)) + C) <-> ((B^2) - (4 x. (A x. C))) <_ 0)

Proof of Theorem discrlem1

Step	Hyp	Ref	Expression
1		4re 4473	. . . . . . 7 |- 4 e. RR
2	1	recn 4098	. . . . . 6 |- 4 e. CC
3		discrlem.1	. . . . . . 7 |- A e. RR
4	3	recn 4098	. . . . . 6 |- A e. CC
5	2, 4	mulcl 4105	. . . . 5 |- (4 x. A) e. CC
6	5	mulzer1 4185	. . . 4 |- ((4 x. A) x. 0) = 0
7		discrlem1.4	. . . . . . . . . 10 |- D = -u(B / (2 x. A))
8		discrlem.2	. . . . . . . . . . . 12 |- B e. RR
9		2re 4470	. . . . . . . . . . . . 13 |- 2 e. RR
10	9, 3	remulcl 4119	. . . . . . . . . . . 12 |- (2 x. A) e. RR
11		2cn 4471	. . . . . . . . . . . . 13 |- 2 e. CC
12		2pos 4479	. . . . . . . . . . . . . 14 |- 0 < 2
13	9, 12	gt0ne0i 4345	. . . . . . . . . . . . 13 |- 2 =/= 0
14		discrlem1.5	. . . . . . . . . . . . . 14 |- 0 < A
15	3, 14	gt0ne0i 4345	. . . . . . . . . . . . 13 |- A =/= 0
16	11, 4, 13, 15	muln0 4214	. . . . . . . . . . . 12 |- (2 x. A) =/= 0
17	8, 10, 16	redivcl 4274	. . . . . . . . . . 11 |- (B / (2 x. A)) e. RR
18	17	renegcl 4171	. . . . . . . . . 10 |- -u(B / (2 x. A)) e. RR
19	7, 18	eqeltr 1159	. . . . . . . . 9 |- D e. RR
20	19	recn 4098	. . . . . . . 8 |- D e. CC
21	20	sqcl 4686	. . . . . . 7 |- (D^2) e. CC
22	4, 21	mulcl 4105	. . . . . 6 |- (A x. (D^2)) e. CC
23	8	recn 4098	. . . . . . 7 |- B e. CC
24	10	recn 4098	. . . . . . . . . 10 |- (2 x. A) e. CC
25	23, 24, 16	divcl 4221	. . . . . . . . 9 |- (B / (2 x. A)) e. CC
26	25	negcl 4142	. . . . . . . 8 |- -u(B / (2 x. A)) e. CC
27	7, 26	eqeltr 1159	. . . . . . 7 |- D e. CC
28	23, 27	mulcl 4105	. . . . . 6 |- (B x. D) e. CC
29	22, 28	addcl 4104	. . . . 5 |- ((A x. (D^2)) + (B x. D)) e. CC
30		discrlem.3	. . . . . 6 |- C e. RR
31	30	recn 4098	. . . . 5 |- C e. CC
32	5, 29, 31	adddi 4110	. . . 4 |- ((4 x. A) x. (((A x. (D^2)) + (B x. D)) + C)) = (((4 x. A) x. ((A x. (D^2)) + (B x. D))) + ((4 x. A) x. C))
33	6, 32	breq12i 2070	. . 3 |- (((4 x. A) x. 0) <_ ((4 x. A) x. (((A x. (D^2)) + (B x. D)) + C)) <-> 0 <_ (((4 x. A) x. ((A x. (D^2)) + (B x. D))) + ((4 x. A) x. C)))
34		4pos 4481	. . . . 5 |- 0 < 4
35	1, 3, 34, 14	mulgt0i 4336	. . . 4 |- 0 < (4 x. A)
36		ax0re 4063	. . . . 5 |- 0 e. RR
37	19	sqrecl 4699	. . . . . . . 8 |- (D^2) e. RR
38	3, 37	remulcl 4119	. . . . . . 7 |- (A x. (D^2)) e. RR
39	8, 19	remulcl 4119	. . . . . . 7 |- (B x. D) e. RR
40	38, 39	readdcl 4118	. . . . . 6 |- ((A x. (D^2)) + (B x. D)) e. RR
41	40, 30	readdcl 4118	. . . . 5 |- (((A x. (D^2)) + (B x. D)) + C) e. RR
42	1, 3	remulcl 4119	. . . . 5 |- (4 x. A) e. RR
43	36, 41, 42	lemul2 4396	. . . 4 |- (0 < (4 x. A) -> (0 <_ (((A x. (D^2)) + (B x. D)) + C) <-> ((4 x. A) x. 0) <_ ((4 x. A) x. (((A x. (D^2)) + (B x. D)) + C))))
44	35, 43	ax-mp 6	. . 3 |- (0 <_ (((A x. (D^2)) + (B x. D)) + C) <-> ((4 x. A) x. 0) <_ ((4 x. A) x. (((A x. (D^2)) + (B x. D)) + C)))
45		neg0 4170	. . . 4 |- -u0 = 0
46	8	sqrecl 4699	. . . . . . 7 |- (B^2) e. RR
47	46	recn 4098	. . . . . 6 |- (B^2) e. CC
48	4, 31	mulcl 4105	. . . . . . 7 |- (A x. C) e. CC
49	2, 48	mulcl 4105	. . . . . 6 |- (4 x. (A x. C)) e. CC
50	47, 49	negdi2 4194	. . . . 5 |- -u((B^2) - (4 x. (A x. C))) = (-u(B^2) + (4 x. (A x. C)))
51	24, 11, 13	divcl 4221	. . . . . . . . . . . 12 |- ((2 x. A) / 2) e. CC
52	51, 25, 25	mulass 4109	. . . . . . . . . . 11 |- ((((2 x. A) / 2) x. (B / (2 x. A))) x. (B / (2 x. A))) = (((2 x. A) / 2) x. ((B / (2 x. A)) x. (B / (2 x. A))))
53	24, 11, 23, 24, 13, 16	divmul13 4267	. . . . . . . . . . . . 13 |- (((2 x. A) / 2) x. (B / (2 x. A))) = ((B / 2) x. ((2 x. A) / (2 x. A)))
54	24, 16	divid 4254	. . . . . . . . . . . . . 14 |- ((2 x. A) / (2 x. A)) = 1
55	54	opreq2i 3010	. . . . . . . . . . . . 13 |- ((B / 2) x. ((2 x. A) / (2 x. A))) = ((B / 2) x. 1)
56	23, 11, 13	divcl 4221	. . . . . . . . . . . . . 14 |- (B / 2) e. CC
57		1cn 4101	. . . . . . . . . . . . . 14 |- 1 e. CC
58	56, 57	mulcom 4107	. . . . . . . . . . . . 13 |- ((B / 2) x. 1) = (1 x. (B / 2))
59	53, 55, 58	3eqtr 1123	. . . . . . . . . . . 12 |- (((2 x. A) / 2) x. (B / (2 x. A))) = (1 x. (B / 2))
60	59	opreq1i 3009	. . . . . . . . . . 11 |- ((((2 x. A) / 2) x. (B / (2 x. A))) x. (B / (2 x. A))) = ((1 x. (B / 2)) x. (B / (2 x. A)))
61	11, 4, 13	divcan3 4247	. . . . . . . . . . . 12 |- ((2 x. A) / 2) = A
62	7	opreq1i 3009	. . . . . . . . . . . . 13 |- (D^2) = (-u(B / (2 x. A))^2)
63	18	recn 4098	. . . . . . . . . . . . . . 15 |- -u(B / (2 x. A)) e. CC
64	63	sqval 4685	. . . . . . . . . . . . . 14 |- (-u(B / (2 x. A))^2) = (-u(B / (2 x. A)) x. -u(B / (2 x. A)))
65	25, 25	mul2neg 4192	. . . . . . . . . . . . . 14 |- (-u(B / (2 x. A)) x. -u(B / (2 x. A))) = ((B / (2 x. A)) x. (B / (2 x. A)))
66	64, 65	eqtr 1119	. . . . . . . . . . . . 13 |- (-u(B / (2 x. A))^2) = ((B / (2 x. A)) x. (B / (2 x. A)))
67	62, 66	eqtr2 1120	. . . . . . . . . . . 12 |- ((B / (2 x. A)) x. (B / (2 x. A))) = (D^2)
68	61, 67	opreq12i 3011	. . . . . . . . . . 11 |- (((2 x. A) / 2) x. ((B / (2 x. A)) x. (B / (2 x. A)))) = (A x. (D^2))
69	52, 60, 68	3eqtr3r 1125	. . . . . . . . . 10 |- (A x. (D^2)) = ((1 x. (B / 2)) x. (B / (2 x. A)))
70	11	negneg 4154	. . . . . . . . . . . . . 14 |- -u-u2 = 2
71	70	opreq1i 3009	. . . . . . . . . . . . 13 |- (-u-u2 x. (B / 2)) = (2 x. (B / 2))
72	11	negcl 4142	. . . . . . . . . . . . . 14 |- -u2 e. CC
73	72, 56	mulneg1 4190	. . . . . . . . . . . . 13 |- (-u-u2 x. (B / 2)) = -u(-u2 x. (B / 2))
74	11, 23, 13	divcan2 4224	. . . . . . . . . . . . 13 |- (2 x. (B / 2)) = B
75	71, 73, 74	3eqtr3r 1125	. . . . . . . . . . . 12 |- B = -u(-u2 x. (B / 2))
76	75, 7	opreq12i 3011	. . . . . . . . . . 11 |- (B x. D) = (-u(-u2 x. (B / 2)) x. -u(B / (2 x. A)))
77	72, 56	mulcl 4105	. . . . . . . . . . . 12 |- (-u2 x. (B / 2)) e. CC
78	77, 25	mul2neg 4192	. . . . . . . . . . 11 |- (-u(-u2 x. (B / 2)) x. -u(B / (2 x. A))) = ((-u2 x. (B / 2)) x. (B / (2 x. A)))
79	76, 78	eqtr 1119	. . . . . . . . . 10 |- (B x. D) = ((-u2 x. (B / 2)) x. (B / (2 x. A)))
80	69, 79	opreq12i 3011	. . . . . . . . 9 |- ((A x. (D^2)) + (B x. D)) = (((1 x. (B / 2)) x. (B / (2 x. A))) + ((-u2 x. (B / 2)) x. (B / (2 x. A))))
81		df-2 4462	. . . . . . . . . . . . . . . . 17 |- 2 = (1 + 1)
82	81	negeqi 4137	. . . . . . . . . . . . . . . 16 |- -u2 = -u(1 + 1)
83	57, 57	negdi 4193	. . . . . . . . . . . . . . . 16 |- -u(1 + 1) = (-u1 + -u1)
84	82, 83	eqtr 1119	. . . . . . . . . . . . . . 15 |- -u2 = (-u1 + -u1)
85	84	opreq2i 3010	. . . . . . . . . . . . . 14 |- (1 + -u2) = (1 + (-u1 + -u1))
86	57	negid 4147	. . . . . . . . . . . . . . . 16 |- (1 + -u1) = 0
87	86	opreq1i 3009	. . . . . . . . . . . . . . 15 |- ((1 + -u1) + -u1) = (0 + -u1)
88	57	negcl 4142	. . . . . . . . . . . . . . . 16 |- -u1 e. CC
89	57, 88, 88	addass 4108	. . . . . . . . . . . . . . 15 |- ((1 + -u1) + -u1) = (1 + (-u1 + -u1))
90	88	addid2 4113	. . . . . . . . . . . . . . 15 |- (0 + -u1) = -u1
91	87, 89, 90	3eqtr3 1124	. . . . . . . . . . . . . 14 |- (1 + (-u1 + -u1)) = -u1
92	85, 91	eqtr 1119	. . . . . . . . . . . . 13 |- (1 + -u2) = -u1
93	92	opreq1i 3009	. . . . . . . . . . . 12 |- ((1 + -u2) x. (B / 2)) = (-u1 x. (B / 2))
94	57, 72, 56	adddir 4111	. . . . . . . . . . . 12 |- ((1 + -u2) x. (B / 2)) = ((1 x. (B / 2)) + (-u2 x. (B / 2)))
95	56	mulm1 4205	. . . . . . . . . . . 12 |- (-u1 x. (B / 2)) = -u(B / 2)
96	93, 94, 95	3eqtr3 1124	. . . . . . . . . . 11 |- ((1 x. (B / 2)) + (-u2 x. (B / 2))) = -u(B / 2)
97	96	opreq1i 3009	. . . . . . . . . 10 |- (((1 x. (B / 2)) + (-u2 x. (B / 2))) x. (B / (2 x. A))) = (-u(B / 2) x. (B / (2 x. A)))
98	57, 56	mulcl 4105	. . . . . . . . . . 11 |- (1 x. (B / 2)) e. CC
99	98, 77, 25	adddir 4111	. . . . . . . . . 10 |- (((1 x. (B / 2)) + (-u2 x. (B / 2