Metamath Proof Explorer

Theorem taupilem1

Description: Lemma for taupi . A positive real whose cosine is one is at least 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019)

Ref Expression
Assertion taupilem1 
|- ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( 2 x. _pi ) <_ A )

Proof

Step Hyp Ref Expression
1 2rp 
 |-  2 e. RR+
2 pirp 
 |-  _pi e. RR+
3 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
4 1 2 3 mp2an 
 |-  ( 2 x. _pi ) e. RR+
5 rpre 
 |-  ( ( 2 x. _pi ) e. RR+ -> ( 2 x. _pi ) e. RR )
6 4 5 ax-mp 
 |-  ( 2 x. _pi ) e. RR
7 6 recni 
 |-  ( 2 x. _pi ) e. CC
8 rpgt0 
 |-  ( ( 2 x. _pi ) e. RR+ -> 0 < ( 2 x. _pi ) )
9 4 8 ax-mp 
 |-  0 < ( 2 x. _pi )
10 6 9 gt0ne0ii 
 |-  ( 2 x. _pi ) =/= 0
11 7 10 dividi 
 |-  ( ( 2 x. _pi ) / ( 2 x. _pi ) ) = 1
12 rpdivcl 
 |-  ( ( A e. RR+ /\ ( 2 x. _pi ) e. RR+ ) -> ( A / ( 2 x. _pi ) ) e. RR+ )
13 12 rpgt0d 
 |-  ( ( A e. RR+ /\ ( 2 x. _pi ) e. RR+ ) -> 0 < ( A / ( 2 x. _pi ) ) )
14 4 13 mpan2 
 |-  ( A e. RR+ -> 0 < ( A / ( 2 x. _pi ) ) )
15 14 adantr 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> 0 < ( A / ( 2 x. _pi ) ) )
16 rpcn 
 |-  ( A e. RR+ -> A e. CC )
17 coseq1 
 |-  ( A e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
18 16 17 syl 
 |-  ( A e. RR+ -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
19 18 biimpa 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( A / ( 2 x. _pi ) ) e. ZZ )
20 zgt0ge1 
 |-  ( ( A / ( 2 x. _pi ) ) e. ZZ -> ( 0 < ( A / ( 2 x. _pi ) ) <-> 1 <_ ( A / ( 2 x. _pi ) ) ) )
21 19 20 syl 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( 0 < ( A / ( 2 x. _pi ) ) <-> 1 <_ ( A / ( 2 x. _pi ) ) ) )
22 15 21 mpbid 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> 1 <_ ( A / ( 2 x. _pi ) ) )
23 11 22 eqbrtrid 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( ( 2 x. _pi ) / ( 2 x. _pi ) ) <_ ( A / ( 2 x. _pi ) ) )
24 rpre 
 |-  ( A e. RR+ -> A e. RR )
25 24 adantr 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> A e. RR )
26 6 9 pm3.2i 
 |-  ( ( 2 x. _pi ) e. RR /\ 0 < ( 2 x. _pi ) )
27 lediv1 
 |-  ( ( ( 2 x. _pi ) e. RR /\ A e. RR /\ ( ( 2 x. _pi ) e. RR /\ 0 < ( 2 x. _pi ) ) ) -> ( ( 2 x. _pi ) <_ A <-> ( ( 2 x. _pi ) / ( 2 x. _pi ) ) <_ ( A / ( 2 x. _pi ) ) ) )
28 6 26 27 mp3an13 
 |-  ( A e. RR -> ( ( 2 x. _pi ) <_ A <-> ( ( 2 x. _pi ) / ( 2 x. _pi ) ) <_ ( A / ( 2 x. _pi ) ) ) )
29 25 28 syl 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( ( 2 x. _pi ) <_ A <-> ( ( 2 x. _pi ) / ( 2 x. _pi ) ) <_ ( A / ( 2 x. _pi ) ) ) )
30 23 29 mpbird 
 |-  ( ( A e. RR+ /\ ( cos ` A ) = 1 ) -> ( 2 x. _pi ) <_ A )