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 
|- _tau = ( 2 x. _pi )

Proof

Step Hyp Ref Expression
1 taupilem2 
 |-  _tau <_ ( 2 x. _pi )
2 inss1 
 |-  ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR+
3 rpssre 
 |-  RR+ C_ RR
4 2 3 sstri 
 |-  ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR
5 2rp 
 |-  2 e. RR+
6 pirp 
 |-  _pi e. RR+
7 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
8 5 6 7 mp2an 
 |-  ( 2 x. _pi ) e. RR+
9 cos2pi 
 |-  ( cos ` ( 2 x. _pi ) ) = 1
10 taupilem3 
 |-  ( ( 2 x. _pi ) e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( ( 2 x. _pi ) e. RR+ /\ ( cos ` ( 2 x. _pi ) ) = 1 ) )
11 8 9 10 mpbir2an 
 |-  ( 2 x. _pi ) e. ( RR+ i^i ( `' cos " { 1 } ) )
12 11 ne0ii 
 |-  ( RR+ i^i ( `' cos " { 1 } ) ) =/= (/)
13 taupilemrplb 
 |-  E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y
14 4 12 13 3pm3.2i 
 |-  ( ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR /\ ( RR+ i^i ( `' cos " { 1 } ) ) =/= (/) /\ E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y )
15 2re 
 |-  2 e. RR
16 pire 
 |-  _pi e. RR
17 15 16 remulcli 
 |-  ( 2 x. _pi ) e. RR
18 infregelb 
 |-  ( ( ( ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR /\ ( RR+ i^i ( `' cos " { 1 } ) ) =/= (/) /\ E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y ) /\ ( 2 x. _pi ) e. RR ) -> ( ( 2 x. _pi ) <_ inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) <-> A. x e. ( RR+ i^i ( `' cos " { 1 } ) ) ( 2 x. _pi ) <_ x ) )
19 14 17 18 mp2an 
 |-  ( ( 2 x. _pi ) <_ inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) <-> A. x e. ( RR+ i^i ( `' cos " { 1 } ) ) ( 2 x. _pi ) <_ x )
20 taupilem3 
 |-  ( x e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( x e. RR+ /\ ( cos ` x ) = 1 ) )
21 taupilem1 
 |-  ( ( x e. RR+ /\ ( cos ` x ) = 1 ) -> ( 2 x. _pi ) <_ x )
22 20 21 sylbi 
 |-  ( x e. ( RR+ i^i ( `' cos " { 1 } ) ) -> ( 2 x. _pi ) <_ x )
23 19 22 mprgbir 
 |-  ( 2 x. _pi ) <_ inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
24 df-tau 
 |-  _tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
25 23 24 breqtrri 
 |-  ( 2 x. _pi ) <_ _tau
26 infrecl 
 |-  ( ( ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR /\ ( RR+ i^i ( `' cos " { 1 } ) ) =/= (/) /\ E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y ) -> inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) e. RR )
27 14 26 ax-mp 
 |-  inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) e. RR
28 24 27 eqeltri 
 |-  _tau e. RR
29 28 17 letri3i 
 |-  ( _tau = ( 2 x. _pi ) <-> ( _tau <_ ( 2 x. _pi ) /\ ( 2 x. _pi ) <_ _tau ) )
30 1 25 29 mpbir2an 
 |-  _tau = ( 2 x. _pi )