Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem efifolem6 8642

Description: Lemma for efifo 8644.

Assertion

Ref	Expression
efifolem6	[,)

Distinct variable groups:   ,   ,

---

Proof of Theorem efifolem6

Step	Hyp	Ref	Expression
1		sq0i 6567	. . . . . . . . . . 11
2	1	opreq2d 3961	. . . . . . . . . 10
3		recnt 5285	. . . . . . . . . . 11
4		sqclt 6542	. . . . . . . . . . 11
5		ax0id 5253	. . . . . . . . . . 11
6	3, 4, 5	3syl 20	. . . . . . . . . 10
7	2, 6	sylan9eqr 1521	. . . . . . . . 9
8	7	eqeq1d 1475	. . . . . . . 8
9		ax1cn 5241	. . . . . . . . . . . 12
10		sqeqort 6580	. . . . . . . . . . . 12
11	9, 10	mpan2 694	. . . . . . . . . . 11
12	3, 11	syl 10	. . . . . . . . . 10
13		sq1 6568	. . . . . . . . . . 11
14	13	eqeq2i 1477	. . . . . . . . . 10
15	12, 14	syl5bbr 532	. . . . . . . . 9
16	15	adantr 389	. . . . . . . 8
17	8, 16	bitrd 526	. . . . . . 7
18	17	ex 373	. . . . . 6
19	18	pm5.32rd 646	. . . . 5
20		0re 5412	. . . . . . . . 9
21	20	leid 5584	. . . . . . . . 9
22		2re 5926	. . . . . . . . . 10
23		pire 8596	. . . . . . . . . 10
24		2pos 5936	. . . . . . . . . 10
25		pipos 8597	. . . . . . . . . 10
26	22, 23, 24, 25	mulgt0i 5582	. . . . . . . . 9
27	22, 23	remulcl 5307	. . . . . . . . . . 11
28		elico2t 6323	. . . . . . . . . . 11 [,)
29	20, 27, 28	mp2an 695	. . . . . . . . . 10 [,)
30	29	biimpr 152	. . . . . . . . 9 [,)
31	20, 21, 26, 30	mp3an 913	. . . . . . . 8 [,)
32		fveq2 3709	. . . . . . . . . . 11
33	32	eqeq2d 1478	. . . . . . . . . 10
34		fveq2 3709	. . . . . . . . . . 11
35	34	eqeq2d 1478	. . . . . . . . . 10
36	33, 35	anbi12d 626	. . . . . . . . 9
37	36	rcla4ev 1868	. . . . . . . 8 [,) [,)
38	31, 37	mpan 693	. . . . . . 7 [,)
39		cos0 7388	. . . . . . . . 9
40		eqeq2 1476	. . . . . . . . 9
41	39, 40	mpbiri 194	. . . . . . . 8
42	41	eqcomd 1472	. . . . . . 7
43		sin0 7386	. . . . . . . . 9
44		eqeq2 1476	. . . . . . . . 9
45	43, 44	mpbiri 194	. . . . . . . 8
46	45	eqcomd 1472	. . . . . . 7
47	38, 42, 46	syl2an 454	. . . . . 6 [,)
48	20, 23, 25	ltlei 5554	. . . . . . . . 9
49	23	recn 5286	. . . . . . . . . . 11
50	49	mulid2 5305	. . . . . . . . . 10
51		1lt2 5975	. . . . . . . . . . 11
52		1re 5407	. . . . . . . . . . . 12
53	52, 22, 23, 25	ltmul1i 5777	. . . . . . . . . . 11
54	51, 53	mpbi 189	. . . . . . . . . 10
55	50, 54	eqbrtrr 2626	. . . . . . . . 9
56		elico2t 6323	. . . . . . . . . . 11 [,)
57	20, 27, 56	mp2an 695	. . . . . . . . . 10 [,)
58	57	biimpr 152	. . . . . . . . 9 [,)
59	23, 48, 55, 58	mp3an 913	. . . . . . . 8 [,)
60		fveq2 3709	. . . . . . . . . . 11
61	60	eqeq2d 1478	. . . . . . . . . 10
62		fveq2 3709	. . . . . . . . . . 11
63	62	eqeq2d 1478	. . . . . . . . . 10
64	61, 63	anbi12d 626	. . . . . . . . 9
65	64	rcla4ev 1868	. . . . . . . 8 [,) [,)
66	59, 65	mpan 693	. . . . . . 7 [,)
67		cospi 8601	. . . . . . . . 9
68		eqeq2 1476	. . . . . . . . 9
69	67, 68	mpbiri 194	. . . . . . . 8
70	69	eqcomd 1472	. . . . . . 7
71		sinpi 8595	. . . . . . . . 9
72		eqeq2 1476	. . . . . . . . 9
73	71, 72	mpbiri 194	. . . . . . . 8
74	73	eqcomd 1472	. . . . . . 7
75	66, 70, 74	syl2an 454	. . . . . 6 [,)
76	47, 75	jaoian 425	. . . . 5 [,)
77	19, 76	syl6bi 214	. . . 4 [,)
78	77	3impib 829	. . 3 [,)
79	78	3expia 833	. 2 [,)