Theorem pilem3 8756

Description: Lemma for pire 8760, pigt2lt4 8758 and sinpi 8759.

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 2182	. . . . . . 7 |- {x e. RR | (0 < x /\ (sin` x) = 0)} (_ RR
3	1, 2	eqsstri 2142	. . . . . 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 1522	. . . . . . . . . . . . . 14 |- {x e. (-u4[,]-u2) | (sin` x) = 0} = {x e. (-u4[,]-u2) | (sin` x) = 0}
7	4, 5, 6	pilem1 8754	. . . . . . . . . . . . 13 |- (C e. (-u4(,)-u2) /\ (sin` C) = 0)
8	7	pm3.26i 327	. . . . . . . . . . . 12 |- C e. (-u4(,)-u2)
9		4re 6043	. . . . . . . . . . . . . 14 |- 4 e. RR
10	9	renegcli 5481	. . . . . . . . . . . . 13 |- -u4 e. RR
11		2re 6040	. . . . . . . . . . . . . 14 |- 2 e. RR
12	11	renegcli 5481	. . . . . . . . . . . . 13 |- -u2 e. RR
13		elioo2 6404	. . . . . . . . . . . . . 14 |- ((-u4 e. RR* /\ -u2 e. RR*) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
14		rexr 5564	. . . . . . . . . . . . . 14 |- (-u4 e. RR -> -u4 e. RR*)
15		rexr 5564	. . . . . . . . . . . . . 14 |- (-u2 e. RR -> -u2 e. RR*)
16	13, 14, 15	syl2an 465	. . . . . . . . . . . . 13 |- ((-u4 e. RR /\ -u2 e. RR) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
17	10, 12, 16	mp2an 709	. . . . . . . . . . . 12 |- (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2))
18	8, 17	mpbi 196	. . . . . . . . . . 11 |- (C e. RR /\ -u4 < C /\ C < -u2)
19	18	3simp3i 805	. . . . . . . . . 10 |- C < -u2
20		2pos 6050	. . . . . . . . . . 11 |- 0 < 2
21		lt0neg2 5734	. . . . . . . . . . . 12 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
22	11, 21	ax-mp 7	. . . . . . . . . . 11 |- (0 < 2 <-> -u2 < 0)
23	20, 22	mpbi 196	. . . . . . . . . 10 |- -u2 < 0
24	18	3simp1i 803	. . . . . . . . . . 11 |- C e. RR
25		0re 5505	. . . . . . . . . . 11 |- 0 e. RR
26	24, 12, 25	lttri 5650	. . . . . . . . . 10 |- ((C < -u2 /\ -u2 < 0) -> C < 0)
27	19, 23, 26	mp2an 709	. . . . . . . . 9 |- C < 0
28		lt0neg1 5733	. . . . . . . . . 10 |- (C e. RR -> (C < 0 <-> 0 < -uC))
29	24, 28	ax-mp 7	. . . . . . . . 9 |- (C < 0 <-> 0 < -uC)
30	27, 29	mpbi 196	. . . . . . . 8 |- 0 < -uC
31	24	recni 5379	. . . . . . . . . 10 |- C e. CC
32		sinneg 7533	. . . . . . . . . 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 331	. . . . . . . . . 10 |- (sin` C) = 0
35	34	negeqi 5425	. . . . . . . . 9 |- -u(sin` C) = -u0
36		neg0 5480	. . . . . . . . 9 |- -u0 = 0
37	33, 35, 36	3eqtri 1546	. . . . . . . 8 |- (sin` -uC) = 0
38	24	renegcli 5481	. . . . . . . . 9 |- -uC e. RR
39		breq2 2678	. . . . . . . . . . . 12 |- (x = -uC -> (0 < x <-> 0 < -uC))
40		fveq2 3781	. . . . . . . . . . . . 13 |- (x = -uC -> (sin` x) = (sin` -uC))
41	40	eqeq1d 1530	. . . . . . . . . . . 12 |- (x = -uC -> ((sin` x) = 0 <-> (sin` -uC) = 0))
42	39, 41	anbi12d 639	. . . . . . . . . . 11 |- (x = -uC -> ((0 < x /\ (sin` x) = 0) <-> (0 < -uC /\ (sin` -uC) = 0)))
43	42, 1	elrab2 1954	. . . . . . . . . 10 |- (-uC e. P <-> (-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)))
44	43	biimpri 159	. . . . . . . . 9 |- ((-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)) -> -uC e. P)
45	38, 44	mpan 707	. . . . . . . 8 |- ((0 < -uC /\ (sin` -uC) = 0) -> -uC e. P)
46	30, 37, 45	mp2an 709	. . . . . . 7 |- -uC e. P
47		ne0i 2337	. . . . . . 7 |- (-uC e. P -> P =/= (/))
48	46, 47	ax-mp 7	. . . . . 6 |- P =/= (/)
49		ltle 5585	. . . . . . . . . 10 |- ((0 e. RR /\ w e. RR) -> (0 < w -> 0 <_ w))
50	25, 49	mpan 707	. . . . . . . . 9 |- (w e. RR -> (0 < w -> 0 <_ w))
51		breq2 2678	. . . . . . . . . . . 12 |- (x = w -> (0 < x <-> 0 < w))
52		fveq2 3781	. . . . . . . . . . . . 13 |- (x = w -> (sin` x) = (sin` w))
53	52	eqeq1d 1530	. . . . . . . . . . . 12 |- (x = w -> ((sin` x) = 0 <-> (sin` w) = 0))
54	51, 53	anbi12d 639	. . . . . . . . . . 11 |- (x = w -> ((0 < x /\ (sin` x) = 0) <-> (0 < w /\ (sin` w) = 0)))
55	54, 1	elrab2 1954	. . . . . . . . . 10 |- (w e. P <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
56	55	pm3.26bi 329	. . . . . . . . 9 |- (w e. P -> w e. RR)
57		3anass 791	. . . . . . . . . . . 12 |- ((w e. RR /\ 0 < w /\ (sin` w) = 0) <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
58	55, 57	bitr4i 183	. . . . . . . . . . 11 |- (w e. P <-> (w e. RR /\ 0 < w /\ (sin` w) = 0))
59	58	biimpi 158	. . . . . . . . . 10 |- (w e. P -> (w e. RR /\ 0 < w /\ (sin` w) = 0))
60	59	3simp2d 807	. . . . . . . . 9 |- (w e. P -> 0 < w)
61	50, 56, 60	sylc 71	. . . . . . . 8 |- (w e. P -> 0 <_ w)
62	61	rgen 1745	. . . . . . 7 |- A.w e. P 0 <_ w
63		breq1 2677	. . . . . . . . 9 |- (z = 0 -> (z <_ w <-> 0 <_ w))
64	63	ralbidv 1710	. . . . . . . 8 |- (z = 0 -> (A.w e. P z <_ w <-> A.w e. P 0 <_ w))
65	64	rcla4ev 1924	. . . . . . 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 709	. . . . . 6 |- E.z e. RR A.w e. P z <_ w
67		infmsup 6150	. . . . . . 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 7392	. . . . . . . 8 |- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
69		supeq1 4635	. . . . . . . . 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	eqtr4i 1545	. . . . . . 7 |- pi = sup(P, RR, `' < )
72	67, 71	syl5eq 1566	. . . . . 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 928	. . . . 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 8755	. . . . . . 7 |- C = sup(T, RR, < )
76		breq1 2677	. . . . . . . . . . 11 |- (x = v -> (x < 0 <-> v < 0))
77		fveq2 3781	. . . . . . . . . . . 12 |- (x = v -> (sin` x) = (sin` v))
78	77	eqeq1d 1530	. . . . . . . . . . 11 |- (x = v -> ((sin` x) = 0 <-> (sin` v) = 0))
79	76, 78	anbi12d 639	. . . . . . . . . 10 |- (x = v -> ((x < 0 /\ (sin` x) = 0) <-> (v < 0 /\ (sin` v) = 0)))
80	79	cbvrabv 1958	. . . . . . . . 9 |- {x e. RR | (x < 0 /\ (sin` x) = 0)} = {v e. RR | (v < 0 /\ (sin` v) = 0)}
81		lt0neg1 5733	. . . . . . . . . . . . 13 |- (v e. RR -> (v < 0 <-> 0 < -uv))
82		resincl 7529	. . . . . . . . . . . . . . . 16 |- (v e. RR -> (sin` v) e. RR)
83	82	recndi 5380	. . . . . . . . . . . . . . 15 |- (v e. RR -> (sin` v) e. CC)
84		negeq0 5864	. . . . . . . . . . . . . . 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		recn 5378	. . . . . . . . . . . . . . . 16 |- (v e. RR -> v e. CC)
87		sinneg 7533	. . . . . . . . . . . . . . . 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 1530	. . . . . . . . . . . . . 14 |- (v e. RR -> ((sin` -uv) = 0 <-> -u(sin` v) = 0))
90	85, 89	bitr4d 542	. . . . . . . . . . . . 13 |- (v e. RR -> ((sin` v) = 0 <-> (sin` -uv) = 0))
91	81, 90	anbi12d 639	. . . . . . . . . . . 12 |- (v e. RR -> ((v < 0 /\ (sin` v) = 0) <-> (0 < -uv /\ (sin` -uv) = 0)))
92		renegcl 5502	. . . . . . . . . . . . 13 |- (v e. RR -> -uv e. RR)
93	92	b