Theorem taupi

Description: Relationship between _tau and _pi . This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Assertion	taupi	⊢ τ = ( 2 · π )

Proof

Step	Hyp	Ref	Expression
1		taupilem2	⊢ τ ≤ ( 2 · π )
2		inss1	⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ+
3		rpssre	⊢ ℝ+ ⊆ ℝ
4	2 3	sstri	⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ
5		2rp	⊢ 2 ∈ ℝ+
6		pirp	⊢ π ∈ ℝ+
7		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
8	5 6 7	mp2an	⊢ ( 2 · π ) ∈ ℝ+
9		cos2pi	⊢ ( cos ‘ ( 2 · π ) ) = 1
10		taupilem3	⊢ ( ( 2 · π ) ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( ( 2 · π ) ∈ ℝ+ ∧ ( cos ‘ ( 2 · π ) ) = 1 ) )
11	8 9 10	mpbir2an	⊢ ( 2 · π ) ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) )
12	11	ne0ii	⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ≠ ∅
13		taupilemrplb	⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦
14	4 12 13	3pm3.2i	⊢ ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ ∧ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦 )
15		2re	⊢ 2 ∈ ℝ
16		pire	⊢ π ∈ ℝ
17	15 16	remulcli	⊢ ( 2 · π ) ∈ ℝ
18		infregelb	⊢ ( ( ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ ∧ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦 ) ∧ ( 2 · π ) ∈ ℝ ) → ( ( 2 · π ) ≤ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ↔ ∀ 𝑥 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ( 2 · π ) ≤ 𝑥 ) )
19	14 17 18	mp2an	⊢ ( ( 2 · π ) ≤ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ↔ ∀ 𝑥 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ( 2 · π ) ≤ 𝑥 )
20		taupilem3	⊢ ( 𝑥 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( 𝑥 ∈ ℝ+ ∧ ( cos ‘ 𝑥 ) = 1 ) )
21		taupilem1	⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( cos ‘ 𝑥 ) = 1 ) → ( 2 · π ) ≤ 𝑥 )
22	20 21	sylbi	⊢ ( 𝑥 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) → ( 2 · π ) ≤ 𝑥 )
23	19 22	mprgbir	⊢ ( 2 · π ) ≤ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < )
24		df-tau	⊢ τ = inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < )
25	23 24	breqtrri	⊢ ( 2 · π ) ≤ τ
26		infrecl	⊢ ( ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ⊆ ℝ ∧ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) 𝑥 ≤ 𝑦 ) → inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ∈ ℝ )
27	14 26	ax-mp	⊢ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < ) ∈ ℝ
28	24 27	eqeltri	⊢ τ ∈ ℝ
29	28 17	letri3i	⊢ ( τ = ( 2 · π ) ↔ ( τ ≤ ( 2 · π ) ∧ ( 2 · π ) ≤ τ ) )
30	1 25 29	mpbir2an	⊢ τ = ( 2 · π )