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 ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( cos ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 1re ⊢ 1 ∈ ℝ
3 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
4 1 2 3 mp2an ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) )
5 4 simp1bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ )
6 5 resqcld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
7 6 recnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
8 2cn ⊢ 2 ∈ ℂ
9 3cn ⊢ 3 ∈ ℂ
10 3ne0 ⊢ 3 ≠ 0
11 9 10 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
12 div12 ⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
13 8 11 12 mp3an13 ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
14 7 13 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
15 2z ⊢ 2 ∈ ℤ
16 expgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 2 ) )
17 15 16 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 2 ) )
18 17 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) → 0 < ( 𝐴 ↑ 2 ) )
19 4 18 sylbi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( 𝐴 ↑ 2 ) )
20 2lt3 ⊢ 2 < 3
21 2re ⊢ 2 ∈ ℝ
22 3re ⊢ 3 ∈ ℝ
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 ) ∈ ℝ
29 ltmul2 ⊢ ( ( ( 2 / 3 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 2 ) ) ) → ( ( 2 / 3 ) < 1 ↔ ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) < ( ( 𝐴 ↑ 2 ) · 1 ) ) )
30 28 2 29 mp3an12 ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 2 ) ) → ( ( 2 / 3 ) < 1 ↔ ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) < ( ( 𝐴 ↑ 2 ) · 1 ) ) )
31 27 30 mpbii ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 2 ) ) → ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) < ( ( 𝐴 ↑ 2 ) · 1 ) )
32 6 19 31 syl2anc ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) < ( ( 𝐴 ↑ 2 ) · 1 ) )
33 7 mulridd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · 1 ) = ( 𝐴 ↑ 2 ) )
34 32 33 breqtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) < ( 𝐴 ↑ 2 ) )
35 14 34 eqbrtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < ( 𝐴 ↑ 2 ) )
36 0re ⊢ 0 ∈ ℝ
37 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
38 36 37 mpan ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
39 38 imdistani ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
40 le2sq2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 1 ∈ ℝ ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 2 ) ≤ ( 1 ↑ 2 ) )
41 2 40 mpanr1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 2 ) ≤ ( 1 ↑ 2 ) )
42 39 41 stoic3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 2 ) ≤ ( 1 ↑ 2 ) )
43 4 42 sylbi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ≤ ( 1 ↑ 2 ) )
44 sq1 ⊢ ( 1 ↑ 2 ) = 1
45 43 44 breqtrdi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ≤ 1 )
46 redivcl ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / 3 ) ∈ ℝ )
47 22 10 46 mp3an23 ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℝ → ( ( 𝐴 ↑ 2 ) / 3 ) ∈ ℝ )
48 6 47 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 3 ) ∈ ℝ )
49 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) / 3 ) ∈ ℝ ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ )
50 21 48 49 sylancr ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ )
51 ltletr ⊢ ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < ( 𝐴 ↑ 2 ) ∧ ( 𝐴 ↑ 2 ) ≤ 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 ) )
52 2 51 mp3an3 ⊢ ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℝ ) → ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < ( 𝐴 ↑ 2 ) ∧ ( 𝐴 ↑ 2 ) ≤ 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 ) )
53 50 6 52 syl2anc ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < ( 𝐴 ↑ 2 ) ∧ ( 𝐴 ↑ 2 ) ≤ 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 ) )
54 35 45 53 mp2and ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 )
55 posdif ⊢ ( ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 ↔ 0 < ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ) )
56 50 2 55 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) < 1 ↔ 0 < ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ) )
57 54 56 mpbid ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )
58 cos01bnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )
59 58 simpld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) )
60 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ∈ ℝ ) → ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ∈ ℝ )
61 2 50 60 sylancr ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ∈ ℝ )
62 5 recoscld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( cos ‘ 𝐴 ) ∈ ℝ )
63 lttr ⊢ ( ( 0 ∈ ℝ ∧ ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ) → ( ( 0 < ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ∧ ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ) → 0 < ( cos ‘ 𝐴 ) ) )
64 36 61 62 63 mp3an2i ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 0 < ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ∧ ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ) → 0 < ( cos ‘ 𝐴 ) ) )
65 57 59 64 mp2and ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( cos ‘ 𝐴 ) )