Theorem pilem3 8940

Description: Lemma for pire 8944, pigt2lt4 8942 and sinpi 8943.

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 2183	. . . . . . 7 |- {x e. RR | (0 < x /\ (sin` x) = 0)} (_ RR
3	1, 2	eqsstri 2143	. . . . . 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 1518	. . . . . . . . . . . . . 14 |- {x e. (-u4[,]-u2) | (sin` x) = 0} = {x e. (-u4[,]-u2) | (sin` x) = 0}
7	4, 5, 6	pilem1 8938	. . . . . . . . . . . . 13 |- (C e. (-u4(,)-u2) /\ (sin` C) = 0)
8	7	pm3.26i 318	. . . . . . . . . . . 12 |- C e. (-u4(,)-u2)
9		4re 6128	. . . . . . . . . . . . . 14 |- 4 e. RR
10	9	renegcli 5570	. . . . . . . . . . . . 13 |- -u4 e. RR
11		2re 6125	. . . . . . . . . . . . . 14 |- 2 e. RR
12	11	renegcli 5570	. . . . . . . . . . . . 13 |- -u2 e. RR
13		elioo2 6505	. . . . . . . . . . . . . 14 |- ((-u4 e. RR* /\ -u2 e. RR*) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
14		rexr 5653	. . . . . . . . . . . . . 14 |- (-u4 e. RR -> -u4 e. RR*)
15		rexr 5653	. . . . . . . . . . . . . 14 |- (-u2 e. RR -> -u2 e. RR*)
16	13, 14, 15	syl2an 456	. . . . . . . . . . . . 13 |- ((-u4 e. RR /\ -u2 e. RR) -> (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2)))
17	10, 12, 16	mp2an 701	. . . . . . . . . . . 12 |- (C e. (-u4(,)-u2) <-> (C e. RR /\ -u4 < C /\ C < -u2))
18	8, 17	mpbi 187	. . . . . . . . . . 11 |- (C e. RR /\ -u4 < C /\ C < -u2)
19	18	3simp3i 799	. . . . . . . . . 10 |- C < -u2
20		2pos 6135	. . . . . . . . . . 11 |- 0 < 2
21		lt0neg2 5823	. . . . . . . . . . . 12 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
22	11, 21	ax-mp 7	. . . . . . . . . . 11 |- (0 < 2 <-> -u2 < 0)
23	20, 22	mpbi 187	. . . . . . . . . 10 |- -u2 < 0
24	18	3simp1i 797	. . . . . . . . . . 11 |- C e. RR
25		0re 5594	. . . . . . . . . . 11 |- 0 e. RR
26	24, 12, 25	lttri 5739	. . . . . . . . . 10 |- ((C < -u2 /\ -u2 < 0) -> C < 0)
27	19, 23, 26	mp2an 701	. . . . . . . . 9 |- C < 0
28		lt0neg1 5822	. . . . . . . . . 10 |- (C e. RR -> (C < 0 <-> 0 < -uC))
29	24, 28	ax-mp 7	. . . . . . . . 9 |- (C < 0 <-> 0 < -uC)
30	27, 29	mpbi 187	. . . . . . . 8 |- 0 < -uC
31	24	recni 5468	. . . . . . . . . 10 |- C e. CC
32		sinneg 7650	. . . . . . . . . 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 322	. . . . . . . . . 10 |- (sin` C) = 0
35	34	negeqi 5514	. . . . . . . . 9 |- -u(sin` C) = -u0
36		neg0 5569	. . . . . . . . 9 |- -u0 = 0
37	33, 35, 36	3eqtri 1542	. . . . . . . 8 |- (sin` -uC) = 0
38	24	renegcli 5570	. . . . . . . . 9 |- -uC e. RR
39		breq2 2696	. . . . . . . . . . . 12 |- (x = -uC -> (0 < x <-> 0 < -uC))
40		fveq2 3835	. . . . . . . . . . . . 13 |- (x = -uC -> (sin` x) = (sin` -uC))
41	40	eqeq1d 1526	. . . . . . . . . . . 12 |- (x = -uC -> ((sin` x) = 0 <-> (sin` -uC) = 0))
42	39, 41	anbi12d 631	. . . . . . . . . . 11 |- (x = -uC -> ((0 < x /\ (sin` x) = 0) <-> (0 < -uC /\ (sin` -uC) = 0)))
43	42, 1	elrab2 1953	. . . . . . . . . 10 |- (-uC e. P <-> (-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)))
44	43	biimpri 150	. . . . . . . . 9 |- ((-uC e. RR /\ (0 < -uC /\ (sin` -uC) = 0)) -> -uC e. P)
45	38, 44	mpan 699	. . . . . . . 8 |- ((0 < -uC /\ (sin` -uC) = 0) -> -uC e. P)
46	30, 37, 45	mp2an 701	. . . . . . 7 |- -uC e. P
47		ne0i 2338	. . . . . . 7 |- (-uC e. P -> P =/= (/))
48	46, 47	ax-mp 7	. . . . . 6 |- P =/= (/)
49		ltle 5674	. . . . . . . . . 10 |- ((0 e. RR /\ w e. RR) -> (0 < w -> 0 <_ w))
50	25, 49	mpan 699	. . . . . . . . 9 |- (w e. RR -> (0 < w -> 0 <_ w))
51		breq2 2696	. . . . . . . . . . . 12 |- (x = w -> (0 < x <-> 0 < w))
52		fveq2 3835	. . . . . . . . . . . . 13 |- (x = w -> (sin` x) = (sin` w))
53	52	eqeq1d 1526	. . . . . . . . . . . 12 |- (x = w -> ((sin` x) = 0 <-> (sin` w) = 0))
54	51, 53	anbi12d 631	. . . . . . . . . . 11 |- (x = w -> ((0 < x /\ (sin` x) = 0) <-> (0 < w /\ (sin` w) = 0)))
55	54, 1	elrab2 1953	. . . . . . . . . 10 |- (w e. P <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
56	55	pm3.26bi 320	. . . . . . . . 9 |- (w e. P -> w e. RR)
57		3anass 785	. . . . . . . . . . . 12 |- ((w e. RR /\ 0 < w /\ (sin` w) = 0) <-> (w e. RR /\ (0 < w /\ (sin` w) = 0)))
58	55, 57	bitr4i 174	. . . . . . . . . . 11 |- (w e. P <-> (w e. RR /\ 0 < w /\ (sin` w) = 0))
59	58	biimpi 149	. . . . . . . . . 10 |- (w e. P -> (w e. RR /\ 0 < w /\ (sin` w) = 0))
60	59	3simp2d 801	. . . . . . . . 9 |- (w e. P -> 0 < w)
61	50, 56, 60	sylc 68	. . . . . . . 8 |- (w e. P -> 0 <_ w)
62	61	rgen 1744	. . . . . . 7 |- A.w e. P 0 <_ w
63		breq1 2695	. . . . . . . . 9 |- (z = 0 -> (z <_ w <-> 0 <_ w))
64	63	ralbidv 1709	. . . . . . . 8 |- (z = 0 -> (A.w e. P z <_ w <-> A.w e. P 0 <_ w))
65	64	rcla4ev 1923	. . . . . . 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 701	. . . . . 6 |- E.z e. RR A.w e. P z <_ w
67		infmsup 6236	. . . . . . 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 7507	. . . . . . . 8 |- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
69		supeq1 4718	. . . . . . . . 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 1541	. . . . . . 7 |- pi = sup(P, RR, `' < )
72	67, 71	syl5eq 1562	. . . . . 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 922	. . . . 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 8939	. . . . . . 7 |- C = sup(T, RR, < )
76		breq1 2695	. . . . . . . . . . 11 |- (x = v -> (x < 0 <-> v < 0))
77		fveq2 3835	. . . . . . . . . . . 12 |- (x = v -> (sin` x) = (sin` v))
78	77	eqeq1d 1526	. . . . . . . . . . 11 |- (x = v -> ((sin` x) = 0 <-> (sin` v) = 0))
79	76, 78	anbi12d 631	. . . . . . . . . 10 |- (x = v -> ((x < 0 /\ (sin` x) = 0) <-> (v < 0 /\ (sin` v) = 0)))
80	79	cbvrabv 1957	. . . . . . . . 9 |- {x e. RR | (x < 0 /\ (sin` x) = 0)} = {v e. RR | (v < 0 /\ (sin` v) = 0)}
81		lt0neg1 5822	. . . . . . . . . . . . 13 |- (v e. RR -> (v < 0 <-> 0 < -uv))
82		resincl 7646	. . . . . . . . . . . . . . . 16 |- (v e. RR -> (sin` v) e. RR)
83	82	recnd 5469	. . . . . . . . . . . . . . 15 |- (v e. RR -> (sin` v) e. CC)
84		negeq0 5946	. . . . . . . . . . . . . . 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 5467	. . . . . . . . . . . . . . . 16 |- (v e. RR -> v e. CC)
87		sinneg 7650	. . . . . . . . . . . . . . . 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 1526	. . . . . . . . . . . . . 14 |- (v e. RR -> ((sin` -uv) = 0 <-> -u(sin` v) = 0))
90	85, 89	bitr4d 534	. . . . . . . . . . . . 13 |- (v e. RR -> ((sin` v) = 0 <-> (sin` -uv) = 0))
91	81, 90	anbi12d 631	. . . . . . . . . . . 12 |- (v e. RR -> ((v < 0 /\ (sin` v) = 0) <-> (0 < -uv /\ (sin` -uv) = 0)))
92		renegcl 5591	. . . . . . . . . . . . 13 |- (v e. RR -> -uv e. RR)
93	92	biantrurd 732	. . . . . . . . . . . 12 |- (v e. RR -> ((0 < -uv /\ (sin` -uv) = 0) <-> (-uv e. RR /\ (0 < -uv /\ (sin` -uv) = 0))))
94	91, 93	bitrd 531	. . . . . . . . . . 11 |- (v e. RR -> ((v < 0 /\ (sin` v) = 0) <-> (-uv e. RR /\ (0 < -uv /\ (sin` -uv) = 0))))
95		breq2 2696	. . . . . . . . . . . . 13 |- (x = -uv -> (0 < x <-> 0 < -uv))
96		fveq2 3835	. . . . . . . . . . . . . 14 |- (x = -uv -> (sin` x) = (sin` -uv))
97	96	eqeq1d 1526	. . . . . . . . . . . . 13 |- (x = -uv -> ((sin` x) = 0 <-> (sin` -uv) = 0))
98	95, 97	anbi12d 631	. . . . . . . . . . . 12 |- (x = -uv -> ((0 < x /\ (sin` x) = 0) <-> (0 < -uv /\ (sin` -uv) = 0)))
99	98, 1	elrab2 1953	. . . . . . . . . . 11 |- (-uv e. P <-> (-uv e. RR /\ (0 < -uv /\ (sin` -uv) = 0)))
100	94, 99	syl6bbr 541	. . . . . . . . . 10 |- (v e. RR -> ((v < 0 /\ (sin` v) = 0) <-> -uv e. P))
101	100	rabbii 1851	. . . . . . . . 9 |- {v e. RR | (v < 0 /\ (sin` v) = 0)} = {v e. RR | -uv e. P}
102	74, 80, 101	3eqtri 1542	. . . . . . . 8 |- T = {v e. RR | -uv e. P}
103		supeq1 4718	. . . . . . . 8 |- (T = {v e. RR | -uv e. P} -> sup(T, RR, < ) = sup({v e. RR | -uv e. P}, RR, < ))
104	102, 103	ax-mp 7	. . . . . . 7 |- sup(T, RR, < ) = sup({v e. RR | -uv e. P}, RR, < )
105	75, 104	eqtri 1538	. . . . . 6 |- C = sup({v e. RR | -uv e. P}, RR, < )
106	105	negeqi 5514	. . . . 5 |- -uC = -usup({v e. RR | -uv e. P}, RR, < )
107	73, 106	eqtr4i 1541	. . . 4 |- pi = -uC
108	107, 38	eqeltri 1587	. . 3 |- pi e. RR
109	30, 107	breqtrri 2713	. . 3 |- 0 < pi
110	108, 109	elrpii 6193	. 2 |- pi e. RR+
111		iooneg 6533	. . . . . 6 |- ((2 e. RR /\ 4 e. RR /\ -uC e. RR) -> (-uC e. (2(,)4) <-> -u-uC e. (-u4(,)-u2)))
112	11, 9, 38, 111	mp3an 922	. . . . 5 |- (-uC e. (2(,)4) <-> -u-uC e. (-u4(,)-u2))
113	31	negnegi 5544	. . . . . 6 |- -u-uC = C
114	113	eleq1i 1580	. . . . 5 |- (-u-uC e. (-u4(,)-u2) <-> C e. (-u4(,)-u2))
115	112, 114	bitr2i 172	. . . 4 |- (C e. (-u4(,)-u2) <-> -uC e. (2(,)4))
116	8, 115	mpbi 187	. . 3 |- -uC e. (2(,)4)
117	107, 116	eqeltri 1587	. 2 |- pi e. (2(,)4)
118	107	fveq2i 3838	. . 3 |- (sin` pi) = (sin` -uC)
119	118, 37	eqtri 1538	. 2 |- (sin` pi) = 0
120	110, 117, 119	3pm3.2i 824	1 |- (pi e. RR+ /\ pi e. (2(,)4) /\ (sin` pi) = 0)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994   =/= wne 1628  A.wral 1691  E.wrex 1692  {crab 1694   (_ wss 2099  (/)c0 2332   class class class wbr 2692  `'ccnv 3250  ` cfv 3263  (class class class)co 4021  supcsup 4716  CCcc 5386  RRcr 5387  0cc0 5388  -ucneg 5447   <_ cle 5449  RR+crp 5454  RR*cxr 5639   < clt 5640  2c2 6107  4c4 6109  (,)cioo 6483  [,)cico 6485  [,]cicc 6486  sincsin 7500  picpi 7502

This theorem is referenced by:  pilem4 8941

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-reg 4736  ax-inf2 4770  ax-ac 4890

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-iin 2636  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-map 4465  df-en 4509  df-dom 4510  df-sdom 4511  df-sup 4717  df-r1 4789  df-rank 4790  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-div 5855  df-n 6070  df-2 6116  df-3 6117  df-4 6118  df-5 6119  df-6 6120  df-7 6121  df-8 6122  df-9 6123  df-rp 6191  df-n0 6268  df-z 6304  df-q 6395  df-fl 6422  df-ioo 6487  df-ioc 6488  df-ico 6489  df-icc 6490  df-uz 6545  df-fz 6596  df-seq1 6673  df-shft 6706  df-seqz 6728  df-seq0 6729  df-exp 6764  df-sqr 6871  df-re 6952  df-im 6953  df-cj 6954  df-abs 6955  df-fac 7135  df-bc 7160  df-clim 7178  df-sum 7183  df-cncf 7468  df-ef 7503  df-sin 7505  df-cos 7506  df-pi 7507  df-top 7804  df-cn 7964  df-cnp 7965  df-met 8003  df-bl 8005  df-opn 8006  df-lm 8133

Copyright terms: Public domain