Step | Hyp | Ref
| Expression |
1 | | 0xr 10402 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
2 | | 1re 10355 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | | elioc2 12523 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 685 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1181 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | eqid 2824 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
7 | 6 | resin4p 15239 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
9 | 8 | eqcomd 2830 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴)) |
10 | 5 | resincld 15244 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
11 | 10 | recnd 10384 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℂ) |
12 | | 3nn0 11637 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
13 | | reexpcl 13170 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
14 | 5, 12, 13 | sylancl 582 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
15 | | 6nn 11442 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
16 | | nndivre 11391 |
. . . . . . . . 9
⊢ (((𝐴↑3) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑3) / 6) ∈
ℝ) |
17 | 14, 15, 16 | sylancl 582 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℝ) |
18 | 5, 17 | resubcld 10781 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℝ) |
19 | 18 | recnd 10384 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℂ) |
20 | | ax-icn 10310 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
21 | 5 | recnd 10384 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
22 | | mulcl 10335 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
23 | 20, 21, 22 | sylancr 583 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
24 | | 4nn0 11638 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
25 | 6 | eftlcl 15208 |
. . . . . . . . 9
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
26 | 23, 24, 25 | sylancl 582 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
27 | 26 | imcld 14311 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
28 | 27 | recnd 10384 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
29 | 11, 19, 28 | subaddd 10730 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ↔ ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴))) |
30 | 9, 29 | mpbird 249 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
31 | 30 | fveq2d 6436 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) =
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
32 | 28 | abscld 14551 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
33 | 26 | abscld 14551 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
34 | | absimle 14425 |
. . . . 5
⊢
(Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
35 | 26, 34 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
36 | | reexpcl 13170 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
37 | 5, 24, 36 | sylancl 582 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
38 | | nndivre 11391 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
39 | 37, 15, 38 | sylancl 582 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
40 | 6 | ef01bndlem 15285 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
41 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
ℕ0) |
42 | | 4z 11738 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
43 | | 3re 11430 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
44 | | 4re 11435 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
45 | | 3lt4 11531 |
. . . . . . . . . 10
⊢ 3 <
4 |
46 | 43, 44, 45 | ltleii 10478 |
. . . . . . . . 9
⊢ 3 ≤
4 |
47 | | 3nn 11429 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
48 | 47 | nnzi 11728 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
49 | 48 | eluz1i 11975 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
50 | 42, 46, 49 | mpbir2an 704 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
51 | 50 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘3)) |
52 | 4 | simp2bi 1182 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
53 | | 0re 10357 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
54 | | ltle 10444 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
55 | 53, 5, 54 | sylancr 583 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
56 | 52, 55 | mpd 15 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
57 | 4 | simp3bi 1183 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
58 | 5, 41, 51, 56, 57 | leexp2rd 13337 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑3)) |
59 | | 6re 11443 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
61 | | 6pos 11467 |
. . . . . . . 8
⊢ 0 <
6 |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
63 | | lediv1 11217 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑3) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
64 | 37, 14, 60, 62, 63 | syl112anc 1499 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
65 | 58, 64 | mpbid 224 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6)) |
66 | 33, 39, 17, 40, 65 | ltletrd 10515 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑3) / 6)) |
67 | 32, 33, 17, 35, 66 | lelttrd 10513 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑3) / 6)) |
68 | 31, 67 | eqbrtrd 4894 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6)) |
69 | 10, 18, 17 | absdifltd 14548 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))))) |
70 | 17 | recnd 10384 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℂ) |
71 | 21, 70, 70 | subsub4d 10743 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6)))) |
72 | 14 | recnd 10384 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
73 | | 3cn 11431 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
74 | | 3ne0 11463 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
75 | 73, 74 | pm3.2i 464 |
. . . . . . . . . . . 12
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
76 | | 2cnne0 11567 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
77 | | divdiv1 11061 |
. . . . . . . . . . . 12
⊢ (((𝐴↑3) ∈ ℂ ∧ (3
∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
78 | 75, 76, 77 | mp3an23 1583 |
. . . . . . . . . . 11
⊢ ((𝐴↑3) ∈ ℂ →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
79 | 72, 78 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) / 2) = ((𝐴↑3) / (3 ·
2))) |
80 | | 3t2e6 11523 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
81 | 80 | oveq2i 6915 |
. . . . . . . . . 10
⊢ ((𝐴↑3) / (3 · 2)) =
((𝐴↑3) /
6) |
82 | 79, 81 | syl6req 2877 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) = (((𝐴↑3) / 3) /
2)) |
83 | 82, 82 | oveq12d 6922 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) /
2))) |
84 | | nndivre 11391 |
. . . . . . . . . . 11
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℕ) → ((𝐴↑3) / 3) ∈
ℝ) |
85 | 14, 47, 84 | sylancl 582 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
86 | 85 | recnd 10384 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℂ) |
87 | 86 | 2halvesd 11603 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) / 2)) = ((𝐴↑3) / 3)) |
88 | 83, 87 | eqtrd 2860 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((𝐴↑3) / 3)) |
89 | 88 | oveq2d 6920 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6))) = (𝐴 − ((𝐴↑3) / 3))) |
90 | 71, 89 | eqtrd 2860 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − ((𝐴↑3) / 3))) |
91 | 90 | breq1d 4882 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ↔ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴))) |
92 | 21, 70 | npcand 10716 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) = 𝐴) |
93 | 92 | breq2d 4884 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) ↔ (sin‘𝐴) < 𝐴)) |
94 | 91, 93 | anbi12d 626 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
95 | 69, 94 | bitrd 271 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
96 | 68, 95 | mpbid 224 |
1
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |