Metamath Proof Explorer


Theorem cosq14gt0

Description: The cosine of a number strictly between -upi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion cosq14gt0 A π 2 π 2 0 < cos A

Proof

Step Hyp Ref Expression
1 halfpire π 2
2 elioore A π 2 π 2 A
3 resubcl π 2 A π 2 A
4 1 2 3 sylancr A π 2 π 2 π 2 A
5 neghalfpirx π 2 *
6 1 rexri π 2 *
7 elioo2 π 2 * π 2 * A π 2 π 2 A π 2 < A A < π 2
8 5 6 7 mp2an A π 2 π 2 A π 2 < A A < π 2
9 8 simp3bi A π 2 π 2 A < π 2
10 posdif A π 2 A < π 2 0 < π 2 A
11 2 1 10 sylancl A π 2 π 2 A < π 2 0 < π 2 A
12 9 11 mpbid A π 2 π 2 0 < π 2 A
13 picn π
14 halfcl π π 2
15 13 14 ax-mp π 2
16 15 negcli π 2
17 13 15 negsubi π + π 2 = π π 2
18 pidiv2halves π 2 + π 2 = π
19 13 15 15 18 subaddrii π π 2 = π 2
20 17 19 eqtri π + π 2 = π 2
21 15 13 16 20 subaddrii π 2 π = π 2
22 8 simp2bi A π 2 π 2 π 2 < A
23 21 22 eqbrtrid A π 2 π 2 π 2 π < A
24 pire π
25 ltsub23 π 2 A π π 2 A < π π 2 π < A
26 1 24 25 mp3an13 A π 2 A < π π 2 π < A
27 2 26 syl A π 2 π 2 π 2 A < π π 2 π < A
28 23 27 mpbird A π 2 π 2 π 2 A < π
29 0xr 0 *
30 24 rexri π *
31 elioo2 0 * π * π 2 A 0 π π 2 A 0 < π 2 A π 2 A < π
32 29 30 31 mp2an π 2 A 0 π π 2 A 0 < π 2 A π 2 A < π
33 4 12 28 32 syl3anbrc A π 2 π 2 π 2 A 0 π
34 sinq12gt0 π 2 A 0 π 0 < sin π 2 A
35 33 34 syl A π 2 π 2 0 < sin π 2 A
36 2 recnd A π 2 π 2 A
37 sinhalfpim A sin π 2 A = cos A
38 36 37 syl A π 2 π 2 sin π 2 A = cos A
39 35 38 breqtrd A π 2 π 2 0 < cos A