Theorem pilem2 8591

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, < )
pilem2.3	|- T = {x e. RR | (x < 0 /\ (sin` x) = 0)}

Assertion

Ref	Expression
pilem2	|- C = sup(T, RR, < )

Distinct variable group:   x,C

Proof of Theorem pilem2

Step	Hyp	Ref	Expression
1		pilem1.1	. . . . . . 7 |- S = {x e. (-u4[,)0) | (sin` x) = 0}
2		pilem1.2	. . . . . . 7 |- C = sup(S, RR, < )
3		eqid 1468	. . . . . . 7 |- {x e. (-u4[,]-u2) | (sin` x) = 0} = {x e. (-u4[,]-u2) | (sin` x) = 0}
4	1, 2, 3	pilem1 8590	. . . . . 6 |- (C e. (-u4(,)-u2) /\ (sin` C) = 0)
5	4	pm3.26i 320	. . . . 5 |- C e. (-u4(,)-u2)
6		4re 5929	. . . . . . 7 |- 4 e. RR
7	6	renegcl 5388	. . . . . 6 |- -u4 e. RR
8		2re 5926	. . . . . . 7 |- 2 e. RR
9	8	renegcl 5388	. . . . . 6 |- -u2 e. RR
10		elioo2t 6316	. . . . . . 7 |- ((-u4 e. RR* /\ -u2 e. RR*) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
11		rexrt 5471	. . . . . . 7 |- (-u4 e. RR -> -u4 e. RR*)
12		rexrt 5471	. . . . . . 7 |- (-u2 e. RR -> -u2 e. RR*)
13	10, 11, 12	syl2an 454	. . . . . 6 |- ((-u4 e. RR /\ -u2 e. RR) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
14	7, 9, 13	mp2an 695	. . . . 5 |- (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2))
15	5, 14	mpbi 189	. . . 4 |- (C e. RR /\ -u4 < C /\ C < -u2)
16	15	3simp1i 789	. . 3 |- C e. RR
17		pilem2.3	. . . . . 6 |- T = {x e. RR | (x < 0 /\ (sin` x) = 0)}
18		ssrab2 2121	. . . . . 6 |- {x e. RR | (x < 0 /\ (sin` x) = 0)} (_ RR
19	17, 18	eqsstr 2081	. . . . 5 |- T (_ RR
20		breq1 2612	. . . . . . . . 9 |- (x = C -> (x < 0 <-> C < 0))
21		fveq2 3709	. . . . . . . . . 10 |- (x = C -> (sin` x) = (sin` C))
22	21	eqeq1d 1475	. . . . . . . . 9 |- (x = C -> ((sin` x) = 0 <-> (sin` C) = 0))
23	20, 22	anbi12d 626	. . . . . . . 8 |- (x = C -> ((x < 0 /\ (sin` x) = 0) <-> (C < 0 /\ (sin` C) = 0)))
24	23, 17	elrab2 1898	. . . . . . 7 |- (C e. T <-> (C e. RR /\ (C < 0 /\ (sin` C) = 0)))
25	15	3simp3i 791	. . . . . . . . 9 |- C < -u2
26		2pos 5936	. . . . . . . . . 10 |- 0 < 2
27		lt0neg2t 5642	. . . . . . . . . . 11 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
28	8, 27	ax-mp 7	. . . . . . . . . 10 |- (0 < 2 <-> -u2 < 0)
29	26, 28	mpbi 189	. . . . . . . . 9 |- -u2 < 0
30		0re 5412	. . . . . . . . . 10 |- 0 e. RR
31	16, 9, 30	lttr 5559	. . . . . . . . 9 |- ((C < -u2 /\ -u2 < 0) -> C < 0)
32	25, 29, 31	mp2an 695	. . . . . . . 8 |- C < 0
33	4	pm3.27i 324	. . . . . . . 8 |- (sin` C) = 0
34	32, 33	pm3.2i 285	. . . . . . 7 |- (C < 0 /\ (sin` C) = 0)
35	24, 16, 34	mpbir2an 728	. . . . . 6 |- C e. T
36		ne0i 2276	. . . . . 6 |- (C e. T -> T =/= (/))
37	35, 36	ax-mp 7	. . . . 5 |- T =/= (/)
38		ltlet 5493	. . . . . . . . 9 |- ((w e. RR /\ 0 e. RR) -> (w < 0 -> w <_ 0))
39	30, 38	mpan2 694	. . . . . . . 8 |- (w e. RR -> (w < 0 -> w <_ 0))
40	19	sseli 2055	. . . . . . . 8 |- (w e. T -> w e. RR)
41		breq1 2612	. . . . . . . . . . . 12 |- (x = w -> (x < 0 <-> w < 0))
42		fveq2 3709	. . . . . . . . . . . . 13 |- (x = w -> (sin` x) = (sin` w))
43	42	eqeq1d 1475	. . . . . . . . . . . 12 |- (x = w -> ((sin` x) = 0 <-> (sin` w) = 0))
44	41, 43	anbi12d 626	. . . . . . . . . . 11 |- (x = w -> ((x < 0 /\ (sin` x) = 0) <-> (w < 0 /\ (sin` w) = 0)))
45	44, 17	elrab2 1898	. . . . . . . . . 10 |- (w e. T <-> (w e. RR /\ (w < 0 /\ (sin` w) = 0)))
46	45	pm3.27bi 326	. . . . . . . . 9 |- (w e. T -> (w < 0 /\ (sin` w) = 0))
47	46	pm3.26d 321	. . . . . . . 8 |- (w e. T -> w < 0)
48	39, 40, 47	sylc 68	. . . . . . 7 |- (w e. T -> w <_ 0)
49	48	rgen 1690	. . . . . 6 |- A.w e. T w <_ 0
50		breq2 2613	. . . . . . . 8 |- (z = 0 -> (w <_ z <-> w <_ 0))
51	50	ralbidv 1655	. . . . . . 7 |- (z = 0 -> (A.w e. T w <_ z <-> A.w e. T w <_ 0))
52	51	rcla4ev 1868	. . . . . 6 |- ((0 e. RR /\ A.w e. T w <_ 0) -> E.z e. RR A.w e. T w <_ z)
53	30, 49, 52	mp2an 695	. . . . 5 |- E.z e. RR A.w e. T w <_ z
54	19, 37, 53	3pm3.2i 816	. . . 4 |- (T (_ RR /\ T =/= (/) /\ E.z e. RR A.w e. T w <_ z)
55	54	suprcli 6008	. . 3 |- sup(T, RR, < ) e. RR
56	16, 55	letri3 5547	. 2 |- (C = sup(T, RR, < ) <-> (C <_ sup(T, RR, < ) /\ sup(T, RR, < ) <_ C))
57	54	suprubi 6009	. . 3 |- (C e. T -> C <_ sup(T, RR, < ))
58	35, 57	ax-mp 7	. 2 |- C <_ sup(T, RR, < )
59		letrit 5594	. . . . . . . . . 10 |- ((-u4 e. RR /\ w e. RR) -> (-u4 <_ w \/ w <_ -u4))
60	7, 59	mpan 693	. . . . . . . . 9 |- (w e. RR -> (-u4 <_ w \/ w <_ -u4))
61	60	adantl 388	. . . . . . . 8 |- (((w < 0 /\ (sin` w) = 0) /\ w e. RR) -> (-u4 <_ w \/ w <_ -u4))
62	43, 1	elrab2 1898	. . . . . . . . . . . . . 14 |- (w e. S <-> (w e. (-u4[,)0) /\ (sin` w) = 0))
63		ssrab2 2121	. . . . . . . . . . . . . . . . . . 19 |- {x e. (-u4[,)0) | (sin` x) = 0} (_ (-u4[,)0)
64	1, 63	eqsstr 2081	. . . . . . . . . . . . . . . . . 18 |- S (_ (-u4[,)0)
65		elico2t 6323	. . . . . . . . . . . . . . . . . . . . . 22 |- ((-u4 e. RR /\ 0 e. RR) -> (w e. (-u4[,)0) <-> (w e. RR /\ -u4 <_ w /\ w < 0)))
66	7, 30, 65	mp2an 695	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. (-u4[,)0) <-> (w e. RR /\ -u4 <_ w /\ w < 0))
67	66	biimp 151	. . . . . . . . . . . . . . . . . . . 20 |- (w e. (-u4[,)0) -> (w e. RR /\ -u4 <_ w /\ w < 0))
68	67	3simp1d 792	. . . . . . . . . . . . . . . . . . 19 |- (w e. (-u4[,)0) -> w e. RR)
69	68	ssriv 2059	. . . . . . . . . . . . . . . . . 18 |- (-u4[,)0) (_ RR
70	64, 69	sstri 2063	. . . . . . . . . . . . . . . . 17 |- S (_ RR
71	22, 1	elrab2 1898	. . . . . . . . . . . . . . . . . . 19 |- (C e. S <-> (C e. (-u4[,)0) /\ (sin` C) = 0))
72	15	3simp2i 790	. . . . . . . . . . . . . . . . . . . . . 22 |- -u4 < C
73	7, 16, 72	ltlei 5554	. . . . . . . . . . . . . . . . . . . . 21 |- -u4 <_ C
74	16, 73, 32	3pm3.2i 816	. . . . . . . . . . . . . . . . . . . 20 |- (C e. RR /\ -u4 <_ C /\ C < 0)
75		elico2t 6323	. . . . . . . . . . . . . . . . . . . . 21 |- ((-u4 e. RR /\ 0 e. RR) -> (C e. (-u4[,)0) <-> (C e. RR /\ -u4 <_ C /\ C < 0)))
76	7, 30, 75	mp2an 695	. . . . . . . . . . . . . . . . . . . 20 |- (C e. (-u4[,)0) <-> (C e. RR /\ -u4 <_ C /\ C < 0))
77	74, 76	mpbir 190	. . . . . . . . . . . . . . . . . . 19 |- C e. (-u4[,)0)
78	71, 77, 33	mpbir2an 728	. . . . . . . . . . . . . . . . . 18 |- C e. S
79		ne0i 2276	. . . . . . . . . . . . . . . . . 18 |- (C e. S -> S =/= (/))
80	78, 79	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- S =/= (/)
81	70	sseli 2055	. . . . . . . . . . . . . . . . . . . 20 |- (w e. S -> w e. RR)
82	62	pm3.26bi 322	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. S -> w e. (-u4[,)0))
83	82, 66	sylib 198	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. S -> (w e. RR /\ -u4 <_ w /\ w < 0))
84	83	3simp3d 794	. . . . . . . . . . . . . . . . . . . 20 |- (w e. S -> w < 0)
85	39, 81, 84	sylc 68	. . . . . . . . . . . . . . . . . . 19 |- (w e. S -> w <_ 0)
86	85	rgen 1690	. . . . . . . . . . . . . . . . . 18 |- A.w e. S w <_ 0
87	50	ralbidv 1655	. . . . . . . . . . . . . . . . . . 19 |- (z = 0 -> (A.w e. S w <_ z <-> A.w e. S w <_ 0))
88	87	rcla4ev 1868	. . . . . . . . . . . . . . . . . 18 |- ((0 e. RR /\ A.w e. S w <_ 0) -> E.z e. RR A.w e. S w <_ z)
89	30, 86, 88	mp2an 695	. . . . . . . . . . . . . . . . 17 |- E.z e. RR A.w e. S w <_ z
90	70, 80, 89	3pm3.2i 816	. . . . . . . . . . . . . . . 16 |- (S (_ RR /\ S =/= (/) /\ E.z e. RR A.w e. S w <_ z)
91	90	suprubi 6009	. . . . . . . . . . . . . . 15 |- (w e. S -> w <_ sup(S, RR, < ))
92	91, 2	syl6breqr 2645	. . . . . . . . . . . . . 14 |- (w e. S -> w <_ C)
93	62, 92	sylbir 201	. . . . . . . . . . . . 13 |- ((w e. (-u4[,)0) /\ (sin` w) = 0) -> w <_ C)
94	93, 66	sylanbr 450	. . . . . . . . . . . 12 |- (((w e. RR /\ -u4 <_ w /\ w < 0) /\ (sin` w) = 0) -> w <_ C)
95	94	3exp1 847	. . . . . . . . . . 11 |- (w e. RR -> (-u4 <_ w -> (w < 0 -> ((sin` w) = 0 -> w <_ C))))
96	95	com4t 40	. . . . . . . . . 10 |- (w < 0 -> ((sin` w) = 0 -> (w e. RR -> (-u4 <_ w -> w <_ C))))
97	96	imp31 362	. . . . . . . . 9 |- (((w < 0 /\ (sin` w) = 0) /\ w e. RR) -> (-u4 <_ w -> w <_ C))
98		letrt 5498	. . . . . . . . . . . 12 |- ((w e. RR /\ -u4 e. RR /\ C e. RR) -> ((w <_ -u4 /\ -u4 <_ C) -> w <_ C))
99	7, 16, 98	mp3an23 905	. . . . . . . . . . 11 |- (w e. RR -> ((w <_ -u4 /\ -u4 <_ C) -> w <_ C))
100	73, 99	mpan2i 697	. . . . . . . . . 10 |- (w e. RR -> (w <_ -u4 -> w <_ C))
101	100	adantl 388	. . . . . . . . 9