This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )