Metamath Proof Explorer

Theorem pilem3

Description: Lemma for pire , pigt2lt4 and sinpi . Existence part. (Contributed by Paul Chapman, 23-Jan-2008) (Proof shortened by Mario Carneiro, 18-Jun-2014) (Revised by AV, 14-Sep-2020) (Proof shortened by BJ, 30-Jun-2022)

Ref Expression
Assertion pilem3 
|- ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( T. -> 2 e. RR )
3 4re 
 |-  4 e. RR
4 3 a1i 
 |-  ( T. -> 4 e. RR )
5 0red 
 |-  ( T. -> 0 e. RR )
6 2lt4 
 |-  2 < 4
7 6 a1i 
 |-  ( T. -> 2 < 4 )
8 iccssre 
 |-  ( ( 2 e. RR /\ 4 e. RR ) -> ( 2 [,] 4 ) C_ RR )
9 1 3 8 mp2an 
 |-  ( 2 [,] 4 ) C_ RR
10 ax-resscn 
 |-  RR C_ CC
11 9 10 sstri 
 |-  ( 2 [,] 4 ) C_ CC
12 11 a1i 
 |-  ( T. -> ( 2 [,] 4 ) C_ CC )
13 sincn 
 |-  sin e. ( CC -cn-> CC )
14 13 a1i 
 |-  ( T. -> sin e. ( CC -cn-> CC ) )
15 9 sseli 
 |-  ( y e. ( 2 [,] 4 ) -> y e. RR )
16 15 resincld 
 |-  ( y e. ( 2 [,] 4 ) -> ( sin ` y ) e. RR )
17 16 adantl 
 |-  ( ( T. /\ y e. ( 2 [,] 4 ) ) -> ( sin ` y ) e. RR )
18 sin4lt0 
 |-  ( sin ` 4 ) < 0
19 sincos2sgn 
 |-  ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
20 19 simpli 
 |-  0 < ( sin ` 2 )
21 18 20 pm3.2i 
 |-  ( ( sin ` 4 ) < 0 /\ 0 < ( sin ` 2 ) )
22 21 a1i 
 |-  ( T. -> ( ( sin ` 4 ) < 0 /\ 0 < ( sin ` 2 ) ) )
23 2 4 5 7 12 14 17 22 ivth2 
 |-  ( T. -> E. x e. ( 2 (,) 4 ) ( sin ` x ) = 0 )
24 23 mptru 
 |-  E. x e. ( 2 (,) 4 ) ( sin ` x ) = 0
25 df-pi 
 |-  _pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
26 inss1 
 |-  ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR+
27 rpssre 
 |-  RR+ C_ RR
28 26 27 sstri 
 |-  ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR
29 0re 
 |-  0 e. RR
30 26 sseli 
 |-  ( z e. ( RR+ i^i ( `' sin " { 0 } ) ) -> z e. RR+ )
31 30 rpge0d 
 |-  ( z e. ( RR+ i^i ( `' sin " { 0 } ) ) -> 0 <_ z )
32 31 rgen 
 |-  A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ z
33 breq1 
 |-  ( y = 0 -> ( y <_ z <-> 0 <_ z ) )
34 33 ralbidv 
 |-  ( y = 0 -> ( A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z <-> A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ z ) )
35 34 rspcev 
 |-  ( ( 0 e. RR /\ A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ z ) -> E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z )
36 29 32 35 mp2an 
 |-  E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z
37 elioore 
 |-  ( x e. ( 2 (,) 4 ) -> x e. RR )
38 37 adantr 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. RR )
39 0red 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> 0 e. RR )
40 1 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> 2 e. RR )
41 2pos 
 |-  0 < 2
42 41 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> 0 < 2 )
43 eliooord 
 |-  ( x e. ( 2 (,) 4 ) -> ( 2 < x /\ x < 4 ) )
44 43 simpld 
 |-  ( x e. ( 2 (,) 4 ) -> 2 < x )
45 44 adantr 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> 2 < x )
46 39 40 38 42 45 lttrd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> 0 < x )
47 38 46 elrpd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. RR+ )
48 simpr 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( sin ` x ) = 0 )
49 pilem1 
 |-  ( x e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( x e. RR+ /\ ( sin ` x ) = 0 ) )
50 47 48 49 sylanbrc 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. ( RR+ i^i ( `' sin " { 0 } ) ) )
51 infrelb 
 |-  ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z /\ x e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ x )
52 28 36 50 51 mp3an12i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ x )
53 25 52 eqbrtrid 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi <_ x )
54 simpll 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> x e. ( 2 (,) 4 ) )
55 simpr 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> y e. ( RR+ i^i ( `' sin " { 0 } ) ) )
56 pilem1 
 |-  ( y e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( y e. RR+ /\ ( sin ` y ) = 0 ) )
57 55 56 sylib 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( y e. RR+ /\ ( sin ` y ) = 0 ) )
58 57 simpld 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> y e. RR+ )
59 simplr 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( sin ` x ) = 0 )
60 57 simprd 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( sin ` y ) = 0 )
61 54 58 59 60 pilem2 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( ( _pi + x ) / 2 ) <_ y )
62 61 ralrimiva 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) ( ( _pi + x ) / 2 ) <_ y )
63 28 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR )
64 50 ne0d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) )
65 36 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z )
66 infrecl 
 |-  ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) /\ E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
67 28 36 66 mp3an13 
 |-  ( ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
68 64 67 syl 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
69 25 68 eqeltrid 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. RR )
70 69 38 readdcld 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi + x ) e. RR )
71 70 rehalfcld 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) e. RR )
72 infregelb 
 |-  ( ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) /\ E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z ) /\ ( ( _pi + x ) / 2 ) e. RR ) -> ( ( ( _pi + x ) / 2 ) <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <-> A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) ( ( _pi + x ) / 2 ) <_ y ) )
73 63 64 65 71 72 syl31anc 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( ( _pi + x ) / 2 ) <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <-> A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) ( ( _pi + x ) / 2 ) <_ y ) )
74 62 73 mpbird 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) )
75 74 25 breqtrrdi 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) <_ _pi )
76 69 recnd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. CC )
77 38 recnd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. CC )
78 76 77 addcomd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi + x ) = ( x + _pi ) )
79 78 oveq1d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) = ( ( x + _pi ) / 2 ) )
80 79 breq1d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( ( _pi + x ) / 2 ) <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
81 avgle2 
 |-  ( ( x e. RR /\ _pi e. RR ) -> ( x <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
82 38 69 81 syl2anc 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( x <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
83 80 82 bitr4d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( ( _pi + x ) / 2 ) <_ _pi <-> x <_ _pi ) )
84 75 83 mpbid 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x <_ _pi )
85 69 38 letri3d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi = x <-> ( _pi <_ x /\ x <_ _pi ) ) )
86 53 84 85 mpbir2and 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi = x )
87 simpl 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. ( 2 (,) 4 ) )
88 86 87 eqeltrd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. ( 2 (,) 4 ) )
89 86 fveq2d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( sin ` _pi ) = ( sin ` x ) )
90 89 48 eqtrd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( sin ` _pi ) = 0 )
91 88 90 jca 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 ) )
92 91 rexlimiva 
 |-  ( E. x e. ( 2 (,) 4 ) ( sin ` x ) = 0 -> ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 ) )
93 24 92 ax-mp 
 |-  ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 )