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 τ 2 π

Proof

Step Hyp Ref Expression
1 df-tau τ = sup + cos -1 1 <
2 inss1 + cos -1 1 +
3 rpssre +
4 2 3 sstri + cos -1 1
5 taupilemrplb x y + cos -1 1 x y
6 2rp 2 +
7 pirp π +
8 rpmulcl 2 + π + 2 π +
9 6 7 8 mp2an 2 π +
10 cos2pi cos 2 π = 1
11 taupilem3 2 π + cos -1 1 2 π + cos 2 π = 1
12 9 10 11 mpbir2an 2 π + cos -1 1
13 infrelb + cos -1 1 x y + cos -1 1 x y 2 π + cos -1 1 sup + cos -1 1 < 2 π
14 4 5 12 13 mp3an sup + cos -1 1 < 2 π
15 1 14 eqbrtri τ 2 π