Metamath Proof Explorer

Theorem pilem2

Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 12-Jun-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses pilem2.1 
|- ( ph -> A e. ( 2 (,) 4 ) )
pilem2.2 
|- ( ph -> B e. RR+ )
pilem2.3 
|- ( ph -> ( sin ` A ) = 0 )
pilem2.4 
|- ( ph -> ( sin ` B ) = 0 )
Assertion pilem2 
|- ( ph -> ( ( _pi + A ) / 2 ) <_ B )

Proof

Step Hyp Ref Expression
1 pilem2.1 
 |-  ( ph -> A e. ( 2 (,) 4 ) )
2 pilem2.2 
 |-  ( ph -> B e. RR+ )
3 pilem2.3 
 |-  ( ph -> ( sin ` A ) = 0 )
4 pilem2.4 
 |-  ( ph -> ( sin ` B ) = 0 )
5 df-pi 
 |-  _pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
6 inss1 
 |-  ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR+
7 rpssre 
 |-  RR+ C_ RR
8 6 7 sstri 
 |-  ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR
9 8 a1i 
 |-  ( ph -> ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR )
10 0re 
 |-  0 e. RR
11 elinel1 
 |-  ( y e. ( RR+ i^i ( `' sin " { 0 } ) ) -> y e. RR+ )
12 11 rpge0d 
 |-  ( y e. ( RR+ i^i ( `' sin " { 0 } ) ) -> 0 <_ y )
13 12 rgen 
 |-  A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ y
14 breq1 
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
15 14 ralbidv 
 |-  ( x = 0 -> ( A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y <-> A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ y ) )
16 15 rspcev 
 |-  ( ( 0 e. RR /\ A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) 0 <_ y ) -> E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y )
17 10 13 16 mp2an 
 |-  E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y
18 17 a1i 
 |-  ( ph -> E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y )
19 2re 
 |-  2 e. RR
20 2 rpred 
 |-  ( ph -> B e. RR )
21 remulcl 
 |-  ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
22 19 20 21 sylancr 
 |-  ( ph -> ( 2 x. B ) e. RR )
23 elioore 
 |-  ( A e. ( 2 (,) 4 ) -> A e. RR )
24 1 23 syl 
 |-  ( ph -> A e. RR )
25 22 24 resubcld 
 |-  ( ph -> ( ( 2 x. B ) - A ) e. RR )
26 4re 
 |-  4 e. RR
27 26 a1i 
 |-  ( ph -> 4 e. RR )
28 eliooord 
 |-  ( A e. ( 2 (,) 4 ) -> ( 2 < A /\ A < 4 ) )
29 1 28 syl 
 |-  ( ph -> ( 2 < A /\ A < 4 ) )
30 29 simprd 
 |-  ( ph -> A < 4 )
31 2t2e4 
 |-  ( 2 x. 2 ) = 4
32 19 a1i 
 |-  ( ph -> 2 e. RR )
33 0red 
 |-  ( ph -> 0 e. RR )
34 2pos 
 |-  0 < 2
35 34 a1i 
 |-  ( ph -> 0 < 2 )
36 29 simpld 
 |-  ( ph -> 2 < A )
37 33 32 24 35 36 lttrd 
 |-  ( ph -> 0 < A )
38 24 37 elrpd 
 |-  ( ph -> A e. RR+ )
39 pilem1 
 |-  ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
40 38 3 39 sylanbrc 
 |-  ( ph -> A e. ( RR+ i^i ( `' sin " { 0 } ) ) )
41 40 ne0d 
 |-  ( ph -> ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) )
42 infrecl 
 |-  ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) /\ E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
43 8 17 42 mp3an13 
 |-  ( ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
44 41 43 syl 
 |-  ( ph -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) e. RR )
45 pilem1 
 |-  ( x e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( x e. RR+ /\ ( sin ` x ) = 0 ) )
46 rpre 
 |-  ( x e. RR+ -> x e. RR )
47 46 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
48 letric 
 |-  ( ( 2 e. RR /\ x e. RR ) -> ( 2 <_ x \/ x <_ 2 ) )
49 19 47 48 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 <_ x \/ x <_ 2 ) )
50 49 ord 
 |-  ( ( ph /\ x e. RR+ ) -> ( -. 2 <_ x -> x <_ 2 ) )
51 46 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> x e. RR )
52 rpgt0 
 |-  ( x e. RR+ -> 0 < x )
53 52 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> 0 < x )
54 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> x <_ 2 )
55 0xr 
 |-  0 e. RR*
56 elioc2 
 |-  ( ( 0 e. RR* /\ 2 e. RR ) -> ( x e. ( 0 (,] 2 ) <-> ( x e. RR /\ 0 < x /\ x <_ 2 ) ) )
