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+cosA=12π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π+A2π+
13 12 rpgt0d A+2π+0<A2π
14 4 13 mpan2 A+0<A2π
15 14 adantr A+cosA=10<A2π
16 rpcn A+A
17 coseq1 AcosA=1A2π
18 16 17 syl A+cosA=1A2π
19 18 biimpa A+cosA=1A2π
20 zgt0ge1 A2π0<A2π1A2π
21 19 20 syl A+cosA=10<A2π1A2π
22 15 21 mpbid A+cosA=11A2π
23 11 22 eqbrtrid A+cosA=12π2πA2π
24 rpre A+A
25 24 adantr A+cosA=1A
26 6 9 pm3.2i 2π0<2π
27 lediv1 2πA2π0<2π2πA2π2πA2π
28 6 26 27 mp3an13 A2πA2π2πA2π
29 25 28 syl A+cosA=12πA2π2πA2π
30 23 29 mpbird A+cosA=12πA