Step |
Hyp |
Ref |
Expression |
1 |
|
df-tau |
⊢ τ = inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) |
2 |
|
inss1 |
⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ+ |
3 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
4 |
2 3
|
sstri |
⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ |
5 |
|
taupilemrplb |
⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦 |
6 |
|
2rp |
⊢ 2 ∈ ℝ+ |
7 |
|
pirp |
⊢ π ∈ ℝ+ |
8 |
|
rpmulcl |
⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ ) |
9 |
6 7 8
|
mp2an |
⊢ ( 2 · π ) ∈ ℝ+ |
10 |
|
cos2pi |
⊢ ( cos ‘ ( 2 · π ) ) = 1 |
11 |
|
taupilem3 |
⊢ ( ( 2 · π ) ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( ( 2 · π ) ∈ ℝ+ ∧ ( cos ‘ ( 2 · π ) ) = 1 ) ) |
12 |
9 10 11
|
mpbir2an |
⊢ ( 2 · π ) ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) |
13 |
|
infrelb |
⊢ ( ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦 ∧ ( 2 · π ) ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ) → inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ≤ ( 2 · π ) ) |
14 |
4 5 12 13
|
mp3an |
⊢ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ≤ ( 2 · π ) |
15 |
1 14
|
eqbrtri |
⊢ τ ≤ ( 2 · π ) |