Theorem discrlem3 6659

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 5815	. . . . . . . . 9 |- C < (C + 1)
3		df-ne 1590	. . . . . . . . . . 11 |- (B =/= 0 <-> -. B = 0)
4		discrlem.2	. . . . . . . . . . . . 13 |- B e. RR
5	4	recn 5326	. . . . . . . . . . . 12 |- B e. CC
6	5	negne0 5809	. . . . . . . . . . 11 |- (B =/= 0 <-> -uB =/= 0)
7	3, 6	bitr3 175	. . . . . . . . . 10 |- (-. B = 0 <-> -uB =/= 0)
8		1re 5447	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR
9	1, 8	readdcl 5346	. . . . . . . . . . . . . . . . . . 19 |- (C + 1) e. RR
10	4	renegcl 5428	. . . . . . . . . . . . . . . . . . 19 |- -uB e. RR
11	9, 10	redivclz 5801	. . . . . . . . . . . . . . . . . 18 |- (-uB =/= 0 -> ((C + 1) / -uB) e. RR)
12		discrlem3.4	. . . . . . . . . . . . . . . . . 18 |- D = ((C + 1) / -uB)
13	11, 12	syl5eqel 1555	. . . . . . . . . . . . . . . . 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 391	. . . . . . . . . . . . . . 15 |- ((-uB =/= 0 /\ 0 = A) -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))
17		opreq1 3974	. . . . . . . . . . . . . . . . . . . 20 |- (0 = A -> (0 x. (D^2)) = (A x. (D^2)))
18	17	eqcomd 1483	. . . . . . . . . . . . . . . . . . 19 |- (0 = A -> (A x. (D^2)) = (0 x. (D^2)))
19	13	recnd 5327	. . . . . . . . . . . . . . . . . . . 20 |- (-uB =/= 0 -> D e. CC)
20		sqclt 6612	. . . . . . . . . . . . . . . . . . . 20 |- (D e. CC -> (D^2) e. CC)
21		mul02t 5456	. . . . . . . . . . . . . . . . . . . 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 1532	. . . . . . . . . . . . . . . . . 18 |- ((-uB =/= 0 /\ 0 = A) -> (A x. (D^2)) = 0)
24	23	opreq1d 3981	. . . . . . . . . . . . . . . . 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 5286	. . . . . . . . . . . . . . . . . . . . 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 5327	. . . . . . . . . . . . . . . . . . 19 |- (-uB =/= 0 -> (B x. D) e. CC)
29		addid2t 5341	. . . . . . . . . . . . . . . . . . 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 391	. . . . . . . . . . . . . . . . 17 |- ((-uB =/= 0 /\ 0 = A) -> (0 + (B x. D)) = (B x. D))
32	24, 31	eqtrd 1510	. . . . . . . . . . . . . . . 16 |- ((-uB =/= 0 /\ 0 = A) -> ((A x. (D^2)) + (B x. D)) = (B x. D))
33	32	opreq1d 3981	. . . . . . . . . . . . . . 15 |- ((-uB =/= 0 /\ 0 = A) -> (((A x. (D^2)) + (B x. D)) + C) = ((B x. D) + C))
34	16, 33	breqtrd 2644	. . . . . . . . . . . . . 14 |- ((-uB =/= 0 /\ 0 = A) -> 0 <_ ((B x. D) + C))
35		0re 5452	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
36		lesubadd2t 5642	. . . . . . . . . . . . . . . . 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 909	. . . . . . . . . . . . . . . 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 391	. . . . . . . . . . . . . 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 5325	. . . . . . . . . . . . . . . . . . . 20 |- (B e. RR -> B e. CC)
42		recnt 5325	. . . . . . . . . . . . . . . . . . . 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 5463	. . . . . . . . . . . . . . . . . . 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 1483	. . . . . . . . . . . . . . . . 17 |- (-uB =/= 0 -> -u(B x. D) = (-uB x. D))
47		df-neg 5370	. . . . . . . . . . . . . . . . 17 |- -u(B x. D) = (0 - (B x. D))
48	12	opreq2i 3978	. . . . . . . . . . . . . . . . 17 |- (-uB x. D) = (-uB x. ((C + 1) / -uB))
49	46, 47, 48	3eqtr3g 1533	. . . . . . . . . . . . . . . 16 |- (-uB =/= 0 -> (0 - (B x. D)) = (-uB x. ((C + 1) / -uB)))
50	9	recn 5326	. . . . . . . . . . . . . . . . 17 |- (C + 1) e. CC
51	5	negcl 5381	. . . . . . . . . . . . . . . . 17 |- -uB e. CC
52	50, 51	divcan2z 5731	. . . . . . . . . . . . . . . 16 |- (-uB =/= 0 -> (-uB x. ((C + 1) / -uB)) = (C + 1))
53	49, 52	eqtrd 1510	. . . . . . . . . . . . . . 15 |- (-uB =/= 0 -> (0 - (B x. D)) = (C + 1))
54	53	breq1d 2634	. . . . . . . . . . . . . 14 |- (-uB =/= 0 -> ((0 - (B x. D)) <_ C <-> (C + 1) <_ C))
55	54	adantr 391	. . . . . . . . . . . . 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 5590	. . . . . . . . . . . 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 3981	. . . . . 6 |- (0 = A -> (B x. B) = (0 x. B))
64	5	mul02 5444	. . . . . 6 |- (0 x. B) = 0
65	63, 64	syl6eq 1526	. . . . 5 |- (0 = A -> (B x. B) = 0)
66	5	sqval 6615	. . . . 5 |- (B^2) = (B x. B)
67	65, 66	syl5eq 1522	. . . 4 |- (0 = A -> (B^2) = 0)
68		opreq1 3974	. . . . . . 7 |- (0 = A -> (0 x. C) = (A x. C))
69	1	recn 5326	. . . . . . . 8 |- C e. CC
70	69	mul02 5444	. . . . . . 7 |- (0 x. C) = 0
71	68, 70	syl5reqr 1525	. . . . . 6 |- (0 = A -> (A x. C) = 0)
72	71	opreq2d 3982	. . . . 5 |- (0 = A -> (4 x. (A x. C)) = (4 x. 0))
73		4re 5984	. . . . . . 7 |- 4 e. RR
74	73	recn 5326	. . . . . 6 |- 4 e. CC
75	74	mul01 5443	. . . . 5 |- (4 x. 0) = 0
76	72, 75	syl6eq 1526	. . . 4 |- (0 = A -> (4 x. (A x. C)) = 0)
77	67, 76	opreq12d 3984	. . 3 |- (0 = A -> ((B^2) - (4 x. (A x. C))) = (0 - 0))
78		0cn 5340	. . . 4 |- 0 e. CC
79	78	subid 5403	. . 3 |- (0 - 0) = 0
80	77, 79	syl6eq 1526	. 2 |- (0 = A -> ((B^2) - (4 x. (A x. C))) = 0)
81	4	resqcl 6624	. . . 4 |- (B^2) e. RR
82		discrlem.1	. . . . . 6 |- A e. RR
83	82, 1	remulcl 5347	. . . . 5 |- (A x. C) e. RR
84	73, 83	remulcl 5347	. . . 4 |- (4 x. (A x. C)) e. RR
85	81, 84	resubcl 5451	. . 3 |- ((B^2) - (4 x. (A x. C))) e. RR
86	85, 35	eqle 5594	. 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 958   e. wcel 960   =/= wne 1588   class class class wbr 2624  (class class class)co 3969  CCcc 5244  RRcr 5245  0cc0 5246  1c1 5247   + caddc 5249   x. cmul 5251   - cmin 5304  -ucneg 5305   / cdiv 5306   <_ cle 5307   < clt 5498  2c2 5963  4c4 5965  ^cexp 6569

This theorem is referenced by:  discrlem 6660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we