Step | Hyp | Ref
| Expression |
1 | | 0xr 9965 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
2 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | | elioc2 12107 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 704 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1069 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
7 | 6 | resin4p 14707 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
9 | 8 | eqcomd 2616 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴)) |
10 | 5 | resincld 14712 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
11 | 10 | recnd 9947 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℂ) |
12 | | 3nn0 11187 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
13 | | reexpcl 12739 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
14 | 5, 12, 13 | sylancl 693 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
15 | | 6nn 11066 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
16 | | nndivre 10933 |
. . . . . . . . 9
⊢ (((𝐴↑3) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑3) / 6) ∈
ℝ) |
17 | 14, 15, 16 | sylancl 693 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℝ) |
18 | 5, 17 | resubcld 10337 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℝ) |
19 | 18 | recnd 9947 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℂ) |
20 | | ax-icn 9874 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
21 | 5 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
22 | | mulcl 9899 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
23 | 20, 21, 22 | sylancr 694 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
24 | | 4nn0 11188 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
25 | 6 | eftlcl 14676 |
. . . . . . . . 9
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
26 | 23, 24, 25 | sylancl 693 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
27 | 26 | imcld 13783 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
28 | 27 | recnd 9947 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
29 | 11, 19, 28 | subaddd 10289 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ↔ ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (sin‘𝐴))) |
30 | 9, 29 | mpbird 246 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
31 | 30 | fveq2d 6107 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) =
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
32 | 28 | abscld 14023 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
33 | 26 | abscld 14023 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
34 | | absimle 13897 |
. . . . 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 12739 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
37 | 5, 24, 36 | sylancl 693 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
38 | | nndivre 10933 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
39 | 37, 15, 38 | sylancl 693 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
40 | 6 | ef01bndlem 14753 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
41 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
ℕ0) |
42 | | 4z 11288 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
43 | | 3re 10971 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
44 | | 4re 10974 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
45 | | 3lt4 11074 |
. . . . . . . . . 10
⊢ 3 <
4 |
46 | 43, 44, 45 | ltleii 10039 |
. . . . . . . . 9
⊢ 3 ≤
4 |
47 | | 3nn 11063 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
48 | 47 | nnzi 11278 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
49 | 48 | eluz1i 11571 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
50 | 42, 46, 49 | mpbir2an 957 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
51 | 50 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘3)) |
52 | 4 | simp2bi 1070 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
53 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
54 | | ltle 10005 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
55 | 53, 5, 54 | sylancr 694 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
56 | 52, 55 | mpd 15 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
57 | 4 | simp3bi 1071 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
58 | 5, 41, 51, 56, 57 | leexp2rd 12904 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑3)) |
59 | | 6re 10978 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
61 | | 6pos 10996 |
. . . . . . . 8
⊢ 0 <
6 |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
63 | | lediv1 10767 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑3) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
64 | 37, 14, 60, 62, 63 | syl112anc 1322 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
65 | 58, 64 | mpbid 221 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6)) |
66 | 33, 39, 17, 40, 65 | ltletrd 10076 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑3) / 6)) |
67 | 32, 33, 17, 35, 66 | lelttrd 10074 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑3) / 6)) |
68 | 31, 67 | eqbrtrd 4605 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6)) |
69 | 10, 18, 17 | absdifltd 14020 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))))) |
70 | 17 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℂ) |
71 | 21, 70, 70 | subsub4d 10302 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6)))) |
72 | 14 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
73 | | 3cn 10972 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
74 | | 3ne0 10992 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
75 | 73, 74 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
76 | | 2cnne0 11119 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
77 | | divdiv1 10615 |
. . . . . . . . . . . 12
⊢ (((𝐴↑3) ∈ ℂ ∧ (3
∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
78 | 75, 76, 77 | mp3an23 1408 |
. . . . . . . . . . 11
⊢ ((𝐴↑3) ∈ ℂ →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
79 | 72, 78 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) / 2) = ((𝐴↑3) / (3 ·
2))) |
80 | | 3t2e6 11056 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
81 | 80 | oveq2i 6560 |
. . . . . . . . . 10
⊢ ((𝐴↑3) / (3 · 2)) =
((𝐴↑3) /
6) |
82 | 79, 81 | syl6req 2661 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) = (((𝐴↑3) / 3) /
2)) |
83 | 82, 82 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) /
2))) |
84 | | nndivre 10933 |
. . . . . . . . . . 11
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℕ) → ((𝐴↑3) / 3) ∈
ℝ) |
85 | 14, 47, 84 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
86 | 85 | recnd 9947 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℂ) |
87 | 86 | 2halvesd 11155 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) / 2)) = ((𝐴↑3) / 3)) |
88 | 83, 87 | eqtrd 2644 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((𝐴↑3) / 3)) |
89 | 88 | oveq2d 6565 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6))) = (𝐴 − ((𝐴↑3) / 3))) |
90 | 71, 89 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − ((𝐴↑3) / 3))) |
91 | 90 | breq1d 4593 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ↔ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴))) |
92 | 21, 70 | npcand 10275 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) = 𝐴) |
93 | 92 | breq2d 4595 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) ↔ (sin‘𝐴) < 𝐴)) |
94 | 91, 93 | anbi12d 743 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
95 | 69, 94 | bitrd 267 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
96 | 68, 95 | mpbid 221 |
1
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |