Theorem discrlem1 4713

Description: Lemma for discriminant theorem.

Hypotheses

Ref	Expression
discrlem.1	⊢ A ∈ ℝ
discrlem.2	⊢ B ∈ ℝ
discrlem.3	⊢ C ∈ ℝ
discrlem1.4	⊢ D = -(B / (2 · A))
discrlem1.5	⊢ 0 < A

Assertion

Ref	Expression
discrlem1	⊢ (0 ≤ (((A · (D↑2)) + (B · D)) + C) ↔ ((B↑2) − (4 · (A · C))) ≤ 0)

Proof of Theorem discrlem1

Step	Hyp	Ref	Expression
1		4re 4473	. . . . . . 7 ⊢ 4 ∈ ℝ
2	1	recn 4098	. . . . . 6 ⊢ 4 ∈ ℂ
3		discrlem.1	. . . . . . 7 ⊢ A ∈ ℝ
4	3	recn 4098	. . . . . 6 ⊢ A ∈ ℂ
5	2, 4	mulcl 4105	. . . . 5 ⊢ (4 · A) ∈ ℂ
6	5	mulzer1 4185	. . . 4 ⊢ ((4 · A) · 0) = 0
7		discrlem1.4	. . . . . . . . . 10 ⊢ D = -(B / (2 · A))
8		discrlem.2	. . . . . . . . . . . 12 ⊢ B ∈ ℝ
9		2re 4470	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
10	9, 3	remulcl 4119	. . . . . . . . . . . 12 ⊢ (2 · A) ∈ ℝ
11		2cn 4471	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
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 · A) ≠ 0
17	8, 10, 16	redivcl 4274	. . . . . . . . . . 11 ⊢ (B / (2 · A)) ∈ ℝ
18	17	renegcl 4171	. . . . . . . . . 10 ⊢ -(B / (2 · A)) ∈ ℝ
19	7, 18	eqeltr 1159	. . . . . . . . 9 ⊢ D ∈ ℝ
20	19	recn 4098	. . . . . . . 8 ⊢ D ∈ ℂ
21	20	sqcl 4686	. . . . . . 7 ⊢ (D↑2) ∈ ℂ
22	4, 21	mulcl 4105	. . . . . 6 ⊢ (A · (D↑2)) ∈ ℂ
23	8	recn 4098	. . . . . . 7 ⊢ B ∈ ℂ
24	10	recn 4098	. . . . . . . . . 10 ⊢ (2 · A) ∈ ℂ
25	23, 24, 16	divcl 4221	. . . . . . . . 9 ⊢ (B / (2 · A)) ∈ ℂ
26	25	negcl 4142	. . . . . . . 8 ⊢ -(B / (2 · A)) ∈ ℂ
27	7, 26	eqeltr 1159	. . . . . . 7 ⊢ D ∈ ℂ
28	23, 27	mulcl 4105	. . . . . 6 ⊢ (B · D) ∈ ℂ
29	22, 28	addcl 4104<&TD>	. . . . 5 ⊢ ((A · (D↑2)) + (B · D)) ∈ ℂ
30		discrlem.3	. . . . . 6 ⊢ C ∈ ℝ
31	30	recn 4098	. . . . 5 ⊢ C ∈ ℂ
32	5, 29, 31	adddi 4110	. . . 4 ⊢ ((4 · A) · (((A · (D↑2)) + (B · D)) + C)) = (((4 · A) · ((A · (D↑2)) + (B · D))) + ((4 · A) · C))
33	6, 32	breq12i 2070	. . 3 ⊢ (((4 · A) · 0) ≤ ((4 · A) · (((A · (D↑2)) + (B · D)) + C)) ↔ 0 ≤ (((4 · A) · ((A · (D↑2)) + (B · D))) + ((4 · A) · C)))
34		4pos 4481	. . . . 5 ⊢ 0 < 4
35	1, 3, 34, 14	mulgt0i 4336	. . . 4 ⊢ 0 < (4 · A)
36		ax0re 4063	. . . . 5 ⊢ 0 ∈ ℝ
37	19	sqrecl 4699	. . . . . . . 8 ⊢ (D↑2) ∈ ℝ
38	3, 37	remulcl 4119	. . . . . . 7 ⊢ (A · (D↑2)) ∈ ℝ
39	8, 19	remulcl 4119	. . . . . . 7 ⊢ (B · D) ∈ ℝ
40	38, 39	readdcl 4118	. . . . . 6 ⊢ ((A · (D↑2)) + (B · D)) ∈ ℝ
41	40, 30	readdcl 4118	. . . . 5 ⊢ (((A · (D↑2)) + (B · D)) + C) ∈ ℝ
42	1, 3	remulcl 4119	. . . . 5 ⊢ (4 · A) ∈ ℝ
43	36, 41, 42	lemul2 4396	. . . 4 ⊢ (0 < (4 · A) → (0 ≤ (((A · (D↑2)) + (B · D)) + C) ↔ ((4 · A) · 0) ≤ ((4 · A) · (((A · (D↑2)) + (B · D)) + C))))
44	35, 43	ax-mp 6	. . 3 ⊢ (0 ≤ (((A · (D↑2)) + (B · D)) + C) ↔ ((4 · A) · 0) ≤ ((4 · A) · (((A · (D↑2)) + (B · D)) + C)))
45		neg0 4170	. . . 4 ⊢ -0 = 0
46	8	sqrecl 4699	. . . . . . 7 ⊢ (B↑2) ∈ ℝ
47	46	recn 4098	. . . . . 6 ⊢ (B↑2) ∈ ℂ
48	4, 31	mulcl 4105	. . . . . . 7 ⊢ (A · C) ∈ ℂ
49	2, 48	mulcl 4105	. . . . . 6 ⊢ (4 · (A · C)) ∈ ℂ
50	47, 49	negdi2 4194	. . . . 5 ⊢ -((B↑2) − (4 · (A · C))) = (-(B↑2) + (4 · (A · C)))
51	24, 11, 13	divcl 4221	. . . . . . . . . . . 12 ⊢ ((2 · A) / 2) ∈ ℂ
52	51, 25, 25	mulass 4109	. . . . . . . . . . 11 ⊢ ((((2 · A) / 2) · (B / (2 · A))) · (B / (2 · A))) = (((2 · A) / 2) · ((B / (2 · A)) · (B / (2 · A))))
53	24, 11, 23, 24, 13, 16	divmul13 4267	. . . . . . . . . . . . 13 ⊢ (((2 · A) / 2) · (B / (2 · A))) = ((B / 2) · ((2 · A) / (2 · A)))
54	24, 16	divid 4254	. . . . . . . . . . . . . 14 ⊢ ((2 · A) / (2 · A)) = 1
55	54	opreq2i 3010	. . . . . . . . . . . . 13 ⊢ ((B / 2) · ((2 · A) / (2 · A))) = ((B / 2) · 1)
56	23, 11, 13	divcl 4221	. . . . . . . . . . . . . 14 ⊢ (B / 2) ∈ ℂ
57		1cn 4101	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
58	56, 57	mulcom 4107	. . . . . . . . . . . . 13 ⊢ ((B / 2) · 1) = (1 · (B / 2))
59	53, 55, 58	3eqtr 1123	. . . . . . . . . . . 12 ⊢ (((2 · A) / 2) · (B / (2 · A))) = (1 · (B / 2))
60	59	opreq1i 3009	. . . . . . . . . . 11 ⊢ ((((2 · A) / 2) · (B / (2 · A))) · (B / (2 · A))) = ((1 · (B / 2)) · (B / (2 · A)))
61	11, 4, 13	divcan3 4247	. . . . . . . . . . . 12 ⊢ ((2 · A) / 2) = A
62	7	opreq1i 3009	. . . . . . . . . . . . 13 ⊢ (D↑2) = (-(B / (2 · A))↑2)
63	18	recn 4098	. . . . . . . . . . . . . . 15 ⊢ -(B / (2 · A)) ∈ ℂ
64	63	sqval 4685	. . . . . . . . . . . . . 14 ⊢ (-(B / (2 · A))↑2) = (-(B / (2 · A)) · -(B / (2 · A)))
65	25, 25	mul2neg 4192	. . . . . . . . . . . . . 14 ⊢ (-(B / (2 · A)) · -(B / (2 · A))) = ((B / (2 · A)) · (B / (2 · A)))
66	64, 65	eqtr 1119	. . . . . . . . . . . . 13 ⊢ (-(B / (2 · A))↑2) = ((B / (2 · A)) · (B / (2 · A)))
67	62, 66	eqtr2 1120	. . . . . . . . . . . 12 ⊢ ((B / (2 · A)) · (B / (2 · A))) = (D↑2)
68	61, 67	opreq12i 3011	. . . . . . . . . . 11 ⊢ (((2 · A) / 2) · ((B / (2 · A)) · (B / (2 · A)))) = (A · (D↑2))
69	52, 60, 68	3eqtr3r 1125	. . . . . . . . . 10 ⊢ (A · (D↑2)) = ((1 · (B / 2)) · (B / (2 · A)))
70	11	negneg 4154	. . . . . . . . . . . . . 14 ⊢ --2 = 2
71	70	opreq1i 3009	. . . . . . . . . . . . 13 ⊢ (--2 · (B / 2)) = (2 · (B / 2))
72	11	negcl 4142	. . . . . . . . . . . . . 14 ⊢ -2 ∈ ℂ
73	72, 56	mulneg1 4190	. . . . . . . . . . . . 13 ⊢ (--2 · (B / 2)) = -(-2 · (B / 2))
74	11, 23, 13	divcan2 4224	. . . . . . . . . . . . 13 ⊢ (2 · (B / 2)) = B
75	71, 73, 74	3eqtr3r 1125	. . . . . . . . . . . 12 ⊢ B = -(-2 · (B / 2))
76	75, 7	opreq12i 3011	. . . . . . . . . . 11 ⊢ (B · D) = (-(-2 · (B / 2)) · -(B / (2 · A)))
77	72, 56	mulcl 4105	. . . . . . . . . . . 12 ⊢ (-2 · (B / 2)) ∈ ℂ
78	77, 25	mul2neg 4192	. . . . . . . . . . 11 ⊢ (-(-2 · (B / 2)) · -(B / (2 · A))) = ((-2 · (B / 2)) · (B / (2 · A)))
79	76, 78	eqtr 1119	. . . . . . . . . 10 ⊢ (B · D) = ((-2 · (B / 2)) · (B / (2 · A)))
80	69, 79	opreq12i 3011	. . . . . . . . 9 ⊢ ((A · (D↑2)) + (B · D)) = (((1 · (B / 2)) · (B / (2 · A))) + ((-2 · (B / 2)) · (B / (2 · A))))
81		df-2 4462	. . . . . . . . . . . . . . . . 17 ⊢ 2 = (1 + 1)
82	81	negeqi 4137	. . . . . . . . . . . . . . . 16 ⊢ -2 = -(1 + 1)
83	57, 57	negdi 4193	. . . . . . . . . . . . . . . 16 ⊢ -(1 + 1) = (-1 + -1)
84	82, 83	eqtr 1119	. . . . . . . . . . . . . . 15 ⊢ -2 = (-1 + -1)
85	84	opreq2i 3010	. . . . . . . . . . . . . 14 ⊢ (1 + -2) = (1 + (-1 + -1))
86	57	negid 4147	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
87	86	opreq1i 3009	. . . . . . . . . . . . . . 15 ⊢ ((1 + -1) + -1) = (0 + -1)
88	57	negcl 4142	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
89	57, 88, 88	addass 4108	. . . . . . . . . . . . . . 15 ⊢ ((1 + -1) + -1) = (1 + (-1 + -1))
90	88	addid2 4113	. . . . . . . . . . . . . . 15 ⊢ (0 + -1) = -1
91	87, 89, 90	3eqtr3 1124	. . . . . . . . . . . . . 14 ⊢ (1 + (-1 + -1)) = -1
92	85, 91	eqtr 1119	. . . . . . . . . . . . 13 ⊢ (1 + -2) = -1
93	92	opreq1i 3009	. . . . . . . . . . . 12 ⊢ ((1 + -2) · (B / 2)) = (-1 · (B / 2))
94	57, 72, 56	adddir 4111	. . . . . . . . . . . 12 ⊢ ((1 + -2) · (B / 2)) = ((1 · (B / 2)) + (-2 · (B / 2)))
95	56	mulm1 4205	. . . . . . . . . . . 12 ⊢ (-1 · (B / 2)) = -(B / 2)
96	93, 94, 95	3eqtr3 1124	. . . . . . . . . . 11 ⊢ ((1 · (B / 2)) + (-2 · (B / 2))) = -(B / 2)
97	96	opreq1i 3009	. . . . . . . . . 10 ⊢ (((1 · (B / 2)) + (-2 · (B / 2))) · (B / (2 · A))) = (-(B / 2) · (B / (2 · A)))
98	57, 56	mulcl 4105	. . . . . . . . . . 11 ⊢ (1 · (B / 2)) ∈ ℂ
99	98, 77, 25	adddir 4111	. . . . . . . . . 10 ⊢ (((1 · (B / 2)) + (-2 · (B / 2))) · (B / (2 · A))) = (((1 · (B / 2)) · (B / (2 · A))) + ((-2 · (B / 2)) · (B / (2 · A))))
100	56, 25	mulneg1 4190	. . . . . . . . . . 11 ⊢ (-(B / 2) · (B / (2 · A))) = -((B / 2) · (B / (2 · A)))
101	23	sqval 4685	. . . . . . . . . . . . . 14 ⊢ (B↑2) = (B · B)
102		2t2e4 4503	. . . . . . . . . . . . . . . 16 ⊢ (2 · 2) = 4
103	102	opreq1i 3009	. . . . . . . . . . . . . . 15 ⊢ ((2 · 2) · A) = (4 · A)
104	11, 11, 4	mulass 4109	. . . . . . . . . . . . . . 15 ⊢ ((2 · 2) · A) = (2 · (2 · A))
105	103, 104	eqtr3 1121	. . . . . . . . . . . . . 14 ⊢ (4 · A) = (2 · (2 · A))
106	101, 105	opreq12i 3011	. . . . . . . . . . . . 13 ⊢ ((B↑2) / (4 · A)) = ((B · B) / (2 · (2 · A)))
107	23, 11, 23, 24, 13, 16	divmuldiv 4266	. . . . . . . . . . . . 13 ⊢ ((B / 2) · (B / (2 · A))) = ((B · B) / (2 · (2 · A)))
108	106, 107	eqtr4 1122	. . . . . . . . . . . 12 ⊢ ((B↑2) / (4 · A)) = ((B / 2) · (B / (2 · A)))
109	108	negeqi 4137	. . . . . . . . . . 11 ⊢ -((B↑2) / (4 · A)) = -((B / 2) · (B / (2 · A)))
110	100, 109	eqtr4 1122	. . . . . . . . . 10 ⊢ (-(B / 2) · (B / (2 · A))) = -((B↑2) / (4 · A))
111	97, 99, 110	3eqtr3 1124	. . . . . . . . 9 ⊢ (((1 · (B / 2)) · (B / (2 · A))) + ((-2 · (B / 2)) · (B / (2 · A)))) = -((B↑2) / (4 · A))
112	80, 111	eqtr 1119	. . . . . . . 8 ⊢ ((A · (D↑2)) + (B · D)) = -((B↑2) / (4 · A))
113	112	opreq2i 3010	. . . . . . 7 ⊢ ((4 · A) · ((A · (D↑2)) + (B · D))) = ((4 · A) · -((B↑2) / (4 · A)))
114	42	recn 4098	. . . . . . . 8 ⊢ (4 · A) ∈ ℂ
115	1, 34	gt0ne0i 4345	. . . . . . . . . . 11 ⊢ 4 ≠ 0
116	2, 4, 115, 15	muln0 4214	. . . . . . . . . 10 ⊢ (4 · A) ≠ 0
117	46, 42, 116	redivcl 4274	. . . . . . . . 9 ⊢ ((B↑2) / (4 · A)) ∈ ℝ
118	117	recn 4098	. . . . . . . 8 ⊢ ((B↑2) / (4 · A)) ∈ ℂ
119	114, 118	mulneg2 4191	. . . . . . 7 ⊢ ((4 · A) · -((B↑2) / (4 · A))) = -((4 · A) · ((B↑2) / (4 · A)))
120	114, 47, 116	divcan2 4224	. . . . . . . 8 ⊢ ((4 · A) · ((B↑2) / (4 · A))) = (B↑2)
121	120	negeqi 4137	. . . . . . 7 ⊢ -((4 · A) · ((B↑2) / (4 · A))) = -(B↑2)
122	113, 119, 121	3eqtr 1123	. . . . . 6 ⊢ ((4 · A) · ((A · (D↑2)) + (B · D))) = -(B↑2)
123	2, 4, 31	mulass 4109	. . . . . 6 ⊢ ((4 · A) · C) = (4 · (A · C))
124	122, 123	opreq12i 3011	. . . . 5 ⊢ (((4 · A) · ((A · (D↑2)) + (B · D))) + ((4 · A) · C)) = (-(B↑2) + (4 · (A · C)))
125	50, 124	eqtr4 1122	. . . 4 ⊢ -((B↑2) − (4 · (A · C))) = (((4 · A) · ((A · (D↑2)) + (B · D))) + ((4 · A) · C))
126	45, 125	breq12i 2070	. . 3 ⊢ (-0 ≤ -((B↑2) − (4 · (A · C))) ↔ 0 ≤ (((4 · A) · ((A · (D↑2)) + (B · D))) + ((4 · A) · C)))
127	33, 44, 126	3bitr4 158	. 2 ⊢ (0 ≤ (((A · (D↑2)) + (B · D)) + C) ↔ -0 ≤ -((B↑2) − (4 · (A · C))))
128	3, 30	remulcl 4119	. . . . 5 ⊢ (A · C) ∈ ℝ
129	1, 128	remulcl 4119	. . . 4 ⊢ (4 · (A · C)) ∈ ℝ
130	46, 129	resubcl 4174	. . 3 ⊢ ((B↑2) − (4 · (A · C))) ∈ ℝ
131	130, 36	leneg 4331	. 2 ⊢ (((B↑2) − (4 · (A · C))) ≤ 0 ↔ -0 ≤ -((B↑2) − (4 · (A · C))))
132	127, 131	bitr4 154	1 ⊢ (0 ≤ (((A · (D↑2)) + (B · D)) + C) ↔ ((B↑2) − (4 · (A · C))) ≤ 0)

Syntax hints:   ↔ wb 127   = wceq 1091   ∈ wcel 1092   class class class wbr 2054  (class class class)co 3001  ℂcc 4026  ℝcr 4027  0cc0 4028  1c1 4029   + caddc 4031   · cmulc 4032   < clt 4033   − cmin 4089  -cneg 4090   / cdiv 4091   ≤ cle 4092  2c2 4454  4c4 4456  ↑cexp 4675

This theorem is referenced by:  discrlem2 4714

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1st 3087  df-2nd 3088  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-r 4038  df-plus 4039  df-mul 4040  df-lt 4041  df-sub 4133  df-neg 4135  df-div 4216  df-le 4277  df-n 4423  df-2 4462  df-3 4463  df-4 4464  df-n0 4535  df-z 4564  df-seq 4661  df-exp 4676

metamath.org