Theorem discrlem3 6658

Description: Lemma for discriminant theorem.

Hypotheses

Ref	Expression
discrlem.1	|- A e. RR
discrlem.2	|- B e. RR
discrlem.3	|- C e. RR
discrlem3.4	|- D = ((C + 1) / -uB)
discrlem3.5	|- (D e. RR -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))

Assertion

Ref	Expression
discrlem3	|- (0 = A -> ((B^2) - (4 x. (A x. C))) <_ 0)

Proof of Theorem discrlem3

Step	Hyp	Ref	Expression
1		discrlem.3	. . . . . . . . . 10 |- C e. RR
2	1	ltp1 5813	. . . . . . . . 9 |- C < (C + 1)
3		df-ne 1587	. . . . . . . . . . 11 |- (B =/= 0 <-> -. B = 0)
4		discrlem.2	. . . . . . . . . . . . 13 |- B e. RR
5	4	recn 5314	. . . . . . . . . . . 12 |- B e. CC
6	5	negne0 5807	. . . . . . . . . . 11 |- (B =/= 0 <-> -uB =/= 0)
7	3, 6	bitr3 175	. . . . . . . . . 10 |- (-. B = 0 <-> -uB =/= 0)
8		1re 5435	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR
9	1, 8	readdcl 5334	. . . . . . . . . . . . . . . . . . 19 |- (C + 1) e. RR
10	4	renegcl 5416	. . . . . . . . . . . . . . . . . . 19 |- -uB e. RR
11	9, 10	redivclz 5799	. . . . . . . . . . . . . . . . . 18 |- (-uB =/= 0 -> ((C + 1) / -uB) e. RR)
12		discrlem3.4	. . . . . . . . . . . . . . . . . 18 |- D = ((C + 1) / -uB)
13	11, 12	syl5eqel 1552	. . . . . . . . . . . . . . . . 17 |- (-uB =/= 0 -> D e. RR)
14		discrlem3.5	. . . . . . . . . . . . . . . . 17 |- (D e. RR -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))
15	13, 14	syl 10	. . . . . . . . . . . . . . . 16 |- (-uB =/= 0 -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))
16	15	adantr 389	. . . . . . . . . . . . . . 15 |- ((-uB =/= 0 /\ 0 = A) -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))
17		opreq1 3968	. . . . . . . . . . . . . . . . . . . 20 |- (0 = A -> (0 x. (D^2)) = (A x. (D^2)))
18	17	eqcomd 1480	. . . . . . . . . . . . . . . . . . 19 |- (0 = A -> (A x. (D^2)) = (0 x. (D^2)))
19	13	recnd 5315	. . . . . . . . . . . . . . . . . . . 20 |- (-uB =/= 0 -> D e. CC)
20		sqclt 6611	. . . . . . . . . . . . . . . . . . . 20 |- (D e. CC -> (D^2) e. CC)
21		mul02t 5444	. . . . . . . . . . . . . . . . . . . 20 |- ((D^2) e. CC -> (0 x. (D^2)) = 0)
22	19, 20, 21	3syl 20	. . . . . . . . . . . . . . . . . . 19 |- (-uB =/= 0 -> (0 x. (D^2)) = 0)
23	18, 22	sylan9eqr 1529	. . . . . . . . . . . . . . . . . 18 |- ((-uB =/= 0 /\ 0 = A) -> (A x. (D^2)) = 0)
24	23	opreq1d 3975	. . . . . . . . . . . . . . . . 17 |- ((-uB =/= 0 /\ 0 = A) -> ((A x. (D^2)) + (B x. D)) = (0 + (B x. D)))
25	13, 4	jctil 292	. . . . . . . . . . . . . . . . . . . . 21 |- (-uB =/= 0 -> (B e. RR /\ D e. RR))
26		axmulrcl 5274	. . . . . . . . . . . . . . . . . . . . 21 |- ((B e. RR /\ D e. RR) -> (B x. D) e. RR)
27	25, 26	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (-uB =/= 0 -> (B x. D) e. RR)
28	27	recnd 5315	. . . . . . . . . . . . . . . . . . 19 |- (-uB =/= 0 -> (B x. D) e. CC)
29		addid2t 5329	. . . . . . . . . . . . . . . . . . 19 |- ((B x. D) e. CC -> (0 + (B x. D)) = (B x. D))
30	28, 29	syl 10	. . . . . . . . . . . . . . . . . 18 |- (-uB =/= 0 -> (0 + (B x. D)) = (B x. D))
31	30	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((-uB =/= 0 /\ 0 = A) -> (0 + (B x. D)) = (B x. D))
32	24, 31	eqtrd 1507	. . . . . . . . . . . . . . . 16 |- ((-uB =/= 0 /\ 0 = A) -> ((A x. (D^2)) + (B x. D)) = (B x. D))
33	32	opreq1d 3975	. . . . . . . . . . . . . . 15 |- ((-uB =/= 0 /\ 0 = A) -> (((A x. (D^2)) + (B x. D)) + C) = ((B x. D) + C))
34	16, 33	breqtrd 2639	. . . . . . . . . . . . . 14 |- ((-uB =/= 0 /\ 0 = A) -> 0 <_ ((B x. D) + C))
35		0re 5440	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
36		lesubadd2t 5630	. . . . . . . . . . . . . . . . 17 |- ((0 e. RR /\ (B x. D) e. RR /\ C e. RR) -> ((0 - (B x. D)) <_ C <-> 0 <_ ((B x. D) + C)))
37	35, 1, 36	mp3an13 907	. . . . . . . . . . . . . . . 16 |- ((B x. D) e. RR -> ((0 - (B x. D)) <_ C <-> 0 <_ ((B x. D) + C)))
38	25, 26, 37	3syl 20	. . . . . . . . . . . . . . 15 |- (-uB =/= 0 -> ((0 - (B x. D)) <_ C <-> 0 <_ ((B x. D) + C)))
39	38	adantr 389	. . . . . . . . . . . . . 14 |- ((-uB =/= 0 /\ 0 = A) -> ((0 - (B x. D)) <_ C <-> 0 <_ ((B x. D) + C)))
40	34, 39	mpbird 196	. . . . . . . . . . . . 13 |- ((-uB =/= 0 /\ 0 = A) -> (0 - (B x. D)) <_ C)
41		recnt 5313	. . . . . . . . . . . . . . . . . . . 20 |- (B e. RR -> B e. CC)
42		recnt 5313	. . . . . . . . . . . . . . . . . . . 20 |- (D e. RR -> D e. CC)
43	41, 42	anim12i 333	. . . . . . . . . . . . . . . . . . 19 |- ((B e. RR /\ D e. RR) -> (B e. CC /\ D e. CC))
44		mulneg1t 5451	. . . . . . . . . . . . . . . . . . 19 |- ((B e. CC /\ D e. CC) -> (-uB x. D) = -u(B x. D))
45	25, 43, 44	3syl 20	. . . . . . . . . . . . . . . . . 18 |- (-uB =/= 0 -> (-uB x. D) = -u(B x. D))
46	45	eqcomd 1480	. . . . . . . . . . . . . . . . 17 |- (-uB =/= 0 -> -u(B x. D) = (-uB x. D))
47		df-neg 5358	. . . . . . . . . . . . . . . . 17 |- -u(B x. D) = (0 - (B x. D))
48	12	opreq2i 3972	. . . . . . . . . . . . . . . . 17 |- (-uB x. D) = (-uB x. ((C + 1) / -uB))
49	46, 47, 48	3eqtr3g 1530	. . . . . . . . . . . . . . . 16 |- (-uB =/= 0 -> (0 - (B x. D)) = (-uB x. ((C + 1) / -uB)))
50	9	recn 5314	. . . . . . . . . . . . . . . . 17 |- (C + 1) e. CC
51	5	negcl 5369	. . . . . . . . . . . . . . . . 17 |- -uB e. CC
52	50, 51	divcan2z 5719	. . . . . . . . . . . . . . . 16 |- (-uB =/= 0 -> (-uB x. ((C + 1) / -uB)) = (C + 1))
53	49, 52	eqtrd 1507	. . . . . . . . . . . . . . 15 |- (-uB =/= 0 -> (0 - (B x. D)) = (C + 1))
54	53	breq1d 2629	. . . . . . . . . . . . . 14 |- (-uB =/= 0 -> ((0 - (B x. D)) <_ C <-> (C + 1) <_ C))
55	54	adantr 389	. . . . . . . . . . . . 13 |- ((-uB =/= 0 /\ 0 = A) -> ((0 - (B x. D)) <_ C <-> (C + 1) <_ C))
56	40, 55	mpbid 195	. . . . . . . . . . . 12 |- ((-uB =/= 0 /\ 0 = A) -> (C + 1) <_ C)
57	9, 1	lenlt 5578	. . . . . . . . . . . 12 |- ((C + 1) <_ C <-> -. C < (C + 1))
58	56, 57	sylib 198	. . . . . . . . . . 11 |- ((-uB =/= 0 /\ 0 = A) -> -. C < (C + 1))
59	58	ex 373	. . . . . . . . . 10 |- (-uB =/= 0 -> (0 = A -> -. C < (C + 1)))
60	7, 59	sylbi 199	. . . . . . . . 9 |- (-. B = 0 -> (0 = A -> -. C < (C + 1)))
61	2, 60	mt2i 110	. . . . . . . 8 |- (-. B = 0 -> -. 0 = A)
62	61	a3i 74	. . . . . . 7 |- (0 = A -> B = 0)
63	62	opreq1d 3975	. . . . . 6 |- (0 = A -> (B x. B) = (0 x. B))
64	5	mul02 5432	. . . . . 6 |- (0 x. B) = 0
65	63, 64	syl6eq 1523	. . . . 5 |- (0 = A -> (B x. B) = 0)
66	5	sqval 6614	. . . . 5 |- (B^2) = (B x. B)
67	65, 66	syl5eq 1519	. . . 4 |- (0 = A -> (B^2) = 0)
68		opreq1 3968	. . . . . . 7 |- (0 = A -> (0 x. C) = (A x. C))
69	1	recn 5314	. . . . . . . 8 |- C e. CC
70	69	mul02 5432	. . . . . . 7 |- (0 x. C) = 0
71	68, 70	syl5reqr 1522	. . . . . 6 |- (0 = A -> (A x. C) = 0)
72	71	opreq2d 3976	. . . . 5 |- (0 = A -> (4 x. (A x. C)) = (4 x. 0))
73		4re 5982	. . . . . . 7 |- 4 e. RR
74	73	recn 5314	. . . . . 6 |- 4 e. CC
75	74	mul01 5431	. . . . 5 |- (4 x. 0) = 0
76	72, 75	syl6eq 1523	. . . 4 |- (0 = A -> (4 x. (A x. C)) = 0)
77	67, 76	opreq12d 3978	. . 3 |- (0 = A -> ((B^2) - (4 x. (A x. C))) = (0 - 0))
78		0cn 5328	. . . 4 |- 0 e. CC
79	78	subid 5391	. . 3 |- (0 - 0) = 0
80	77, 79	syl6eq 1523	. 2 |- (0 = A -> ((B^2) - (4 x. (A x. C))) = 0)
81	4	resqcl 6623	. . . 4 |- (B^2) e. RR
82		discrlem.1	. . . . . 6 |- A e. RR
83	82, 1	remulcl 5335	. . . . 5 |- (A x. C) e. RR
84	73, 83	remulcl 5335	. . . 4 |- (4 x. (A x. C)) e. RR
85	81, 84	resubcl 5439	. . 3 |- ((B^2) - (4 x. (A x. C))) e. RR
86	85, 35	eqle 5582	. 2 |- (((B^2) - (4 x. (A x. C))) = 0 -> ((B^2) - (4 x. (A x. C))) <_ 0)
87	80, 86	syl 10	1 |- (0 = A -> ((B^2) - (4 x. (A x. C))) <_ 0)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958   =/= wne 1585   class class class wbr 2619  (class class class)co 3963  CCcc 5232  RRcr 5233  0cc0 5234  1c1 5235   + caddc 5237   x. cmul 5239   - cmin 5292  -ucneg 5293   / cdiv 5294   <_ cle 5295   < clt 5486  2c2 5961  4c4 5963  ^cexp 6568

This theorem is referenced by:  discrlem 6659

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-nel 1588  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-pss 2055  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-iun 2568  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we