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 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℝ+ ∩ ( ◡ 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 ) ≤ 𝐵 )