Theorem discrlem1 6601

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 5939	. . . . . . 7 |- 4 e. RR
2		discrlem.1	. . . . . . 7 |- A e. RR
3	1, 2	remulcl 5318	. . . . . 6 |- (4 x. A) e. RR
4	3	recn 5297	. . . . 5 |- (4 x. A) e. CC
5	4	mul01 5414	. . . 4 |- ((4 x. A) x. 0) = 0
6		discrlem1.4	. . . . . . . . . 10 |- D = -u(B / (2 x. A))
7		discrlem.2	. . . . . . . . . . . 12 |- B e. RR
8		2re 5936	. . . . . . . . . . . . 13 |- 2 e. RR
9	8, 2	remulcl 5318	. . . . . . . . . . . 12 |- (2 x. A) e. RR
10		2cn 5937	. . . . . . . . . . . . 13 |- 2 e. CC
11	2	recn 5297	. . . . . . . . . . . . 13 |- A e. CC
12		2ne0 5947	. . . . . . . . . . . . 13 |- 2 =/= 0
13		discrlem1.5	. . . . . . . . . . . . . 14 |- 0 < A
14	2, 13	gt0ne0i 5601	. . . . . . . . . . . . 13 |- A =/= 0
15	10, 11, 12, 14	muln0 5678	. . . . . . . . . . . 12 |- (2 x. A) =/= 0
16	7, 9, 15	redivcl 5764	. . . . . . . . . . 11 |- (B / (2 x. A)) e. RR
17	16	renegcl 5399	. . . . . . . . . 10 |- -u(B / (2 x. A)) e. RR
18	6, 17	eqeltr 1542	. . . . . . . . 9 |- D e. RR
19	18	resqcl 6568	. . . . . . . 8 |- (D^2) e. RR
20	2, 19	remulcl 5318	. . . . . . 7 |- (A x. (D^2)) e. RR
21	7, 18	remulcl 5318	. . . . . . 7 |- (B x. D) e. RR
22	20, 21	readdcl 5317	. . . . . 6 |- ((A x. (D^2)) + (B x. D)) e. RR
23	22	recn 5297	. . . . 5 |- ((A x. (D^2)) + (B x. D)) e. CC
24		discrlem.3	. . . . . 6 |- C e. RR
25	24	recn 5297	. . . . 5 |- C e. CC
26	4, 23, 25	adddi 5309	. . . 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))
27	5, 26	breq12i 2624	. . 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)))
28		4pos 5949	. . . . 5 |- 0 < 4
29	1, 2, 28, 13	mulgt0i 5592	. . . 4 |- 0 < (4 x. A)
30		0re 5423	. . . . 5 |- 0 e. RR
31	22, 24	readdcl 5317	. . . . 5 |- (((A x. (D^2)) + (B x. D)) + C) e. RR
32	30, 31, 3	lemul2 5802	. . . 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))))
33	29, 32	ax-mp 7	. . 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)))
34		neg0 5398	. . . 4 |- -u0 = 0
35	7	resqcl 6568	. . . . . . 7 |- (B^2) e. RR
36	35	recn 5297	. . . . . 6 |- (B^2) e. CC
37	2, 24	remulcl 5318	. . . . . . . 8 |- (A x. C) e. RR
38	1, 37	remulcl 5318	. . . . . . 7 |- (4 x. (A x. C)) e. RR
39	38	recn 5297	. . . . . 6 |- (4 x. (A x. C)) e. CC
40	36, 39	negsubdi 5432	. . . . 5 |- -u((B^2) - (4 x. (A x. C))) = (-u(B^2) + (4 x. (A x. C)))
41	9	recn 5297	. . . . . . . . . . . . 13 |- (2 x. A) e. CC
42	41, 10, 12	divcl 5689	. . . . . . . . . . . 12 |- ((2 x. A) / 2) e. CC
43	16	recn 5297	. . . . . . . . . . . 12 |- (B / (2 x. A)) e. CC
44	42, 43, 43	mulass 5308	. . . . . . . . . . 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))))
45	7	recn 5297	. . . . . . . . . . . . . 14 |- B e. CC
46	41, 10, 45, 41, 12, 15	divmul13 5753	. . . . . . . . . . . . 13 |- (((2 x. A) / 2) x. (B / (2 x. A))) = ((B / 2) x. ((2 x. A) / (2 x. A)))
47	41, 15	divid 5736	. . . . . . . . . . . . . 14 |- ((2 x. A) / (2 x. A)) = 1
48	47	opreq2i 3967	. . . . . . . . . . . . 13 |- ((B / 2) x. ((2 x. A) / (2 x. A))) = ((B / 2) x. 1)
49	45, 10, 12	divcl 5689	. . . . . . . . . . . . . 14 |- (B / 2) e. CC
50		ax1cn 5252	. . . . . . . . . . . . . 14 |- 1 e. CC
51	49, 50	mulcom 5306	. . . . . . . . . . . . 13 |- ((B / 2) x. 1) = (1 x. (B / 2))
52	46, 48, 51	3eqtr 1497	. . . . . . . . . . . 12 |- (((2 x. A) / 2) x. (B / (2 x. A))) = (1 x. (B / 2))
53	52	opreq1i 3966	. . . . . . . . . . 11 |- ((((2 x. A) / 2) x. (B / (2 x. A))) x. (B / (2 x. A))) = ((1 x. (B / 2)) x. (B / (2 x. A)))
54	10, 11, 12	divcan3 5724	. . . . . . . . . . . 12 |- ((2 x. A) / 2) = A
55	6	opreq1i 3966	. . . . . . . . . . . . 13 |- (D^2) = (-u(B / (2 x. A))^2)
56	17	recn 5297	. . . . . . . . . . . . . 14 |- -u(B / (2 x. A)) e. CC
57	56	sqval 6559	. . . . . . . . . . . . 13 |- (-u(B / (2 x. A))^2) = (-u(B / (2 x. A)) x. -u(B / (2 x. A)))
58	43, 43	mul2neg 5430	. . . . . . . . . . . . 13 |- (-u(B / (2 x. A)) x. -u(B / (2 x. A))) = ((B / (2 x. A)) x. (B / (2 x. A)))
59	55, 57, 58	3eqtrr 1498	. . . . . . . . . . . 12 |- ((B / (2 x. A)) x. (B / (2 x. A))) = (D^2)
60	54, 59	opreq12i 3968	. . . . . . . . . . 11 |- (((2 x. A) / 2) x. ((B / (2 x. A)) x. (B / (2 x. A)))) = (A x. (D^2))
61	44, 53, 60	3eqtr3r 1502	. . . . . . . . . 10 |- (A x. (D^2)) = ((1 x. (B / 2)) x. (B / (2 x. A)))
62	10	negneg 5373	. . . . . . . . . . . . . 14 |- -u-u2 = 2
63	62	opreq1i 3966	. . . . . . . . . . . . 13 |- (-u-u2 x. (B / 2)) = (2 x. (B / 2))
64	10	negcl 5352	. . . . . . . . . . . . . 14 |- -u2 e. CC
65	64, 49	mulneg1 5428	. . . . . . . . . . . . 13 |- (-u-u2 x. (B / 2)) = -u(-u2 x. (B / 2))
66	10, 45, 12	divcan2 5695	. . . . . . . . . . . . 13 |- (2 x. (B / 2)) = B
67	63, 65, 66	3eqtr3r 1502	. . . . . . . . . . . 12 |- B = -u(-u2 x. (B / 2))
68	67, 6	opreq12i 3968	. . . . . . . . . . 11 |- (B x. D) = (-u(-u2 x. (B / 2)) x. -u(B / (2 x. A)))
69	64, 49	mulcl 5304	. . . . . . . . . . . 12 |- (-u2 x. (B / 2)) e. CC
70	69, 43	mul2neg 5430	. . . . . . . . . . 11 |- (-u(-u2 x. (B / 2)) x. -u(B / (2 x. A))) = ((-u2 x. (B / 2)) x. (B / (2 x. A)))
71	68, 70	eqtr 1493	. . . . . . . . . 10 |- (B x. D) = ((-u2 x. (B / 2)) x. (B / (2 x. A)))
72	61, 71	opreq12i 3968	. . . . . . . . 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))))
73		df-2 5927	. . . . . . . . . . . . . . . . 17 |- 2 = (1 + 1)
74	73	negeqi 5343	. . . . . . . . . . . . . . . 16 |- -u2 = -u(1 + 1)
75	50, 50	negdi 5431	. . . . . . . . . . . . . . . 16 |- -u(1 + 1) = (-u1 + -u1)
76	74, 75	eqtr 1493	. . . . . . . . . . . . . . 15 |- -u2 = (-u1 + -u1)
77	76	opreq2i 3967	. . . . . . . . . . . . . 14 |- (1 + -u2) = (1 + (-u1 + -u1))
78	50	negid 5363	. . . . . . . . . . . . . . . 16 |- (1 + -u1) = 0
79	78	opreq1i 3966	. . . . . . . . . . . . . . 15 |- ((1 + -u1) + -u1) = (0 + -u1)
80	50	negcl 5352	. . . . . . . . . . . . . . . 16 |- -u1 e. CC
81	50, 80, 80	addass 5307	. . . . . . . . . . . . . . 15 |- ((1 + -u1) + -u1) = (1 + (-u1 + -u1))
82	80	addid2 5314	. . . . . . . . . . . . . . 15 |- (0 + -u1) = -u1
83	79, 81, 82	3eqtr3 1501	. . . . . . . . . . . . . 14 |- (1 + (-u1 + -u1)) = -u1
84	77, 83	eqtr 1493	. . . . . . . . . . . . 13 |- (1 + -u2) = -u1
85	84	opreq1i 3966	. . . . . . . . . . . 12 |- ((1 + -u2) x. (B / 2)) = (-u1 x. (B / 2))
86	50, 64, 49	adddir 5310	. . . . . . . . . . . 12 |- ((1 + -u2) x. (B / 2)) = ((1 x. (B / 2)) + (-u2 x. (B / 2)))
87	49	mulm1 5455	. . . . . . . . . . . 12 |- (-u1 x. (B / 2)) = -u(B / 2)
88	85, 86, 87	3eqtr3 1501	. . . . . . . . . . 11 |- ((1 x. (B / 2)) + (-u2 x. (B / 2))) = -u(B / 2)
89	88	opreq1i 3966	. . . . . . . . . 10 |- (((1 x. (B / 2)) + (-u2 x. (B / 2))) x. (B / (2 x. A))) = (-u(B / 2) x. (B / (2 x. A)))
90	50, 49	mulcl 5304	. . . . . . . . . . 11 |- (1 x. (B / 2)) e. CC
91	90, 69, 43	adddir 5310	. . . . . . . . . 10 |- (((1 x. (B / 2)) + (-u2 x. (B / 2))) x. (B / (2 x. A))) = (((1 x. (B / 2)) x. (B / (2 x. A