Metamath Proof Explorer

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