57 55 19 56 mp2an 
 |-  ( x e. ( 0 (,] 2 ) <-> ( x e. RR /\ 0 < x /\ x <_ 2 ) )
58 51 53 54 57 syl3anbrc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> x e. ( 0 (,] 2 ) )
59 sin02gt0 
 |-  ( x e. ( 0 (,] 2 ) -> 0 < ( sin ` x ) )
60 58 59 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> 0 < ( sin ` x ) )
61 60 gt0ne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ x <_ 2 ) -> ( sin ` x ) =/= 0 )
62 61 ex 
 |-  ( ( ph /\ x e. RR+ ) -> ( x <_ 2 -> ( sin ` x ) =/= 0 ) )
63 50 62 syld 
 |-  ( ( ph /\ x e. RR+ ) -> ( -. 2 <_ x -> ( sin ` x ) =/= 0 ) )
64 63 necon4bd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sin ` x ) = 0 -> 2 <_ x ) )
65 64 expimpd 
 |-  ( ph -> ( ( x e. RR+ /\ ( sin ` x ) = 0 ) -> 2 <_ x ) )
66 45 65 syl5bi 
 |-  ( ph -> ( x e. ( RR+ i^i ( `' sin " { 0 } ) ) -> 2 <_ x ) )
67 66 ralrimiv 
 |-  ( ph -> A. x e. ( RR+ i^i ( `' sin " { 0 } ) ) 2 <_ x )
68 infregelb 
 |-  ( ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ ( RR+ i^i ( `' sin " { 0 } ) ) =/= (/) /\ E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y ) /\ 2 e. RR ) -> ( 2 <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <-> A. x e. ( RR+ i^i ( `' sin " { 0 } ) ) 2 <_ x ) )
69 9 41 18 32 68 syl31anc 
 |-  ( ph -> ( 2 <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <-> A. x e. ( RR+ i^i ( `' sin " { 0 } ) ) 2 <_ x ) )
70 67 69 mpbird 
 |-  ( ph -> 2 <_ inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) )
71 pilem1 
 |-  ( B e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( B e. RR+ /\ ( sin ` B ) = 0 ) )
72 2 4 71 sylanbrc 
 |-  ( ph -> B e. ( RR+ i^i ( `' sin " { 0 } ) ) )
73 infrelb 
 |-  ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y /\ B e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ B )
74 9 18 72 73 syl3anc 
 |-  ( ph -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ B )
75 32 44 20 70 74 letrd 
 |-  ( ph -> 2 <_ B )
76 19 34 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
77 76 a1i 
 |-  ( ph -> ( 2 e. RR /\ 0 < 2 ) )
78 lemul2 
 |-  ( ( 2 e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 2 <_ B <-> ( 2 x. 2 ) <_ ( 2 x. B ) ) )
79 32 20 77 78 syl3anc 
 |-  ( ph -> ( 2 <_ B <-> ( 2 x. 2 ) <_ ( 2 x. B ) ) )
80 75 79 mpbid 
 |-  ( ph -> ( 2 x. 2 ) <_ ( 2 x. B ) )
81 31 80 eqbrtrrid 
 |-  ( ph -> 4 <_ ( 2 x. B ) )
82 24 27 22 30 81 ltletrd 
 |-  ( ph -> A < ( 2 x. B ) )
83 24 22 posdifd 
 |-  ( ph -> ( A < ( 2 x. B ) <-> 0 < ( ( 2 x. B ) - A ) ) )
84 82 83 mpbid 
 |-  ( ph -> 0 < ( ( 2 x. B ) - A ) )
85 25 84 elrpd 
 |-  ( ph -> ( ( 2 x. B ) - A ) e. RR+ )
86 22 recnd 
 |-  ( ph -> ( 2 x. B ) e. CC )
87 24 recnd 
 |-  ( ph -> A e. CC )
88 sinsub 
 |-  ( ( ( 2 x. B ) e. CC /\ A e. CC ) -> ( sin ` ( ( 2 x. B ) - A ) ) = ( ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) - ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) ) )
89 86 87 88 syl2anc 
 |-  ( ph -> ( sin ` ( ( 2 x. B ) - A ) ) = ( ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) - ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) ) )
90 20 recnd 
 |-  ( ph -> B e. CC )
91 sin2t 
 |-  ( B e. CC -> ( sin ` ( 2 x. B ) ) = ( 2 x. ( ( sin ` B ) x. ( cos ` B ) ) ) )
92 90 91 syl 
 |-  ( ph -> ( sin ` ( 2 x. B ) ) = ( 2 x. ( ( sin ` B ) x. ( cos ` B ) ) ) )
93 4 oveq1d 
 |-  ( ph -> ( ( sin ` B ) x. ( cos ` B ) ) = ( 0 x. ( cos ` B ) ) )
94 90 coscld 
 |-  ( ph -> ( cos ` B ) e. CC )
95 94 mul02d 
 |-  ( ph -> ( 0 x. ( cos ` B ) ) = 0 )
96 93 95 eqtrd 
 |-  ( ph -> ( ( sin ` B ) x. ( cos ` B ) ) = 0 )
97 96 oveq2d 
 |-  ( ph -> ( 2 x. ( ( sin ` B ) x. ( cos ` B ) ) ) = ( 2 x. 0 ) )
98 2t0e0 
 |-  ( 2 x. 0 ) = 0
99 97 98 syl6eq 
 |-  ( ph -> ( 2 x. ( ( sin ` B ) x. ( cos ` B ) ) ) = 0 )
100 92 99 eqtrd 
 |-  ( ph -> ( sin ` ( 2 x. B ) ) = 0 )
101 100 oveq1d 
 |-  ( ph -> ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) = ( 0 x. ( cos ` A ) ) )
102 87 coscld 
 |-  ( ph -> ( cos ` A ) e. CC )
103 102 mul02d 
 |-  ( ph -> ( 0 x. ( cos ` A ) ) = 0 )
104 101 103 eqtrd 
 |-  ( ph -> ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) = 0 )
105 3 oveq2d 
 |-  ( ph -> ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) = ( ( cos ` ( 2 x. B ) ) x. 0 ) )
106 86 coscld 
 |-  ( ph -> ( cos ` ( 2 x. B ) ) e. CC )
107 106 mul01d 
 |-  ( ph -> ( ( cos ` ( 2 x. B ) ) x. 0 ) = 0 )
108 105 107 eqtrd 
 |-  ( ph -> ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) = 0 )
109 104 108 oveq12d 
 |-  ( ph -> ( ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) - ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) ) = ( 0 - 0 ) )
110 0m0e0 
 |-  ( 0 - 0 ) = 0
111 109 110 syl6eq 
 |-  ( ph -> ( ( ( sin ` ( 2 x. B ) ) x. ( cos ` A ) ) - ( ( cos ` ( 2 x. B ) ) x. ( sin ` A ) ) ) = 0 )
112 89 111 eqtrd 
 |-  ( ph -> ( sin ` ( ( 2 x. B ) - A ) ) = 0 )
113 pilem1 
 |-  ( ( ( 2 x. B ) - A ) e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( ( ( 2 x. B ) - A ) e. RR+ /\ ( sin ` ( ( 2 x. B ) - A ) ) = 0 ) )
114 85 112 113 sylanbrc 
 |-  ( ph -> ( ( 2 x. B ) - A ) e. ( RR+ i^i ( `' sin " { 0 } ) ) )
115 infrelb 
 |-  ( ( ( RR+ i^i ( `' sin " { 0 } ) ) C_ RR /\ E. x e. RR A. y e. ( RR+ i^i ( `' sin " { 0 } ) ) x <_ y /\ ( ( 2 x. B ) - A ) e. ( RR+ i^i ( `' sin " { 0 } ) ) ) -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ ( ( 2 x. B ) - A ) )
116 9 18 114 115 syl3anc 
 |-  ( ph -> inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < ) <_ ( ( 2 x. B ) - A ) )
117 5 116 eqbrtrid 
 |-  ( ph -> _pi <_ ( ( 2 x. B ) - A ) )
118 5 44 eqeltrid 
 |-  ( ph -> _pi e. RR )
119 leaddsub 
 |-  ( ( _pi e. RR /\ A e. RR /\ ( 2 x. B ) e. RR ) -> ( ( _pi + A ) <_ ( 2 x. B ) <-> _pi <_ ( ( 2 x. B ) - A ) ) )
120 118 24 22 119 syl3anc 
 |-  ( ph -> ( ( _pi + A ) <_ ( 2 x. B ) <-> _pi <_ ( ( 2 x. B ) - A ) ) )
121 117 120 mpbird 
 |-  ( ph -> ( _pi + A ) <_ ( 2 x. B ) )
122 118 24 readdcld 
 |-  ( ph -> ( _pi + A ) e. RR )
123 ledivmul 
 |-  ( ( ( _pi + A ) e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( _pi + A ) / 2 ) <_ B <-> ( _pi + A ) <_ ( 2 x. B ) ) )
124 122 20 77 123 syl3anc 
 |-  ( ph -> ( ( ( _pi + A ) / 2 ) <_ B <-> ( _pi + A ) <_ ( 2 x. B ) ) )
125 121 124 mpbird 
 |-  ( ph -> ( ( _pi + A ) / 2 ) <_ B )