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 ( π ∈ ( 2 (,) 4 ) ∧ ( sin ‘ π ) = 0 )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
3 4re ⊢ 4 ∈ ℝ
4 3 a1i ⊢ ( ⊤ → 4 ∈ ℝ )
5 0red ⊢ ( ⊤ → 0 ∈ ℝ )
6 2lt4 ⊢ 2 < 4
7 6 a1i ⊢ ( ⊤ → 2 < 4 )
8 iccssre ⊢ ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ ) → ( 2 [,] 4 ) ⊆ ℝ )
9 1 3 8 mp2an ⊢ ( 2 [,] 4 ) ⊆ ℝ
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 9 10 sstri ⊢ ( 2 [,] 4 ) ⊆ ℂ
12 11 a1i ⊢ ( ⊤ → ( 2 [,] 4 ) ⊆ ℂ )
13 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
14 13 a1i ⊢ ( ⊤ → sin ∈ ( ℂ –cn→ ℂ ) )
15 9 sseli ⊢ ( 𝑦 ∈ ( 2 [,] 4 ) → 𝑦 ∈ ℝ )
16 15 resincld ⊢ ( 𝑦 ∈ ( 2 [,] 4 ) → ( sin ‘ 𝑦 ) ∈ ℝ )
17 16 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 2 [,] 4 ) ) → ( sin ‘ 𝑦 ) ∈ ℝ )
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 ⊢ ( ⊤ → ( ( sin ‘ 4 ) < 0 ∧ 0 < ( sin ‘ 2 ) ) )
23 2 4 5 7 12 14 17 22 ivth2 ⊢ ( ⊤ → ∃ 𝑥 ∈ ( 2 (,) 4 ) ( sin ‘ 𝑥 ) = 0 )
24 23 mptru ⊢ ∃ 𝑥 ∈ ( 2 (,) 4 ) ( sin ‘ 𝑥 ) = 0
25 df-pi ⊢ π = inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < )
26 inss1 ⊢ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ+
27 rpssre ⊢ ℝ+ ⊆ ℝ
28 26 27 sstri ⊢ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ
29 0re ⊢ 0 ∈ ℝ
30 26 sseli ⊢ ( 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) → 𝑧 ∈ ℝ+ )
31 30 rpge0d ⊢ ( 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) → 0 ≤ 𝑧 )
32 31 rgen ⊢ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 0 ≤ 𝑧
33 breq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ≤ 𝑧 ↔ 0 ≤ 𝑧 ) )
34 33 ralbidv ⊢ ( 𝑦 = 0 → ( ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 ↔ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 0 ≤ 𝑧 ) )
35 34 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 0 ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 )
36 29 32 35 mp2an ⊢ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧
37 elioore ⊢ ( 𝑥 ∈ ( 2 (,) 4 ) → 𝑥 ∈ ℝ )
38 37 adantr ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ℝ )
39 0red ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 0 ∈ ℝ )
40 1 a1i ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 2 ∈ ℝ )
41 2pos ⊢ 0 < 2
42 41 a1i ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 0 < 2 )
43 eliooord ⊢ ( 𝑥 ∈ ( 2 (,) 4 ) → ( 2 < 𝑥 ∧ 𝑥 < 4 ) )
44 43 simpld ⊢ ( 𝑥 ∈ ( 2 (,) 4 ) → 2 < 𝑥 )
45 44 adantr ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 2 < 𝑥 )
46 39 40 38 42 45 lttrd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 0 < 𝑥 )
47 38 46 elrpd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ℝ+ )
48 simpr ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( sin ‘ 𝑥 ) = 0 )
49 pilem1 ⊢ ( 𝑥 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ↔ ( 𝑥 ∈ ℝ+ ∧ ( sin ‘ 𝑥 ) = 0 ) )
50 47 48 49 sylanbrc ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) )
51 infrelb ⊢ ( ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 ∧ 𝑥 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ≤ 𝑥 )
52 28 36 50 51 mp3an12i ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ≤ 𝑥 )
53 25 52 eqbrtrid ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → π ≤ 𝑥 )
54 simpll ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → 𝑥 ∈ ( 2 (,) 4 ) )
55 pilem1 ⊢ ( 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ↔ ( 𝑦 ∈ ℝ+ ∧ ( sin ‘ 𝑦 ) = 0 ) )
56 55 bilani ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → ( 𝑦 ∈ ℝ+ ∧ ( sin ‘ 𝑦 ) = 0 ) )
57 56 simpld ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → 𝑦 ∈ ℝ+ )
58 simplr ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → ( sin ‘ 𝑥 ) = 0 )
59 56 simprd ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → ( sin ‘ 𝑦 ) = 0 )
60 54 57 58 59 pilem2 ⊢ ( ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) ∧ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ) → ( ( π + 𝑥 ) / 2 ) ≤ 𝑦 )
61 60 ralrimiva ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ( ( π + 𝑥 ) / 2 ) ≤ 𝑦 )
62 28 a1i ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ )
63 50 ne0d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ≠ ∅ )
64 36 a1i ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 )
65 infrecl ⊢ ( ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ ∧ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 ) → inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ∈ ℝ )
66 28 36 65 mp3an13 ⊢ ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ≠ ∅ → inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ∈ ℝ )
67 63 66 syl ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ∈ ℝ )
68 25 67 eqeltrid ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → π ∈ ℝ )
69 68 38 readdcld ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( π + 𝑥 ) ∈ ℝ )
70 69 rehalfcld ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( π + 𝑥 ) / 2 ) ∈ ℝ )
71 infregelb ⊢ ( ( ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ⊆ ℝ ∧ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) 𝑦 ≤ 𝑧 ) ∧ ( ( π + 𝑥 ) / 2 ) ∈ ℝ ) → ( ( ( π + 𝑥 ) / 2 ) ≤ inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ↔ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ( ( π + 𝑥 ) / 2 ) ≤ 𝑦 ) )
72 62 63 64 70 71 syl31anc ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( ( π + 𝑥 ) / 2 ) ≤ inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) ↔ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ( ( π + 𝑥 ) / 2 ) ≤ 𝑦 ) )
73 61 72 mpbird ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( π + 𝑥 ) / 2 ) ≤ inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < ) )
74 73 25 breqtrrdi ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( π + 𝑥 ) / 2 ) ≤ π )
75 68 recnd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → π ∈ ℂ )
76 38 recnd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ℂ )
77 75 76 addcomd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( π + 𝑥 ) = ( 𝑥 + π ) )
78 77 oveq1d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( π + 𝑥 ) / 2 ) = ( ( 𝑥 + π ) / 2 ) )
79 78 breq1d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( ( π + 𝑥 ) / 2 ) ≤ π ↔ ( ( 𝑥 + π ) / 2 ) ≤ π ) )
80 avgle2 ⊢ ( ( 𝑥 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝑥 ≤ π ↔ ( ( 𝑥 + π ) / 2 ) ≤ π ) )
81 38 68 80 syl2anc ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( 𝑥 ≤ π ↔ ( ( 𝑥 + π ) / 2 ) ≤ π ) )
82 79 81 bitr4d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( ( ( π + 𝑥 ) / 2 ) ≤ π ↔ 𝑥 ≤ π ) )
83 74 82 mpbid ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ≤ π )
84 68 38 letri3d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( π = 𝑥 ↔ ( π ≤ 𝑥 ∧ 𝑥 ≤ π ) ) )
85 53 83 84 mpbir2and ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → π = 𝑥 )
86 simpl ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ( 2 (,) 4 ) )
87 85 86 eqeltrd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → π ∈ ( 2 (,) 4 ) )
88 85 fveq2d ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( sin ‘ π ) = ( sin ‘ 𝑥 ) )
89 88 48 eqtrd ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( sin ‘ π ) = 0 )
90 87 89 jca ⊢ ( ( 𝑥 ∈ ( 2 (,) 4 ) ∧ ( sin ‘ 𝑥 ) = 0 ) → ( π ∈ ( 2 (,) 4 ) ∧ ( sin ‘ π ) = 0 ) )
91 90 rexlimiva ⊢ ( ∃ 𝑥 ∈ ( 2 (,) 4 ) ( sin ‘ 𝑥 ) = 0 → ( π ∈ ( 2 (,) 4 ) ∧ ( sin ‘ π ) = 0 ) )
92 24 91 ax-mp ⊢ ( π ∈ ( 2 (,) 4 ) ∧ ( sin ‘ π ) = 0 )