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