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 eqtrdi
 |-  ( 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 eqtrdi
 |-  ( 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 )