Theorem 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	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0xr	⊢ 0 ∈ ℝ*
2		1re	⊢ 1 ∈ ℝ
3		elioc2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) )
5	4	simp1bi	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ )
6		3nn0	⊢ 3 ∈ ℕ0
7		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℝ )
8	5 6 7	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ∈ ℝ )
9		6nn	⊢ 6 ∈ ℕ
10		nndivre	⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ )
11	8 9 10	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ )
12	5 11	resubcld	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℝ )
13	12	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℂ )
14		ax-icn	⊢ i ∈ ℂ
15	5	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℂ )
16		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
17	14 15 16	sylancr	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( i · 𝐴 ) ∈ ℂ )
18		4nn0	⊢ 4 ∈ ℕ0
19		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
20	19	eftlcl	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 4 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
21	17 18 20	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
22	21	imcld	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℝ )
23	22	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℂ )
24	19	resin4p	⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
25	5 24	syl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( sin ‘ 𝐴 ) = ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
26	13 23 25	mvrladdd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( sin ‘ 𝐴 ) − ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
27	26	fveq2d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ( sin ‘ 𝐴 ) − ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) = ( abs ‘ ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
28	23	abscld	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ∈ ℝ )
29	21	abscld	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ∈ ℝ )
30		absimle	⊢ ( Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
31	21 30	syl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
32		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
33	5 18 32	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
34		nndivre	⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
35	33 9 34	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
36	19	ef01bndlem	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 4 ) / 6 ) )
37	6	a1i	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 3 ∈ ℕ0 )
38		4z	⊢ 4 ∈ ℤ
39		3re	⊢ 3 ∈ ℝ
40		4re	⊢ 4 ∈ ℝ
41		3lt4	⊢ 3 < 4
42	39 40 41	ltleii	⊢ 3 ≤ 4
43		3z	⊢ 3 ∈ ℤ
44	43	eluz1i	⊢ ( 4 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 4 ∈ ℤ ∧ 3 ≤ 4 ) )
45	38 42 44	mpbir2an	⊢ 4 ∈ ( ℤ≥ ‘ 3 )
46	45	a1i	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 4 ∈ ( ℤ≥ ‘ 3 ) )
47	4	simp2bi	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 𝐴 )
48		0re	⊢ 0 ∈ ℝ
49		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
50	48 5 49	sylancr	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
51	47 50	mpd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 ≤ 𝐴 )
52	4	simp3bi	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ≤ 1 )
53	5 37 46 51 52	leexp2rd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 3 ) )
54		6re	⊢ 6 ∈ ℝ
55	54	a1i	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 6 ∈ ℝ )
56		6pos	⊢ 0 < 6
57	56	a1i	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 6 )
58		lediv1	⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ ( 𝐴 ↑ 3 ) ∈ ℝ ∧ ( 6 ∈ ℝ ∧ 0 < 6 ) ) → ( ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 3 ) ↔ ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 3 ) / 6 ) ) )
59	33 8 55 57 58	syl112anc	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) ≤ ( 𝐴 ↑ 3 ) ↔ ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 3 ) / 6 ) ) )
60	53 59	mpbid	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) ≤ ( ( 𝐴 ↑ 3 ) / 6 ) )
61	29 35 11 36 60	ltletrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 3 ) / 6 ) )
62	28 29 11 31 61	lelttrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ℑ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) < ( ( 𝐴 ↑ 3 ) / 6 ) )
63	27 62	eqbrtrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( ( sin ‘ 𝐴 ) − ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) < ( ( 𝐴 ↑ 3 ) / 6 ) )
64	5	resincld	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( sin ‘ 𝐴 ) ∈ ℝ )
65	64 12 11	absdifltd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ ( ( sin ‘ 𝐴 ) − ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) < ( ( 𝐴 ↑ 3 ) / 6 ) ↔ ( ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) − ( ( 𝐴 ↑ 3 ) / 6 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) )
66	11	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
67	15 66 66	subsub4d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) − ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( ( 𝐴 ↑ 3 ) / 6 ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
68	8	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
69		3cn	⊢ 3 ∈ ℂ
70		3ne0	⊢ 3 ≠ 0
71	69 70	pm3.2i	⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
72		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
73		divdiv1	⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) = ( ( 𝐴 ↑ 3 ) / ( 3 · 2 ) ) )
74	71 72 73	mp3an23	⊢ ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) = ( ( 𝐴 ↑ 3 ) / ( 3 · 2 ) ) )
75	68 74	syl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) = ( ( 𝐴 ↑ 3 ) / ( 3 · 2 ) ) )
76		3t2e6	⊢ ( 3 · 2 ) = 6
77	76	oveq2i	⊢ ( ( 𝐴 ↑ 3 ) / ( 3 · 2 ) ) = ( ( 𝐴 ↑ 3 ) / 6 )
78	75 77	eqtr2di	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 6 ) = ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) )
79	78 78	oveq12d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 3 ) / 6 ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) + ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) ) )
80		3nn	⊢ 3 ∈ ℕ
81		nndivre	⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℝ )
82	8 80 81	sylancl	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℝ )
83	82	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℂ )
84	83	2halvesd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) + ( ( ( 𝐴 ↑ 3 ) / 3 ) / 2 ) ) = ( ( 𝐴 ↑ 3 ) / 3 ) )
85	79 84	eqtrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 3 ) / 6 ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( ( 𝐴 ↑ 3 ) / 3 ) )
86	85	oveq2d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 − ( ( ( 𝐴 ↑ 3 ) / 6 ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) )
87	67 86	eqtrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) − ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) )
88	87	breq1d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) − ( ( 𝐴 ↑ 3 ) / 6 ) ) < ( sin ‘ 𝐴 ) ↔ ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ) )
89	15 66	npcand	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) = 𝐴 )
90	89	breq2d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( sin ‘ 𝐴 ) < ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) ↔ ( sin ‘ 𝐴 ) < 𝐴 ) )
91	88 90	anbi12d	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) − ( ( 𝐴 ↑ 3 ) / 6 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ↔ ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) ) )
92	65 91	bitrd	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ ( ( sin ‘ 𝐴 ) − ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) < ( ( 𝐴 ↑ 3 ) / 6 ) ↔ ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) ) )
93	63 92	mpbid	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) )