Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem discrlem3 6588

Description: Lemma for discriminant theorem.

Hypotheses

Ref	Expression
discrlem.1
discrlem.2
discrlem.3
discrlem3.4
discrlem3.5

Assertion

Ref	Expression
discrlem3

---

Proof of Theorem discrlem3

Step	Hyp	Ref	Expression
1		discrlem.3	. . . . . . . . . 10
2	1	ltp1 5769	. . . . . . . . 9
3		df-ne 1579	. . . . . . . . . . 11
4		discrlem.2	. . . . . . . . . . . . 13
5	4	recn 5286	. . . . . . . . . . . 12
6	5	negne0 5763	. . . . . . . . . . 11
7	3, 6	bitr3 175	. . . . . . . . . 10
8		1re 5407	. . . . . . . . . . . . . . . . . . . 20
9	1, 8	readdcl 5306	. . . . . . . . . . . . . . . . . . 19
10	4	renegcl 5388	. . . . . . . . . . . . . . . . . . 19
11	9, 10	redivclz 5755	. . . . . . . . . . . . . . . . . 18
12		discrlem3.4	. . . . . . . . . . . . . . . . . 18
13	11, 12	syl5eqel 1544	. . . . . . . . . . . . . . . . 17
14		discrlem3.5	. . . . . . . . . . . . . . . . 17
15	13, 14	syl 10	. . . . . . . . . . . . . . . 16
16	15	adantr 389	. . . . . . . . . . . . . . 15
17		opreq1 3953	. . . . . . . . . . . . . . . . . . . 20
18	17	eqcomd 1472	. . . . . . . . . . . . . . . . . . 19
19	13	recnd 5287	. . . . . . . . . . . . . . . . . . . 20
20		sqclt 6542	. . . . . . . . . . . . . . . . . . . 20
21		mul02t 5416	. . . . . . . . . . . . . . . . . . . 20
22	19, 20, 21	3syl 20	. . . . . . . . . . . . . . . . . . 19
23	18, 22	sylan9eqr 1521	. . . . . . . . . . . . . . . . . 18
24	23	opreq1d 3960	. . . . . . . . . . . . . . . . 17
25	13, 4	jctil 292	. . . . . . . . . . . . . . . . . . . . 21
26		axmulrcl 5246	. . . . . . . . . . . . . . . . . . . . 21
27	25, 26	syl 10	. . . . . . . . . . . . . . . . . . . 20
28	27	recnd 5287	. . . . . . . . . . . . . . . . . . 19
29		addid2t 5301	. . . . . . . . . . . . . . . . . . 19
30	28, 29	syl 10	. . . . . . . . . . . . . . . . . 18
31	30	adantr 389	. . . . . . . . . . . . . . . . 17
32	24, 31	eqtrd 1499	. . . . . . . . . . . . . . . 16
33	32	opreq1d 3960	. . . . . . . . . . . . . . 15
34	16, 33	breqtrd 2629	. . . . . . . . . . . . . 14
35		0re 5412	. . . . . . . . . . . . . . . . 17
36		lesubadd2t 5604	. . . . . . . . . . . . . . . . 17
37	35, 1, 36	mp3an13 904	. . . . . . . . . . . . . . . 16
38	25, 26, 37	3syl 20	. . . . . . . . . . . . . . 15
39	38	adantr 389	. . . . . . . . . . . . . 14
40	34, 39	mpbird 196	. . . . . . . . . . . . 13
41		recnt 5285	. . . . . . . . . . . . . . . . . . . 20
42		recnt 5285	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	anim12i 333	. . . . . . . . . . . . . . . . . . 19
44		mulneg1t 5423	. . . . . . . . . . . . . . . . . . 19
45	25, 43, 44	3syl 20	. . . . . . . . . . . . . . . . . 18
46	45	eqcomd 1472	. . . . . . . . . . . . . . . . 17
47		df-neg 5330	. . . . . . . . . . . . . . . . 17
48	12	opreq2i 3957	. . . . . . . . . . . . . . . . 17
49	46, 47, 48	3eqtr3g 1522	. . . . . . . . . . . . . . . 16
50	5	negcl 5341	. . . . . . . . . . . . . . . . 17
51	9	recn 5286	. . . . . . . . . . . . . . . . 17
52	50, 51	divcan2z 5688	. . . . . . . . . . . . . . . 16
53	49, 52	eqtrd 1499	. . . . . . . . . . . . . . 15
54	53	breq1d 2619	. . . . . . . . . . . . . 14
55	54	adantr 389	. . . . . . . . . . . . 13
56	40, 55	mpbid 195	. . . . . . . . . . . 12
57	9, 1	lenlt 5551	. . . . . . . . . . . 12
58	56, 57	sylib 198	. . . . . . . . . . 11
59	58	ex 373	. . . . . . . . . 10
60	7, 59	sylbi 199	. . . . . . . . 9
61	2, 60	mt2i 110	. . . . . . . 8
62	61	a3i 74	. . . . . . 7
63	62	opreq1d 3960	. . . . . 6
64	5	mul02 5404	. . . . . 6
65	63, 64	syl6eq 1515	. . . . 5
66	5	sqval 6544	. . . . 5
67	65, 66	syl5eq 1511	. . . 4
68		opreq1 3953	. . . . . . 7
69	1	recn 5286	. . . . . . . 8
70	69	mul02 5404	. . . . . . 7
71	68, 70	syl5reqr 1514	. . . . . 6
72	71	opreq2d 3961	. . . . 5
73		4re 5929	. . . . . . 7
74	73	recn 5286	. . . . . 6
75	74	mul01 5403	. . . . 5
76	72, 75	syl6eq 1515	. . . 4
77	67, 76	opreq12d 3963	. . 3
78		0cn 5300	. . . 4
79	78	subid 5363	. . 3
80	77, 79	syl6eq 1515	. 2
81	4	resqcl 6554	. . . 4
82		discrlem.1	. . . . . 6
83	82, 1	remulcl 5307	. . . . 5
84	73, 83	remulcl 5307	. . . 4
85	81, 84	resubcl 5411	. . 3
86	85, 35	eqle 5555	. 2
87	80, 86	syl 10	1

Colors of variables: wff set class

Syntax hints:   wn 2   wi 3   wb 146   wa 223   wceq 953   wcel 955   wne 1577   class class class wbr 2609  (class class class)co 3948  cc 5204  cr 5205  cc0 5206  c1 5207   caddc 5209   cmul 5211   cmin 5264  cneg 5265   cdiv 5266   cle 5267   clt 5458  c2 5908  c4 5910  cexp 6500

This theorem is referenced by:  discrlem 6589

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924