Description: Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | cosq34lt1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pire | |
|
2 | 2re | |
|
3 | 2 1 | remulcli | |
4 | 3 | rexri | |
5 | elico2 | |
|
6 | 1 4 5 | mp2an | |
7 | 6 | simp1bi | |
8 | 0red | |
|
9 | 1 | a1i | |
10 | pipos | |
|
11 | 10 | a1i | |
12 | 6 | simp2bi | |
13 | 8 9 7 11 12 | ltletrd | |
14 | 6 | simp3bi | |
15 | 0xr | |
|
16 | elioo2 | |
|
17 | 15 4 16 | mp2an | |
18 | 7 13 14 17 | syl3anbrc | |
19 | cos02pilt1 | |
|
20 | 18 19 | syl | |