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 + cos A = 1 2 π A

Proof

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