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