Metamath Proof Explorer

Theorem cos01gt0

Description: The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion cos01gt0 
|- ( A e. ( 0 (,] 1 ) -> 0 < ( cos ` A ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1re 
 |-  1 e. RR
3 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) ) )
4 1 2 3 mp2an 
 |-  ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
5 4 simp1bi 
 |-  ( A e. ( 0 (,] 1 ) -> A e. RR )
6 5 resqcld 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) e. RR )
7 6 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) e. CC )
8 2cn 
 |-  2 e. CC
9 3cn 
 |-  3 e. CC
10 3ne0 
 |-  3 =/= 0
11 9 10 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
12 div12 
 |-  ( ( 2 e. CC /\ ( A ^ 2 ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
13 8 11 12 mp3an13 
 |-  ( ( A ^ 2 ) e. CC -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
14 7 13 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
15 2z 
 |-  2 e. ZZ
16 expgt0 
 |-  ( ( A e. RR /\ 2 e. ZZ /\ 0 < A ) -> 0 < ( A ^ 2 ) )
17 15 16 mp3an2 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( A ^ 2 ) )
18 17 3adant3 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 1 ) -> 0 < ( A ^ 2 ) )
19 4 18 sylbi 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( A ^ 2 ) )
20 2lt3 
 |-  2 < 3
21 2re 
 |-  2 e. RR
22 3re 
 |-  3 e. RR
23 3pos 
 |-  0 < 3
24 21 22 22 23 ltdiv1ii 
 |-  ( 2 < 3 <-> ( 2 / 3 ) < ( 3 / 3 ) )
25 20 24 mpbi 
 |-  ( 2 / 3 ) < ( 3 / 3 )
26 9 10 dividi 
 |-  ( 3 / 3 ) = 1
27 25 26 breqtri 
 |-  ( 2 / 3 ) < 1
28 21 22 10 redivcli 
 |-  ( 2 / 3 ) e. RR
29 ltmul2 
 |-  ( ( ( 2 / 3 ) e. RR /\ 1 e. RR /\ ( ( A ^ 2 ) e. RR /\ 0 < ( A ^ 2 ) ) ) -> ( ( 2 / 3 ) < 1 <-> ( ( A ^ 2 ) x. ( 2 / 3 ) ) < ( ( A ^ 2 ) x. 1 ) ) )
30 28 2 29 mp3an12 
 |-  ( ( ( A ^ 2 ) e. RR /\ 0 < ( A ^ 2 ) ) -> ( ( 2 / 3 ) < 1 <-> ( ( A ^ 2 ) x. ( 2 / 3 ) ) < ( ( A ^ 2 ) x. 1 ) ) )
31 27 30 mpbii 
 |-  ( ( ( A ^ 2 ) e. RR /\ 0 < ( A ^ 2 ) ) -> ( ( A ^ 2 ) x. ( 2 / 3 ) ) < ( ( A ^ 2 ) x. 1 ) )
32 6 19 31 syl2anc 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( 2 / 3 ) ) < ( ( A ^ 2 ) x. 1 ) )
33 7 mulid1d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. 1 ) = ( A ^ 2 ) )
34 32 33 breqtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( 2 / 3 ) ) < ( A ^ 2 ) )
35 14 34 eqbrtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) < ( A ^ 2 ) )
36 0re 
 |-  0 e. RR
37 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
38 36 37 mpan 
 |-  ( A e. RR -> ( 0 < A -> 0 <_ A ) )
39 38 imdistani 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. RR /\ 0 <_ A ) )
40 le2sq2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( 1 e. RR /\ A <_ 1 ) ) -> ( A ^ 2 ) <_ ( 1 ^ 2 ) )
41 2 40 mpanr1 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ A <_ 1 ) -> ( A ^ 2 ) <_ ( 1 ^ 2 ) )
42 39 41 stoic3 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 1 ) -> ( A ^ 2 ) <_ ( 1 ^ 2 ) )
43 4 42 sylbi 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) <_ ( 1 ^ 2 ) )
44 sq1 
 |-  ( 1 ^ 2 ) = 1
45 43 44 breqtrdi 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) <_ 1 )
46 redivcl 
 |-  ( ( ( A ^ 2 ) e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( ( A ^ 2 ) / 3 ) e. RR )
47 22 10 46 mp3an23 
 |-  ( ( A ^ 2 ) e. RR -> ( ( A ^ 2 ) / 3 ) e. RR )
48 6 47 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 3 ) e. RR )
49 remulcl 
 |-  ( ( 2 e. RR /\ ( ( A ^ 2 ) / 3 ) e. RR ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR )
50 21 48 49 sylancr 
 |-  ( A e. ( 0 (,] 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR )
51 ltletr 
 |-  ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR /\ ( A ^ 2 ) e. RR /\ 1 e. RR ) -> ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) < ( A ^ 2 ) /\ ( A ^ 2 ) <_ 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 ) )
52 2 51 mp3an3 
 |-  ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR /\ ( A ^ 2 ) e. RR ) -> ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) < ( A ^ 2 ) /\ ( A ^ 2 ) <_ 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 ) )
53 50 6 52 syl2anc 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) < ( A ^ 2 ) /\ ( A ^ 2 ) <_ 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 ) )
54 35 45 53 mp2and 
 |-  ( A e. ( 0 (,] 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 )
55 posdif 
 |-  ( ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR /\ 1 e. RR ) -> ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 <-> 0 < ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) ) )
56 50 2 55 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 2 x. ( ( A ^ 2 ) / 3 ) ) < 1 <-> 0 < ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) ) )
57 54 56 mpbid 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) )
58 cos01bnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )
59 58 simpld 
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) )
60 resubcl 
 |-  ( ( 1 e. RR /\ ( 2 x. ( ( A ^ 2 ) / 3 ) ) e. RR ) -> ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) e. RR )
61 2 50 60 sylancr 
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) e. RR )
62 5 recoscld 
 |-  ( A e. ( 0 (,] 1 ) -> ( cos ` A ) e. RR )
63 lttr 
 |-  ( ( 0 e. RR /\ ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) e. RR /\ ( cos ` A ) e. RR ) -> ( ( 0 < ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) /\ ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) ) -> 0 < ( cos ` A ) ) )
64 36 61 62 63 mp3an2i 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 0 < ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) /\ ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) ) -> 0 < ( cos ` A ) ) )
65 57 59 64 mp2and 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( cos ` A ) )