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 pilem1 
 |-  ( y e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( y e. RR+ /\ ( sin ` y ) = 0 ) )
56 55 bilani 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( y e. RR+ /\ ( sin ` y ) = 0 ) )
57 56 simpld 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> y e. RR+ )
58 simplr 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( sin ` x ) = 0 )
59 56 simprd 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( sin ` y ) = 0 )
60 54 57 58 59 pilem2 
 |-  ( ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) /\ y e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> ( ( _pi + x ) / 2 ) <_ y )
61 60 ralrimiva 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) ( ( _pi + x ) / 2 ) <_ y )
62 28 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR )
63 50 ne0d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) )
64 36 a1i 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> E. y e. RR A. z e. ( RR+ i^i ( `' sin " { 0 } ) ) y <_ z )
65 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 )
66 28 36 65 mp3an13 
 |-  ( ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
67 63 66 syl 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
68 25 67 eqeltrid 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. RR )
69 68 38 readdcld 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi + x ) e. RR )
70 69 rehalfcld 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) e. RR )
71 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 ) )
72 62 63 64 70 71 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 ) )
73 61 72 mpbird 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) )
74 73 25 breqtrrdi 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) <_ _pi )
75 68 recnd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. CC )
76 38 recnd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. CC )
77 75 76 addcomd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi + x ) = ( x + _pi ) )
78 77 oveq1d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( _pi + x ) / 2 ) = ( ( x + _pi ) / 2 ) )
79 78 breq1d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( ( _pi + x ) / 2 ) <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
80 avgle2 
 |-  ( ( x e. RR /\ _pi e. RR ) -> ( x <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
81 38 68 80 syl2anc 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( x <_ _pi <-> ( ( x + _pi ) / 2 ) <_ _pi ) )
82 79 81 bitr4d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( ( ( _pi + x ) / 2 ) <_ _pi <-> x <_ _pi ) )
83 74 82 mpbid 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x <_ _pi )
84 68 38 letri3d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi = x <-> ( _pi <_ x /\ x <_ _pi ) ) )
85 53 83 84 mpbir2and 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi = x )
86 simpl 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> x e. ( 2 (,) 4 ) )
87 85 86 eqeltrd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> _pi e. ( 2 (,) 4 ) )
88 85 fveq2d 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( sin ` _pi ) = ( sin ` x ) )
89 88 48 eqtrd 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( sin ` _pi ) = 0 )
90 87 89 jca 
 |-  ( ( x e. ( 2 (,) 4 ) /\ ( sin ` x ) = 0 ) -> ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 ) )
91 90 rexlimiva 
 |-  ( E. x e. ( 2 (,) 4 ) ( sin ` x ) = 0 -> ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 ) )
92 24 91 ax-mp 
 |-  ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 )