Theorem pilem3 8592

Description: Lemma for pire 8596, pigt2lt4 8594 and sinpi 8595.

Hypotheses

Ref	Expression
pilem1.1	|- S = {x e. (-u4[,)0) | (sin` x) = 0}
pilem1.2	|- C = sup(S, RR, < )
pilem3.3	|- T = {x e. RR | (x < 0 /\ (sin` x) = 0)}
pilem3.4	|- P = {x e. RR | (0 < x /\ (sin` x) = 0)}

Assertion

Ref	Expression
pilem3	|- (pi e. RR+ /\ pi e. (2(,)4) /\ (sin` pi) = 0)

Distinct variable groups:   x,C   x,P

Proof of Theorem pilem3

Step	Hyp	Ref	Expression
1		pilem3.4	. . . . . . 7 |- P = {x e. RR | (0 < x /\ (sin` x) = 0)}
2		ssrab2 2121	. . . . . . 7 |- {x e. RR | (0 < x /\ (sin` x) = 0)} (_ RR
3	1, 2	eqsstr 2081	. . . . . 6 |- P (_ RR
4		pilem1.1	. . . . . . . . . . . . . 14 |- S = {x e. (-u4[,)0) | (sin` x) = 0}
5		pilem1.2	. . . . . . . . . . . . . 14 |- C = sup(S, RR, < )
6		eqid 1468	. . . . . . . . . . . . . 14 |- {x e. (-u4[,]-u2) | (sin` x) = 0} = {x e. (-u4[,]-u2) | (sin` x) = 0}
7	4, 5, 6	pilem1 8590	. . . . . . . . . . . . 13 |- (C e. (-u4(,)-u2) /\ (sin` C) = 0)
8	7	pm3.26i 320	. . . . . . . . . . . 12 |- C e. (-u4(,)-u2)
9		4re 5929	. . . . . . . . . . . . . 14 |- 4 e. RR
10	9	renegcl 5388	. . . . . . . . . . . . 13 |- -u4 e. RR
11		2re 5926	. . . . . . . . . . . . . 14 |- 2 e. RR
12	11	renegcl 5388	. . . . . . . . . . . . 13 |- -u2 e. RR
13		elioo2t 6316	. . . . . . . . . . . . . 14 |- ((-u4 e. RR* /\ -u2 e. RR*) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
14		rexrt 5471	. . . . . . . . . . . . . 14 |- (-u4 e. RR -> -u4 e. RR*)
15		rexrt 5471	. . . . . . . . . . . . . 14 |- (-u2 e. RR -> -u2 e. RR*)
16	13, 14, 15	syl2an 454	. . . . . . . . . . . . 13 |- ((-u4 e. RR /\ -u2 e. RR) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
17	10, 12, 16	mp2an 695	. . . . . . . . . . . 12 |- (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2))
18	8, 17	mpbi 189	. . . . . . . . . . 11 |- (C e. RR /\ -u4 < C /\ C < -u2)
19	18	3simp3i 791	. . . . . . . . . 10 |- C < -u2
20		2pos 5936	. . . . . . . . . . 11 |- 0 < 2
21		lt0neg2t 5642	. . . . . . . . . . . 12 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
22	11, 21	ax-mp 7	. . . . . . . . . . 11 |- (0 < 2 <-> -u2 < 0)
23	20, 22	mpbi 189	. . . . . . . . . 10 |- -u2 < 0
24	18	3simp1i 789	. . . . . . . . . . 11 |- C e. RR
25		0re 5412	. . . . . . . . . . 11 |- 0 e. RR
26	24, 12, 25	lttr 5559	. . . . . . . . . 10 |- ((C < -u2 /\ -u2 < 0) -> C < 0)
27	19, 23, 26	mp2an 695	. . . . . . . . 9 |- C < 0
28		lt0neg1t 5641	. . . . . . . . . 10 |- (C e. RR -> (C < 0 <-> 0 < -uC))
29	24, 28	ax-mp 7	. . . . . . . . 9 |- (C < 0 <-> 0 < -uC)
30	27, 29	mpbi 189	. . . . . . . 8 |- 0 < -uC
31	24	recn 5286	. . . . . . . . . 10 |- C e. CC
32		sinnegt 7384	. . . . . . . . . 10 |- (C e. CC -> (sin` -uC) = -u(sin` C))
33	31, 32	ax-mp 7	. . . . . . . . 9 |- (sin` -uC) = -u(sin` C)
34	7	pm3.27i 324	. . . . . . . . . 10 |- (sin` C) = 0
35	34	negeqi 5332	. . . . . . . . 9 |- -u(sin` C) = -u0
36		neg0 5387	. . . . . . . . 9 |- -u0 = 0
37	33, 35, 36	3eqtr 1491	. . . . . . . 8 |- (sin` -uC) = 0
38	24	renegcl 5388	. . . . . . . . 9 |- -uC e. RR
39		breq2 2613	. . . . . . . . . . . 12 |- (x = -uC -> (0 < x <-> 0 < -uC))
40		fveq2 3709	. . . . . . . . . . . . 13 |- (x = -uC -> (sin` x) = (sin` -uC))
41	40	eqeq1d 1475	. . . . . . . . . . . 12 |- (x = -uC -> ((sin` x) = 0 <-> (sin` -uC) = 0))
42	39, 41	anbi12d 626	. . . . . . . . . . 11 |- (x = -uC -> ((0 < x /\ (sin` x) = 0) <-> (0 < -uC /\ (sin` -uC) = 0)))
43	42, 1	elrab2 1898	. . . . . . . . . 10 |- (-uC e. P <-> (-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)))
44	43	biimpr 152	. . . . . . . . 9 |- ((-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)) -> -uC e. P)
45	38, 44	mpan 693	. . . . . . . 8 |- ((0 < -uC /\ (sin` -uC) = 0) -> -uC e. P)
46	30, 37, 45	mp2an 695	. . . . . . 7 |- -uC e. P
47		ne0i 2276	. . . . . . 7 |- (-uC e. P -> P =/= (/))
48	46, 47	ax-mp 7	. . . . . 6 |- P =/= (/)
49		ltlet 5493	. . . . . . . . . 10 |- ((0 e. RR /\ w e. RR) -> (0 < w -> 0 <_ w))
50	25, 49	mpan 693	. . . . . . . . 9 |- (w e. RR -> (0 < w -> 0 <_ w))
51		breq2 2613	. . . . . . . . . . . 12 |- (x = w -> (0 < x <-> 0 < w))
52		fveq2 3709	. . . . . . . . . . . . 13 |- (x = w -> (sin` x) = (sin` w))
53	52	eqeq1d 1475	. . . . . . . . . . . 12 |- (x = w -> ((sin` x) = 0 <-> (sin` w) = 0))
54	51, 53	anbi12d 626	. . . . . . . . . . 11 |- (x = w -> ((0 < x /\ (sin` x) = 0) <-> (0 < w /\ (sin` w) = 0)))
55	54, 1	elrab2 1898	. . . . . . . . . 10 |- (w e. P <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
56	55	pm3.26bi 322	. . . . . . . . 9 |- (w e. P -> w e. RR)
57		3anass 777	. . . . . . . . . . . 12 |- ((w e. RR /\ 0 < w /\ (sin` w) = 0) <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
58	55, 57	bitr4 176	. . . . . . . . . . 11 |- (w e. P <-> (w e. RR /\ 0 < w /\ (sin` w) = 0))
59	58	biimp 151	. . . . . . . . . 10 |- (w e. P -> (w e. RR /\ 0 < w /\ (sin` w) = 0))
60	59	3simp2d 793	. . . . . . . . 9 |- (w e. P -> 0 < w)
61	50, 56, 60	sylc 68	. . . . . . . 8 |- (w e. P -> 0 <_ w)
62	61	rgen 1690	. . . . . . 7 |- A.w e. P 0 <_ w
63		breq1 2612	. . . . . . . . 9 |- (z = 0 -> (z <_ w <-> 0 <_ w))
64	63	ralbidv 1655	. . . . . . . 8 |- (z = 0 -> (A.w e. P z <_ w <-> A.w e. P 0 <_ w))
65	64	rcla4ev 1868	. . . . . . 7 |- ((0 e. RR /\ A.w e. P 0 <_ w) -> E.z e. RR A.w e. P z <_ w)
66	25, 62, 65	mp2an 695	. . . . . 6 |- E.z e. RR A.w e. P z <_ w
67		infmsup 6015	. . . . . . 7 |- ((P (_ RR /\ P =/= (/) /\ E.z e. RR A.w e. P z <_ w) -> sup(P, RR, `' < ) = -usup({v e. RR | -uv e. P}, RR, < ))
68		df-pi 7244	. . . . . . . 8 |- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
69		supeq1 4549	. . . . . . . . 9 |- (P = {x e. RR | (0 < x /\ (sin` x) = 0)} -> sup(P, RR, `' < ) = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < ))
70	1, 69	ax-mp 7	. . . . . . . 8 |- sup(P, RR, `' < ) = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
71	68, 70	eqtr4 1490	. . . . . . 7 |- pi = sup(P, RR, `' < )
72	67, 71	syl5eq 1511	. . . . . 6 |- ((P (_ RR /\ P =/= (/) /\ E.z e. RR A.w e. P z <_ w) -> pi = -usup({v e. RR | -uv e. P}, RR, < ))
73	3, 48, 66, 72	mp3an 913	. . . . 5 |- pi = -usup({v e. RR | -uv e. P}, RR, < )
74		pilem3.3	. . . . . . . 8 |- T = {x e. RR | (x < 0 /\ (sin` x) = 0)}
75	4, 5, 74	pilem2 8591	. . . . . . 7 |- C = sup(T, RR, < )
76		breq1 2612	. . . . . . . . . . 11 |- (x = v -> (x < 0 <-> v < 0))
77		fveq2 3709	. . . . . . . . . . . 12 |- (x = v -> (sin` x) = (sin` v))
78	77	eqeq1d 1475	. . . . . . . . . . 11 |- (x = v -> ((sin` x) = 0 <-> (sin` v) = 0))
79	76, 78	anbi12d 626	. . . . . . . . . 10 |- (x = v -> ((x < 0 /\ (sin` x) = 0) <-> (v < 0 /\ (sin` v) = 0)))
80	79	cbvrabv 1902	. . . . . . . . 9 |- {x e. RR | (x < 0 /\ (sin` x) = 0)} = {v e. RR | (v < 0 /\ (sin` v) = 0)}
81		lt0neg1t 5641	. . . . . . . . . . . . 13 |- (v e. RR -> (v < 0 <-> 0 < -uv))
82		resinclt 7380	. . . . . . . . . . . . . . . 16 |- (v e. RR -> (sin` v) e. RR)
83	82	recnd 5287	. . . . . . . . . . . . . . 15 |- (v e. RR -> (sin` v) e. CC)
84		negeq0t 5762	. . . . . . . . . . . . . . 15 |- ((sin` v) e. CC -> ((sin` v) = 0 <-> -u(sin` v) = 0))
85	83, 84	syl 10	. . . . . . . . . . . . . 14 |- (v e. RR -> ((sin` v) = 0 <-> -u(sin` v) = 0))
86		recnt 5285	. . . . . . . . . . . . . . . 16 |- (v e. RR -> v e. CC)
87		sinnegt 7384	. . . . . . . . . . . . . . . 16 |- (v e. CC -> (sin` -uv) = -u(sin` v))
88	86, 87	syl 10	. . . . . . . . . . . . . . 15 |- (v e. RR -> (sin` -uv) = -u(sin` v))
89	88	eqeq1d 1475	. . . . . . . . . . . . . 14 |- (v e. RR -> ((sin` -uv) = 0 <-> -u(sin` v) = 0))
90	85, 89	bitr4d 529	. . . . . . . . . . . . 13 |- (v e. RR -> ((sin` v) = 0 <-> (sin` -uv) = 0))
91	81, 90	anbi12d 626	. . . . . . . . . . . 12 |- (v e. RR -> ((v < 0 /\ (sin` v) = 0) <-> (0 < -uv /\ (sin` -uv) = 0)))
92		renegclt 5409	. . . . . . . . . . . . 13 |- (v e. RR -> -uv e. RR)
93	92	biantrurd 725