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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rp | |
|
2 | pirp | |
|
3 | rpmulcl | |
|
4 | 1 2 3 | mp2an | |
5 | rpre | |
|
6 | 4 5 | ax-mp | |
7 | 6 | recni | |
8 | rpgt0 | |
|
9 | 4 8 | ax-mp | |
10 | 6 9 | gt0ne0ii | |
11 | 7 10 | dividi | |
12 | rpdivcl | |
|
13 | 12 | rpgt0d | |
14 | 4 13 | mpan2 | |
15 | 14 | adantr | |
16 | rpcn | |
|
17 | coseq1 | |
|
18 | 16 17 | syl | |
19 | 18 | biimpa | |
20 | zgt0ge1 | |
|
21 | 19 20 | syl | |
22 | 15 21 | mpbid | |
23 | 11 22 | eqbrtrid | |
24 | rpre | |
|
25 | 24 | adantr | |
26 | 6 9 | pm3.2i | |
27 | lediv1 | |
|
28 | 6 26 27 | mp3an13 | |
29 | 25 28 | syl | |
30 | 23 29 | mpbird | |