Metamath Proof Explorer


Theorem cosq34lt1

Description: Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024)

Ref Expression
Assertion cosq34lt1 Aπ2πcosA<1

Proof

Step Hyp Ref Expression
1 pire π
2 2re 2
3 2 1 remulcli 2π
4 3 rexri 2π*
5 elico2 π2π*Aπ2πAπAA<2π
6 1 4 5 mp2an Aπ2πAπAA<2π
7 6 simp1bi Aπ2πA
8 0red Aπ2π0
9 1 a1i Aπ2ππ
10 pipos 0<π
11 10 a1i Aπ2π0<π
12 6 simp2bi Aπ2ππA
13 8 9 7 11 12 ltletrd Aπ2π0<A
14 6 simp3bi Aπ2πA<2π
15 0xr 0*
16 elioo2 0*2π*A02πA0<AA<2π
17 15 4 16 mp2an A02πA0<AA<2π
18 7 13 14 17 syl3anbrc Aπ2πA02π
19 cos02pilt1 A02πcosA<1
20 18 19 syl Aπ2πcosA<1