Metamath Proof Explorer


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 1 +
3 rpssre +
4 2 3 sstri + cos -1 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 1 2 π + cos 2 π = 1
11 8 9 10 mpbir2an 2 π + cos -1 1
12 11 ne0ii + cos -1 1
13 taupilemrplb x y + cos -1 1 x y
14 4 12 13 3pm3.2i + cos -1 1 + cos -1 1 x y + cos -1 1 x y
15 2re 2
16 pire π
17 15 16 remulcli 2 π
18 infregelb + cos -1 1 + cos -1 1 x y + cos -1 1 x y 2 π 2 π sup + cos -1 1 < x + cos -1 1 2 π x
19 14 17 18 mp2an 2 π sup + cos -1 1 < x + cos -1 1 2 π x
20 taupilem3 x + cos -1 1 x + cos x = 1
21 taupilem1 x + cos x = 1 2 π x
22 20 21 sylbi x + cos -1 1 2 π x
23 19 22 mprgbir 2 π sup + cos -1 1 <
24 df-tau τ = sup + cos -1 1 <
25 23 24 breqtrri 2 π τ
26 infrecl + cos -1 1 + cos -1 1 x y + cos -1 1 x y sup + cos -1 1 <
27 14 26 ax-mp sup + cos -1 1 <
28 24 27 eqeltri τ
29 28 17 letri3i τ = 2 π τ 2 π 2 π τ
30 1 25 29 mpbir2an τ = 2 π