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