Theorem pilem1 8609

Description: Lemma for pire 8615, pigt2lt4 8613 and sinpi 8614.

Hypotheses

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

Assertion

Ref	Expression
pilem1	|- (C e. (-u4(,)-u2) /\ (sin` C) = 0)

Distinct variable group:   x,C

Proof of Theorem pilem1

Step	Hyp	Ref	Expression
1		4re 5937	. . 3 |- 4 e. RR
2	1	renegcl 5396	. 2 |- -u4 e. RR
3		2re 5934	. . 3 |- 2 e. RR
4	3	renegcl 5396	. 2 |- -u2 e. RR
5		0re 5420	. 2 |- 0 e. RR
6		2pos 5944	. . . . 5 |- 0 < 2
7	5, 3, 3	ltadd1 5573	. . . . 5 |- (0 < 2 <-> (0 + 2) < (2 + 2))
8	6, 7	mpbi 189	. . . 4 |- (0 + 2) < (2 + 2)
9		2cn 5935	. . . . 5 |- 2 e. CC
10	9	addid2 5311	. . . 4 |- (0 + 2) = 2
11		2p2e4 5956	. . . 4 |- (2 + 2) = 4
12	8, 10, 11	3brtr3 2637	. . 3 |- 2 < 4
13	3, 1	ltneg 5585	. . 3 |- (2 < 4 <-> -u4 < -u2)
14	12, 13	mpbi 189	. 2 |- -u4 < -u2
15		iccssret 6337	. . . 4 |- ((-u4 e. RR /\ -u2 e. RR) -> (-u4[,]-u2) (_ RR)
16	2, 4, 15	mp2an 696	. . 3 |- (-u4[,]-u2) (_ RR
17		axresscn 5248	. . 3 |- RR (_ CC
18	16, 17	sstri 2069	. 2 |- (-u4[,]-u2) (_ CC
19		ssid 2076	. 2 |- CC (_ CC
20		sincn 8607	. 2 |- sin e. (CC-cn->CC)
21	16	sseli 2061	. . 3 |- (x e. (-u4[,]-u2) -> x e. RR)
22		resinclt 7388	. . 3 |- (x e. RR -> (sin` x) e. RR)
23	21, 22	syl 10	. 2 |- (x e. (-u4[,]-u2) -> (sin` x) e. RR)
24		letrit 5602	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 e. RR) -> (y <_ -u2 \/ -u2 <_ y))
25	4, 24	mpan2 695	. . . . . . . . . . . . 13 |- (y e. RR -> (y <_ -u2 \/ -u2 <_ y))
26	25	biantrurd 726	. . . . . . . . . . . 12 |- (y e. RR -> (y < 0 <-> ((y <_ -u2 \/ -u2 <_ y) /\ y < 0)))
27		andir 604	. . . . . . . . . . . 12 |- (((y <_ -u2 \/ -u2 <_ y) /\ y < 0) <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0)))
28	26, 27	syl6bb 535	. . . . . . . . . . 11 |- (y e. RR -> (y < 0 <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0))))
29		lt0neg2t 5650	. . . . . . . . . . . . . . . 16 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
30	3, 29	ax-mp 7	. . . . . . . . . . . . . . 15 |- (0 < 2 <-> -u2 < 0)
31	6, 30	mpbi 189	. . . . . . . . . . . . . 14 |- -u2 < 0
32		lelttrt 5504	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 e. RR /\ 0 e. RR) -> ((y <_ -u2 /\ -u2 < 0) -> y < 0))
33	4, 5, 32	mp3an23 906	. . . . . . . . . . . . . 14 |- (y e. RR -> ((y <_ -u2 /\ -u2 < 0) -> y < 0))
34	31, 33	mpan2i 698	. . . . . . . . . . . . 13 |- (y e. RR -> (y <_ -u2 -> y < 0))
35		pm4.71 634	. . . . . . . . . . . . 13 |- ((y <_ -u2 -> y < 0) <-> (y <_ -u2 <-> (y <_ -u2 /\ y < 0)))
36	34, 35	sylib 198	. . . . . . . . . . . 12 |- (y e. RR -> (y <_ -u2 <-> (y <_ -u2 /\ y < 0)))
37	36	orbi1d 614	. . . . . . . . . . 11 |- (y e. RR -> ((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0))))
38	28, 37	bitr4d 530	. . . . . . . . . 10 |- (y e. RR -> (y < 0 <-> (y <_ -u2 \/ (-u2 <_ y /\ y < 0))))
39	38	anbi1d 616	. . . . . . . . 9 |- (y e. RR -> ((y < 0 /\ (sin` y) = 0) <-> ((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) /\ (sin` y) = 0)))
40		andir 604	. . . . . . . . 9 |- (((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0)))
41	39, 40	syl6bb 535	. . . . . . . 8 |- (y e. RR -> ((y < 0 /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))))
42		renegclt 5417	. . . . . . . . . . . . . . 15 |- (y e. RR -> -uy e. RR)
43	42	3ad2ant1 799	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -uy e. RR)
44		lt0neg1t 5649	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (y < 0 <-> 0 < -uy))
45	44	adantr 389	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 <_ y) -> (y < 0 <-> 0 < -uy))
46	45	biimp3a 917	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> 0 < -uy)
47		lenegcon1t 5639	. . . . . . . . . . . . . . . . 17 |- ((2 e. RR /\ y e. RR) -> (-u2 <_ y <-> -uy <_ 2))
48	3, 47	mpan 694	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (-u2 <_ y <-> -uy <_ 2))
49	48	biimpa 416	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 <_ y) -> -uy <_ 2)
50	49	3adant3 798	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -uy <_ 2)
51	43, 46, 50	3jca 818	. . . . . . . . . . . . 13 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2))
52		elioc2t 6330	. . . . . . . . . . . . . . 15 |- ((0 e. RR /\ 2 e. RR) -> (-uy e. (0(,]2) <-> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2)))
53	5, 3, 52	mp2an 696	. . . . . . . . . . . . . 14 |- (-uy e. (0(,]2) <-> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2))
54	53	biimpr 152	. . . . . . . . . . . . 13 |- ((-uy e. RR /\ 0 < -uy /\ -uy <_ 2) -> -uy e. (0(,]2))
55		sin02gt0 7428	. . . . . . . . . . . . 13 |- (-uy e. (0(,]2) -> 0 < (sin` -uy))
56	51, 54, 55	3syl 20	. . . . . . . . . . . 12 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> 0 < (sin` -uy))
57		recnt 5293	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> y e. CC)
58		sinnegt 7392	. . . . . . . . . . . . . . . . . 18 |- (y e. CC -> (sin` -uy) = -u(sin` y))
59	57, 58	syl 10	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (sin` -uy) = -u(sin` y))
60	59	breq2d 2625	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (0 < (sin` -uy) <-> 0 < -u(sin` y)))
61		resinclt 7388	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (sin` y) e. RR)
62		lt0neg1t 5649	. . . . . . . . . . . . . . . . 17 |- ((sin` y) e. RR -> ((sin` y) < 0 <-> 0 < -u(sin` y)))
63	61, 62	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. RR -> ((sin` y) < 0 <-> 0 < -u(sin` y)))
64	60, 63	bitr4d 530	. . . . . . . . . . . . . . 15 |- (y e. RR -> (0 < (sin` -uy) <-> (sin` y) < 0))
65		ltnet 5496	. . . . . . . . . . . . . . . . . 18 |- (((sin` y) e. RR /\ 0 e. RR /\ (sin` y) < 0) -> 0 =/= (sin` y))
66	5, 65	mp3an2 902	. . . . . . . . . . . . . . . . 17 |- (((sin` y) e. RR /\ (sin` y) < 0) -> 0 =/= (sin` y))
67	66	ex 373	. . . . . . . . . . . . . . . 16 |- ((sin` y) e. RR -> ((sin` y) < 0 -> 0 =/= (sin` y)))
68	61, 67	syl 10	. . . . . . . . . . . . . . 15 |- (y e. RR -> ((sin` y) < 0 -> 0 =/= (sin` y)))
69	64, 68	sylbid 203	. . . . . . . . . . . . . 14 |- (y e. RR -> (0 < (sin` -uy) -> 0 =/= (sin` y)))
70		necom 1633	. . . . . . . . . . . . . . 15 |- (0 =/= (sin` y) <-> (sin` y) =/= 0)
71		df-ne 1584	. . . . . . . . . . . . . . 15 |- ((sin` y) =/= 0 <-> -. (sin` y) = 0)
72	70, 71	bitr 173	. . . . . . . . . . . . . 14 |- (0 =/= (sin` y) <-> -. (sin` y) = 0)
73	69, 72	syl6ib 212	. . . . . . . . . . . . 13 |- (y e. RR -> (0 < (sin` -uy) -> -. (sin` y) = 0))
74	73	3ad2ant1 799	. . . . . . . . . . . 12 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> (0 < (sin` -uy) -> -. (sin` y) = 0))
75	56, 74	mpd 26	. . . . . . . . . . 11 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -. (sin` y) = 0)
76	75	3expib 835	. . . . . . . . . 10 |- (y e. RR -> ((-u2 <_ y /\ y < 0) -> -. (sin` y) = 0))
77		imnan 242	. . . . . . . . . 10 |- (((-u2 <_ y /\ y < 0) -> -. (sin` y) = 0) <-> -. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))
78	76, 77	sylib 198	. . . . . . . . 9 |- (y e. RR -> -. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))
79		biorf 734	. . . . . . . . . 10 |- (-. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) -> ((y <_ -u2 /\ (sin` y) = 0) <-> (((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) \/ (y <_ -u2 /\ (sin` y) = 0))))
80		orcom 246	. . . . . . . . . 10 |- ((((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) \/ (y <_ -u2 /\ (sin` y) = 0)) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ (