Metamath Proof Explorer


Theorem taupilem2

Description: Lemma for taupi . The smallest positive real whose cosine is one is at most 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)

Ref Expression
Assertion taupilem2 τ ≤ ( 2 · π )

Proof

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 · π )