Metamath Proof Explorer

Theorem taupilem2

Description: Lemma for taupi . The smallest positive real whose cosine is one is at most 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)

Ref Expression
Assertion taupilem2 
|- _tau <_ ( 2 x. _pi )

Proof

Step Hyp Ref Expression
1 df-tau 
 |-  _tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
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 taupilemrplb 
 |-  E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y
6 2rp 
 |-  2 e. RR+
7 pirp 
 |-  _pi e. RR+
8 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
9 6 7 8 mp2an 
 |-  ( 2 x. _pi ) e. RR+
10 cos2pi 
 |-  ( cos ` ( 2 x. _pi ) ) = 1
11 taupilem3 
 |-  ( ( 2 x. _pi ) e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( ( 2 x. _pi ) e. RR+ /\ ( cos ` ( 2 x. _pi ) ) = 1 ) )
12 9 10 11 mpbir2an 
 |-  ( 2 x. _pi ) e. ( RR+ i^i ( `' cos " { 1 } ) )
13 infrelb 
 |-  ( ( ( RR+ i^i ( `' cos " { 1 } ) ) C_ RR /\ E. x e. RR A. y e. ( RR+ i^i ( `' cos " { 1 } ) ) x <_ y /\ ( 2 x. _pi ) e. ( RR+ i^i ( `' cos " { 1 } ) ) ) -> inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) <_ ( 2 x. _pi ) )
14 4 5 12 13 mp3an 
 |-  inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < ) <_ ( 2 x. _pi )
15 1 14 eqbrtri 
 |-  _tau <_ ( 2 x. _pi )