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