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 ( 𝜑𝐴 ∈ ( 2 (,) 4 ) )
pilem2.2 ( 𝜑𝐵 ∈ ℝ+ )
pilem2.3 ( 𝜑 → ( sin ‘ 𝐴 ) = 0 )
pilem2.4 ( 𝜑 → ( sin ‘ 𝐵 ) = 0 )
Assertion pilem2 ( 𝜑 → ( ( π + 𝐴 ) / 2 ) ≤ 𝐵 )

Proof

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