Metamath Proof Explorer


Theorem cos01bnd

Description: Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion cos01bnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 0xr 0 ∈ ℝ*
3 elioc2 ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 1 ) ) )
4 2 1 3 mp2an ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 1 ) )
5 4 simp1bi ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ )
6 5 resqcld ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
7 6 rehalfcld ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℝ )
8 resubcl ( ( 1 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℝ ) → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℝ )
9 1 7 8 sylancr ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℝ )
10 9 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℂ )
11 ax-icn i ∈ ℂ
12 5 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℂ )
13 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
14 11 12 13 sylancr ( 𝐴 ∈ ( 0 (,] 1 ) → ( i · 𝐴 ) ∈ ℂ )
15 4nn0 4 ∈ ℕ0
16 eqid ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
17 16 eftlcl ( ( ( i · 𝐴 ) ∈ ℂ ∧ 4 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
18 14 15 17 sylancl ( 𝐴 ∈ ( 0 (,] 1 ) → Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
19 18 recld ( 𝐴 ∈ ( 0 (,] 1 ) → ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℝ )
20 19 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℂ )
21 16 recos4p ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
22 5 21 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( cos ‘ 𝐴 ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
23 10 20 22 mvrladdd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( cos ‘ 𝐴 ) − ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ) = ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
24 23 fveq2d ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ( cos ‘ 𝐴 ) − ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ) ) = ( abs ‘ ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
25 20 abscld ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ∈ ℝ )
26 18 abscld ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℝ )
27 6nn 6 ∈ ℕ
28 nndivre ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) / 6 ) ∈ ℝ )
29 6 27 28 sylancl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 6 ) ∈ ℝ )
30 absrele ( Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
31 18 30 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
32 reexpcl ( ( 𝐴 ∈ ℝ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
33 5 15 32 sylancl ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
34 nndivre ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
35 33 27 34 sylancl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
36 16 ef01bndlem ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 4 ) / 6 ) )
37 2nn0 2 ∈ ℕ0
38 37 a1i ( 𝐴 ∈ ( 0 (,] 1 ) → 2 ∈ ℕ0 )
39 4z 4 ∈ ℤ
40 2re 2 ∈ ℝ
41 4re 4 ∈ ℝ
42 2lt4 2 < 4
43 40 41 42 ltleii 2 ≤ 4
44 2z 2 ∈ ℤ
45 44 eluz1i ( 4 ∈ ( ℤ ‘ 2 ) ↔ ( 4 ∈ ℤ ∧ 2 ≤ 4 ) )
46 39 43 45 mpbir2an 4 ∈ ( ℤ ‘ 2 )
47 46 a1i ( 𝐴 ∈ ( 0 (,] 1 ) → 4 ∈ ( ℤ ‘ 2 ) )
48 4 simp2bi ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 𝐴 )
49 0re 0 ∈ ℝ
50 ltle ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
51 49 5 50 sylancr ( 𝐴 ∈ ( 0 (,] 1 ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
52 48 51 mpd ( 𝐴 ∈ ( 0 (,] 1 ) → 0 ≤ 𝐴 )
53 4 simp3bi ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ≤ 1 )
54 5 38 47 52 53 leexp2rd ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 2 ) )
55 6re 6 ∈ ℝ
56 55 a1i ( 𝐴 ∈ ( 0 (,] 1 ) → 6 ∈ ℝ )
57 6pos 0 < 6
58 57 a1i ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 6 )
59 lediv1 ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℝ ∧ ( 6 ∈ ℝ ∧ 0 < 6 ) ) → ( ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 2 ) ↔ ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 2 ) / 6 ) ) )
60 33 6 56 58 59 syl112anc ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 2 ) ↔ ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 2 ) / 6 ) ) )
61 54 60 mpbid ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 2 ) / 6 ) )
62 26 35 29 36 61 ltletrd ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 2 ) / 6 ) )
63 25 26 29 31 62 lelttrd ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℜ ‘ Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) < ( ( 𝐴 ↑ 2 ) / 6 ) )
64 24 63 eqbrtrd ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ( cos ‘ 𝐴 ) − ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ) ) < ( ( 𝐴 ↑ 2 ) / 6 ) )
65 5 recoscld ( 𝐴 ∈ ( 0 (,] 1 ) → ( cos ‘ 𝐴 ) ∈ ℝ )
66 65 9 29 absdifltd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ ( ( cos ‘ 𝐴 ) − ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ) ) < ( ( 𝐴 ↑ 2 ) / 6 ) ↔ ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) ) ) )
67 1cnd ( 𝐴 ∈ ( 0 (,] 1 ) → 1 ∈ ℂ )
68 7 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ )
69 29 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 6 ) ∈ ℂ )
70 67 68 69 subsub4d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( 1 − ( ( ( 𝐴 ↑ 2 ) / 2 ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) ) )
71 halfpm6th ( ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 ) ∧ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )
72 71 simpri ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
73 72 oveq2i ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) )
74 6 recnd ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
75 2cn 2 ∈ ℂ
76 2ne0 2 ≠ 0
77 75 76 reccli ( 1 / 2 ) ∈ ℂ
78 6cn 6 ∈ ℂ
79 27 nnne0i 6 ≠ 0
80 78 79 reccli ( 1 / 6 ) ∈ ℂ
81 adddi ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
82 77 80 81 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
83 74 82 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
84 73 83 eqtr3id ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
85 3cn 3 ∈ ℂ
86 3ne0 3 ≠ 0
87 85 86 pm3.2i ( 3 ∈ ℂ ∧ 3 ≠ 0 )
88 div12 ( ( 2 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
89 75 87 88 mp3an13 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
90 74 89 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) = ( ( 𝐴 ↑ 2 ) · ( 2 / 3 ) ) )
91 divrec ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / 2 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) )
92 75 76 91 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 2 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) )
93 74 92 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 2 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) )
94 divrec ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / 6 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) )
95 78 79 94 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 6 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) )
96 74 95 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 6 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) )
97 93 96 oveq12d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 2 ) / 2 ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
98 84 90 97 3eqtr4rd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 2 ) / 2 ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) )
99 98 oveq2d ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( ( ( 𝐴 ↑ 2 ) / 2 ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) ) = ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )
100 70 99 eqtrd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )
101 100 breq1d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) < ( cos ‘ 𝐴 ) ↔ ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ) )
102 67 68 69 subsubd ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( ( ( 𝐴 ↑ 2 ) / 2 ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) )
103 71 simpli ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 )
104 103 oveq2i ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) − ( 1 / 6 ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 3 ) )
105 subdi ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) − ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
106 77 80 105 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) − ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
107 74 106 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( ( 1 / 2 ) − ( 1 / 6 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
108 104 107 eqtr3id ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) · ( 1 / 3 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
109 divrec ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / 3 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 3 ) ) )
110 85 86 109 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 3 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 3 ) ) )
111 74 110 syl ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 2 ) / 3 ) = ( ( 𝐴 ↑ 2 ) · ( 1 / 3 ) ) )
112 93 96 oveq12d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 2 ) / 2 ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 1 / 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 1 / 6 ) ) ) )
113 108 111 112 3eqtr4rd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 2 ) / 2 ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( ( 𝐴 ↑ 2 ) / 3 ) )
114 113 oveq2d ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 − ( ( ( 𝐴 ↑ 2 ) / 2 ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) )
115 102 114 eqtr3d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) )
116 115 breq2d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( cos ‘ 𝐴 ) < ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) ↔ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )
117 101 116 anbi12d ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) − ( ( 𝐴 ↑ 2 ) / 6 ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 2 ) / 6 ) ) ) ↔ ( ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ) )
118 66 117 bitrd ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ ( ( cos ‘ 𝐴 ) − ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ) ) < ( ( 𝐴 ↑ 2 ) / 6 ) ↔ ( ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) ) )
119 64 118 mpbid ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 1 − ( 2 · ( ( 𝐴 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < ( 1 − ( ( 𝐴 ↑ 2 ) / 3 ) ) ) )