Step | Hyp | Ref
| Expression |
1 | | 0xr 7966 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
2 | | 1re 7919 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | | elioc2 9893 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 424 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1007 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | eqid 2170 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
7 | 6 | resin4p 11681 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
8 | 5, 7 | syl 14 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
9 | 8 | eqcomd 2176 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴)) |
10 | 5 | resincld 11686 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
11 | 10 | recnd 7948 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℂ) |
12 | | 3nn0 9153 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
13 | | reexpcl 10493 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
14 | 5, 12, 13 | sylancl 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
15 | | 6nn 9043 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
16 | | nndivre 8914 |
. . . . . . . . 9
⊢ (((𝐴↑3) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑3) / 6) ∈
ℝ) |
17 | 14, 15, 16 | sylancl 411 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℝ) |
18 | 5, 17 | resubcld 8300 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℝ) |
19 | 18 | recnd 7948 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℂ) |
20 | | ax-icn 7869 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
21 | 5 | recnd 7948 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
22 | | mulcl 7901 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
23 | 20, 21, 22 | sylancr 412 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
24 | | 4nn0 9154 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
25 | 6 | eftlcl 11651 |
. . . . . . . . 9
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
26 | 23, 24, 25 | sylancl 411 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
27 | 26 | imcld 10903 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
28 | 27 | recnd 7948 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
29 | 11, 19, 28 | subaddd 8248 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ↔ ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴))) |
30 | 9, 29 | mpbird 166 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
31 | 30 | fveq2d 5500 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) =
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
32 | 28 | abscld 11145 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
33 | 26 | abscld 11145 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
34 | | absimle 11048 |
. . . . 5
⊢
(Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
35 | 26, 34 | syl 14 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
36 | | reexpcl 10493 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
37 | 5, 24, 36 | sylancl 411 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
38 | | nndivre 8914 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
39 | 37, 15, 38 | sylancl 411 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
40 | 6 | ef01bndlem 11719 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
41 | 12 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
ℕ0) |
42 | | 4z 9242 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
43 | | 3re 8952 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
44 | | 4re 8955 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
45 | | 3lt4 9050 |
. . . . . . . . . 10
⊢ 3 <
4 |
46 | 43, 44, 45 | ltleii 8022 |
. . . . . . . . 9
⊢ 3 ≤
4 |
47 | | 3z 9241 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
48 | 47 | eluz1i 9494 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
49 | 42, 46, 48 | mpbir2an 937 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
50 | 49 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘3)) |
51 | 4 | simp2bi 1008 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
52 | | 0re 7920 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
53 | | ltle 8007 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
54 | 52, 5, 53 | sylancr 412 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
55 | 51, 54 | mpd 13 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
56 | 4 | simp3bi 1009 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
57 | 5, 41, 50, 55, 56 | leexp2rd 10639 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑3)) |
58 | | 6re 8959 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
59 | 58 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
60 | | 6pos 8979 |
. . . . . . . 8
⊢ 0 <
6 |
61 | 60 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
62 | | lediv1 8785 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑3) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
63 | 37, 14, 59, 61, 62 | syl112anc 1237 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
64 | 57, 63 | mpbid 146 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6)) |
65 | 33, 39, 17, 40, 64 | ltletrd 8342 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑3) / 6)) |
66 | 32, 33, 17, 35, 65 | lelttrd 8044 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑3) / 6)) |
67 | 31, 66 | eqbrtrd 4011 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6)) |
68 | 10, 18, 17 | absdifltd 11142 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))))) |
69 | 17 | recnd 7948 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℂ) |
70 | 21, 69, 69 | subsub4d 8261 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6)))) |
71 | 14 | recnd 7948 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
72 | | 3cn 8953 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
73 | | 3ap0 8974 |
. . . . . . . . . . . . 13
⊢ 3 #
0 |
74 | 72, 73 | pm3.2i 270 |
. . . . . . . . . . . 12
⊢ (3 ∈
ℂ ∧ 3 # 0) |
75 | | 2cn 8949 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
76 | | 2ap0 8971 |
. . . . . . . . . . . . 13
⊢ 2 #
0 |
77 | 75, 76 | pm3.2i 270 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 # 0) |
78 | | divdivap1 8640 |
. . . . . . . . . . . 12
⊢ (((𝐴↑3) ∈ ℂ ∧ (3
∈ ℂ ∧ 3 # 0) ∧ (2 ∈ ℂ ∧ 2 # 0)) →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
79 | 74, 77, 78 | mp3an23 1324 |
. . . . . . . . . . 11
⊢ ((𝐴↑3) ∈ ℂ →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
80 | 71, 79 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) / 2) = ((𝐴↑3) / (3 ·
2))) |
81 | | 3t2e6 9034 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
82 | 81 | oveq2i 5864 |
. . . . . . . . . 10
⊢ ((𝐴↑3) / (3 · 2)) =
((𝐴↑3) /
6) |
83 | 80, 82 | eqtr2di 2220 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) = (((𝐴↑3) / 3) /
2)) |
84 | 83, 83 | oveq12d 5871 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) /
2))) |
85 | | 3nn 9040 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
86 | | nndivre 8914 |
. . . . . . . . . . 11
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℕ) → ((𝐴↑3) / 3) ∈
ℝ) |
87 | 14, 85, 86 | sylancl 411 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
88 | 87 | recnd 7948 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℂ) |
89 | 88 | 2halvesd 9123 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) / 2)) = ((𝐴↑3) / 3)) |
90 | 84, 89 | eqtrd 2203 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((𝐴↑3) / 3)) |
91 | 90 | oveq2d 5869 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6))) = (𝐴 − ((𝐴↑3) / 3))) |
92 | 70, 91 | eqtrd 2203 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − ((𝐴↑3) / 3))) |
93 | 92 | breq1d 3999 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ↔ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴))) |
94 | 21, 69 | npcand 8234 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) = 𝐴) |
95 | 94 | breq2d 4001 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) ↔ (sin‘𝐴) < 𝐴)) |
96 | 93, 95 | anbi12d 470 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
97 | 68, 96 | bitrd 187 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
98 | 67, 97 | mpbid 146 |
1
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |