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	$⊢ A \in (0, 1] \to (1 - 2 (\frac{A^{2}}{3}) < \cos A \land \cos A < 1 - (\frac{A^{2}}{3}))$

Proof

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

Metamath Proof Explorer

Theorem cos01bnd

Proof