Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem efif1lem5 8649

Description: Lemma for efif1 8652.

Hypotheses

Ref	Expression
efif1lem5.1	[,)
efif1lem5.2	[,)

Assertion

Ref	Expression
efif1lem5

---

Proof of Theorem efif1lem5

Step	Hyp	Ref	Expression
1		efif1lem5.1	. . . 4 [,)
2		0re 5412	. . . . . . 7
3		pire 8596	. . . . . . 7
4		pipos 8597	. . . . . . 7
5		snunioo 6348	. . . . . . 7 (,) [,)
6	2, 3, 4, 5	mp3an 913	. . . . . 6 (,) [,)
7	6	eleq2i 1530	. . . . 5 (,) [,)
8		elun 2163	. . . . 5 (,) (,)
9	7, 8	bitr3 175	. . . 4 [,) (,)
10	1, 9	mpbi 189	. . 3 (,)
11		elsnc2g 2426	. . . . 5
12	2, 11	ax-mp 7	. . . 4
13	12	orbi1i 256	. . 3 (,) (,)
14	10, 13	mpbi 189	. 2 (,)
15		efif1lem5.2	. . . 4 [,)
16		2re 5926	. . . . . . . 8
17	16, 3	remulcl 5307	. . . . . . 7
18		1lt2 5975	. . . . . . . 8
19		ltmulgt12t 5803	. . . . . . . . 9
20	3, 16, 4, 19	mp3an 913	. . . . . . . 8
21	18, 20	mpbi 189	. . . . . . 7
22		snunioo 6348	. . . . . . 7 (,) [,)
23	3, 17, 21, 22	mp3an 913	. . . . . 6 (,) [,)
24	23	eleq2i 1530	. . . . 5 (,) [,)
25		elun 2163	. . . . 5 (,) (,)
26	24, 25	bitr3 175	. . . 4 [,) (,)
27	15, 26	mpbi 189	. . 3 (,)
28		elsnc2g 2426	. . . . 5
29	3, 28	ax-mp 7	. . . 4
30	29	orbi1i 256	. . 3 (,) (,)
31	27, 30	mpbi 189	. 2 (,)
32		ax1ne0 5252	. . . . . 6
33		df-ne 1579	. . . . . 6
34	32, 33	mpbi 189	. . . . 5
35		fveq2 3709	. . . . . . . 8
36		cos0 7388	. . . . . . . 8
37	35, 36	syl6eq 1515	. . . . . . 7
38		fveq2 3709	. . . . . . . 8
39		cospi 8601	. . . . . . . 8
40	38, 39	syl6eq 1515	. . . . . . 7
41	37, 40	eqeqan12d 1482	. . . . . 6
42		ax1cn 5241	. . . . . . 7
43	42	eqneg 5760	. . . . . 6
44	41, 43	syl6bb 534	. . . . 5
45	34, 44	mtbiri 715	. . . 4
46		orc 269	. . . . . 6
47		ianor 305	. . . . . 6
48	46, 47	sylibr 200	. . . . 5
49		elico2t 6323	. . . . . . . . . 10 [,)
50	2, 3, 49	mp2an 695	. . . . . . . . 9 [,)
51	1, 50	mpbi 189	. . . . . . . 8
52	51	3simp1i 789	. . . . . . 7
53		elico2t 6323	. . . . . . . . . 10 [,)
54	3, 17, 53	mp2an 695	. . . . . . . . 9 [,)
55	15, 54	mpbi 189	. . . . . . . 8
56	55	3simp1i 789	. . . . . . 7
57		efieq 7392	. . . . . . 7
58	52, 56, 57	mp2an 695	. . . . . 6
59	58	negbii 187	. . . . 5
60	48, 59	sylibr 200	. . . 4
61	45, 60	syl 10	. . 3
62		sinq12gt0t 8625	. . . . . . . 8 (,)
63		resinclt 7380	. . . . . . . . . 10
64	52, 63	ax-mp 7	. . . . . . . . 9
65	64	gt0ne0 5585	. . . . . . . 8
66	62, 65	syl 10	. . . . . . 7 (,)
67		df-ne 1579	. . . . . . 7
68	66, 67	sylib 198	. . . . . 6 (,)
69	68	adantr 389	. . . . 5 (,)
70		eqtrt 1484	. . . . . . 7
71		fveq2 3709	. . . . . . . . 9
72		sinpi 8595	. . . . . . . . 9
73	71, 72	syl6eq 1515	. . . . . . . 8
74	73	adantl 388	. . . . . . 7 (,)
75	70, 74	sylan2 451	. . . . . 6 (,)
76	75	expcom 374	. . . . 5 (,)
77	69, 76	mtod 108	. . . 4 (,)
78		olc 268	. . . . . 6
79	78, 47	sylibr 200	. . . . 5
80	79, 59	sylibr 200	. . . 4
81	77, 80	syl 10	. . 3 (,)
82		efif1lem1 8645	. . . . . . . . . 10 (,) (,)
83		sinq12gt0t 8625	. . . . . . . . . 10 (,)