sin01bnd

Description: Bounds on the sine 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	sin01bnd	$⊢ A \in (0, 1] \to (A - (\frac{A^{3}}{3}) < \sin A \land \sin A < A)$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		1re	$⊢ 1 \in ℝ$
3		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (A \in (0, 1] \leftrightarrow (A \in ℝ \land 0 < A \land A \leq 1))$
4	1 2 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		3nn0	$⊢ 3 \in ℕ_{0}$
7		reexpcl	$⊢ (A \in ℝ \land 3 \in ℕ_{0}) \to A^{3} \in ℝ$
8	5 6 7	sylancl	$⊢ A \in (0, 1] \to A^{3} \in ℝ$
9		6nn	$⊢ 6 \in ℕ$
10		nndivre	$⊢ (A^{3} \in ℝ \land 6 \in ℕ) \to \frac{A^{3}}{6} \in ℝ$
11	8 9 10	sylancl	$⊢ A \in (0, 1] \to \frac{A^{3}}{6} \in ℝ$
12	5 11	resubcld	$⊢ A \in (0, 1] \to A - (\frac{A^{3}}{6}) \in ℝ$
13	12	recnd	$⊢ A \in (0, 1] \to A - (\frac{A^{3}}{6}) \in ℂ$
14		ax-icn	$⊢ i \in ℂ$
15	5	recnd	$⊢ A \in (0, 1] \to A \in ℂ$
16		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
17	14 15 16	sylancr	$⊢ A \in (0, 1] \to i A \in ℂ$
18		4nn0	$⊢ 4 \in ℕ_{0}$
19		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!})$
20	19	eftlcl	$⊢ (i A \in ℂ \land 4 \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k) \in ℂ$
21	17 18 20	sylancl	$⊢ A \in (0, 1] \to \sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k) \in ℂ$
22	21	imcld	$⊢ A \in (0, 1] \to ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k)) \in ℝ$
23	22	recnd	$⊢ A \in (0, 1] \to ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k)) \in ℂ$
24	19	resin4p	$⊢ A \in ℝ \to \sin A = A - (\frac{A^{3}}{6}) + ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))$
25	5 24	syl	$⊢ A \in (0, 1] \to \sin A = A - (\frac{A^{3}}{6}) + ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))$
26	13 23 25	mvrladdd	$⊢ A \in (0, 1] \to \sin A - (A - (\frac{A^{3}}{6})) = ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))$
27	26	fveq2d	$⊢ A \in (0, 1] \to \|\sin A - (A - (\frac{A^{3}}{6}))\| = \|ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))\|$
28	23	abscld	$⊢ A \in (0, 1] \to \|ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))\| \in ℝ$
29	21	abscld	$⊢ A \in (0, 1] \to \|\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k)\| \in ℝ$
30		absimle	$⊢ \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	21 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 18 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 9 34	sylancl	$⊢ A \in (0, 1] \to \frac{A^{4}}{6} \in ℝ$
36	19	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	6	a1i	$⊢ A \in (0, 1] \to 3 \in ℕ_{0}$
38		4z	$⊢ 4 \in ℤ$
39		3re	$⊢ 3 \in ℝ$
40		4re	$⊢ 4 \in ℝ$
41		3lt4	$⊢ 3 < 4$
42	39 40 41	ltleii	$⊢ 3 \leq 4$
43		3z	$⊢ 3 \in ℤ$
44	43	eluz1i	$⊢ 4 \in ℤ_{\geq 3} \leftrightarrow (4 \in ℤ \land 3 \leq 4)$
45	38 42 44	mpbir2an	$⊢ 4 \in ℤ_{\geq 3}$
46	45	a1i	$⊢ A \in (0, 1] \to 4 \in ℤ_{\geq 3}$
47	4	simp2bi	$⊢ A \in (0, 1] \to 0 < A$
48		0re	$⊢ 0 \in ℝ$
49		ltle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \to 0 \leq A)$
50	48 5 49	sylancr	$⊢ A \in (0, 1] \to (0 < A \to 0 \leq A)$
51	47 50	mpd	$⊢ A \in (0, 1] \to 0 \leq A$
52	4	simp3bi	$⊢ A \in (0, 1] \to A \leq 1$
53	5 37 46 51 52	leexp2rd	$⊢ A \in (0, 1] \to A^{4} \leq A^{3}$
54		6re	$⊢ 6 \in ℝ$
55	54	a1i	$⊢ A \in (0, 1] \to 6 \in ℝ$
56		6pos	$⊢ 0 < 6$
57	56	a1i	$⊢ A \in (0, 1] \to 0 < 6$
58		lediv1	$⊢ (A^{4} \in ℝ \land A^{3} \in ℝ \land (6 \in ℝ \land 0 < 6)) \to (A^{4} \leq A^{3} \leftrightarrow \frac{A^{4}}{6} \leq \frac{A^{3}}{6})$
59	33 8 55 57 58	syl112anc	$⊢ A \in (0, 1] \to (A^{4} \leq A^{3} \leftrightarrow \frac{A^{4}}{6} \leq \frac{A^{3}}{6})$
60	53 59	mpbid	$⊢ A \in (0, 1] \to \frac{A^{4}}{6} \leq \frac{A^{3}}{6}$
61	29 35 11 36 60	ltletrd	$⊢ A \in (0, 1] \to \|\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k)\| < \frac{A^{3}}{6}$
62	28 29 11 31 61	lelttrd	$⊢ A \in (0, 1] \to \|ℑ (\sum_{k \in ℤ_{\geq 4}} (n \in ℕ_{0} ⟼ \frac{{i A}^{n}}{n!}) (k))\| < \frac{A^{3}}{6}$
63	27 62	eqbrtrd	$⊢ A \in (0, 1] \to \|\sin A - (A - (\frac{A^{3}}{6}))\| < \frac{A^{3}}{6}$
64	5	resincld	$⊢ A \in (0, 1] \to \sin A \in ℝ$
65	64 12 11	absdifltd	$⊢ A \in (0, 1] \to (\|\sin A - (A - (\frac{A^{3}}{6}))\| < \frac{A^{3}}{6} \leftrightarrow (A - (\frac{A^{3}}{6}) - (\frac{A^{3}}{6}) < \sin A \land \sin A < A - (\frac{A^{3}}{6}) + (\frac{A^{3}}{6})))$
66	11	recnd	$⊢ A \in (0, 1] \to \frac{A^{3}}{6} \in ℂ$
67	15 66 66	subsub4d	$⊢ A \in (0, 1] \to A - (\frac{A^{3}}{6}) - (\frac{A^{3}}{6}) = A - ((\frac{A^{3}}{6}) + (\frac{A^{3}}{6}))$
68	8	recnd	$⊢ A \in (0, 1] \to A^{3} \in ℂ$
69		3cn	$⊢ 3 \in ℂ$
70		3ne0	$⊢ 3 \neq 0$
71	69 70	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
72		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
73		divdiv1	$⊢ (A^{3} \in ℂ \land (3 \in ℂ \land 3 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{A^{3}}{3}}{2} = \frac{A^{3}}{3 \cdot 2}$
74	71 72 73	mp3an23	$⊢ A^{3} \in ℂ \to \frac{\frac{A^{3}}{3}}{2} = \frac{A^{3}}{3 \cdot 2}$
75	68 74	syl	$⊢ A \in (0, 1] \to \frac{\frac{A^{3}}{3}}{2} = \frac{A^{3}}{3 \cdot 2}$
76		3t2e6	$⊢ 3 \cdot 2 = 6$
77	76	oveq2i	$⊢ \frac{A^{3}}{3 \cdot 2} = \frac{A^{3}}{6}$
78	75 77	eqtr2di	$⊢ A \in (0, 1] \to \frac{A^{3}}{6} = \frac{\frac{A^{3}}{3}}{2}$
79	78 78	oveq12d	$⊢ A \in (0, 1] \to (\frac{A^{3}}{6}) + (\frac{A^{3}}{6}) = (\frac{\frac{A^{3}}{3}}{2}) + (\frac{\frac{A^{3}}{3}}{2})$
80		3nn	$⊢ 3 \in ℕ$
81		nndivre	$⊢ (A^{3} \in ℝ \land 3 \in ℕ) \to \frac{A^{3}}{3} \in ℝ$
82	8 80 81	sylancl	$⊢ A \in (0, 1] \to \frac{A^{3}}{3} \in ℝ$
83	82	recnd	$⊢ A \in (0, 1] \to \frac{A^{3}}{3} \in ℂ$
84	83	2halvesd	$⊢ A \in (0, 1] \to (\frac{\frac{A^{3}}{3}}{2}) + (\frac{\frac{A^{3}}{3}}{2}) = \frac{A^{3}}{3}$
85	79 84	eqtrd	$⊢ A \in (0, 1] \to (\frac{A^{3}}{6}) + (\frac{A^{3}}{6}) = \frac{A^{3}}{3}$
86	85	oveq2d	$⊢ A \in (0, 1] \to A - ((\frac{A^{3}}{6}) + (\frac{A^{3}}{6})) = A - (\frac{A^{3}}{3})$
87	67 86	eqtrd	$⊢ A \in (0, 1] \to A - (\frac{A^{3}}{6}) - (\frac{A^{3}}{6}) = A - (\frac{A^{3}}{3})$
88	87	breq1d	$⊢ A \in (0, 1] \to (A - (\frac{A^{3}}{6}) - (\frac{A^{3}}{6}) < \sin A \leftrightarrow A - (\frac{A^{3}}{3}) < \sin A)$
89	15 66	npcand	$⊢ A \in (0, 1] \to A - (\frac{A^{3}}{6}) + (\frac{A^{3}}{6}) = A$
90	89	breq2d	$⊢ A \in (0, 1] \to (\sin A < A - (\frac{A^{3}}{6}) + (\frac{A^{3}}{6}) \leftrightarrow \sin A < A)$
91	88 90	anbi12d	$⊢ A \in (0, 1] \to ((A - (\frac{A^{3}}{6}) - (\frac{A^{3}}{6}) < \sin A \land \sin A < A - (\frac{A^{3}}{6}) + (\frac{A^{3}}{6})) \leftrightarrow (A - (\frac{A^{3}}{3}) < \sin A \land \sin A < A))$
92	65 91	bitrd	$⊢ A \in (0, 1] \to (\|\sin A - (A - (\frac{A^{3}}{6}))\| < \frac{A^{3}}{6} \leftrightarrow (A - (\frac{A^{3}}{3}) < \sin A \land \sin A < A))$
93	63 92	mpbid	$⊢ A \in (0, 1] \to (A - (\frac{A^{3}}{3}) < \sin A \land \sin A < A)$

Metamath Proof Explorer

Theorem sin01bnd

Proof