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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | taupilem2 | |
|
2 | inss1 | |
|
3 | rpssre | |
|
4 | 2 3 | sstri | |
5 | 2rp | |
|
6 | pirp | |
|
7 | rpmulcl | |
|
8 | 5 6 7 | mp2an | |
9 | cos2pi | |
|
10 | taupilem3 | |
|
11 | 8 9 10 | mpbir2an | |
12 | 11 | ne0ii | |
13 | taupilemrplb | |
|
14 | 4 12 13 | 3pm3.2i | |
15 | 2re | |
|
16 | pire | |
|
17 | 15 16 | remulcli | |
18 | infregelb | |
|
19 | 14 17 18 | mp2an | |
20 | taupilem3 | |
|
21 | taupilem1 | |
|
22 | 20 21 | sylbi | |
23 | 19 22 | mprgbir | |
24 | df-tau | |
|
25 | 23 24 | breqtrri | |
26 | infrecl | |
|
27 | 14 26 | ax-mp | |
28 | 24 27 | eqeltri | |
29 | 28 17 | letri3i | |
30 | 1 25 29 | mpbir2an | |