Step | Hyp | Ref
| Expression |
1 | | 0xr 10767 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
2 | | 1re 10720 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | | elioc2 12885 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 692 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1146 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | 3nn0 11995 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
7 | | reexpcl 13539 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
8 | 5, 6, 7 | sylancl 589 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
9 | | 6nn 11806 |
. . . . . . . 8
⊢ 6 ∈
ℕ |
10 | | nndivre 11758 |
. . . . . . . 8
⊢ (((𝐴↑3) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑3) / 6) ∈
ℝ) |
11 | 8, 9, 10 | sylancl 589 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℝ) |
12 | 5, 11 | resubcld 11147 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℝ) |
13 | 12 | recnd 10748 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℂ) |
14 | | ax-icn 10675 |
. . . . . . . . 9
⊢ i ∈
ℂ |
15 | 5 | recnd 10748 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
16 | | mulcl 10700 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
17 | 14, 15, 16 | sylancr 590 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
18 | | 4nn0 11996 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
19 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
20 | 19 | eftlcl 15553 |
. . . . . . . 8
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
21 | 17, 18, 20 | sylancl 589 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
22 | 21 | imcld 14645 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
23 | 22 | recnd 10748 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
24 | 19 | resin4p 15584 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
25 | 5, 24 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
26 | 13, 23, 25 | mvrladdd 11132 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
27 | 26 | fveq2d 6679 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) =
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
28 | 23 | abscld 14887 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
29 | 21 | abscld 14887 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
30 | | absimle 14760 |
. . . . 5
⊢
(Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
31 | 21, 30 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
32 | | reexpcl 13539 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
33 | 5, 18, 32 | sylancl 589 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
34 | | nndivre 11758 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
35 | 33, 9, 34 | sylancl 589 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
36 | 19 | ef01bndlem 15630 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
37 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
ℕ0) |
38 | | 4z 12098 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
39 | | 3re 11797 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
40 | | 4re 11801 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
41 | | 3lt4 11891 |
. . . . . . . . . 10
⊢ 3 <
4 |
42 | 39, 40, 41 | ltleii 10842 |
. . . . . . . . 9
⊢ 3 ≤
4 |
43 | | 3z 12097 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
44 | 43 | eluz1i 12333 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
45 | 38, 42, 44 | mpbir2an 711 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
46 | 45 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘3)) |
47 | 4 | simp2bi 1147 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
48 | | 0re 10722 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
49 | | ltle 10808 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
50 | 48, 5, 49 | sylancr 590 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
51 | 47, 50 | mpd 15 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
52 | 4 | simp3bi 1148 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
53 | 5, 37, 46, 51, 52 | leexp2rd 13711 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑3)) |
54 | | 6re 11807 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
56 | | 6pos 11827 |
. . . . . . . 8
⊢ 0 <
6 |
57 | 56 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
58 | | lediv1 11584 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑3) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
59 | 33, 8, 55, 57, 58 | syl112anc 1375 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑3) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6))) |
60 | 53, 59 | mpbid 235 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6)) |
61 | 29, 35, 11, 36, 60 | ltletrd 10879 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑3) / 6)) |
62 | 28, 29, 11, 31, 61 | lelttrd 10877 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑3) / 6)) |
63 | 27, 62 | eqbrtrd 5053 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6)) |
64 | 5 | resincld 15589 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
65 | 64, 12, 11 | absdifltd 14884 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))))) |
66 | 11 | recnd 10748 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℂ) |
67 | 15, 66, 66 | subsub4d 11107 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6)))) |
68 | 8 | recnd 10748 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
69 | | 3cn 11798 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
70 | | 3ne0 11823 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
71 | 69, 70 | pm3.2i 474 |
. . . . . . . . . . . 12
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
72 | | 2cnne0 11927 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
73 | | divdiv1 11430 |
. . . . . . . . . . . 12
⊢ (((𝐴↑3) ∈ ℂ ∧ (3
∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
74 | 71, 72, 73 | mp3an23 1454 |
. . . . . . . . . . 11
⊢ ((𝐴↑3) ∈ ℂ →
(((𝐴↑3) / 3) / 2) =
((𝐴↑3) / (3 ·
2))) |
75 | 68, 74 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) / 2) = ((𝐴↑3) / (3 ·
2))) |
76 | | 3t2e6 11883 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
77 | 76 | oveq2i 7182 |
. . . . . . . . . 10
⊢ ((𝐴↑3) / (3 · 2)) =
((𝐴↑3) /
6) |
78 | 75, 77 | eqtr2di 2790 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) = (((𝐴↑3) / 3) /
2)) |
79 | 78, 78 | oveq12d 7189 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) /
2))) |
80 | | 3nn 11796 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
81 | | nndivre 11758 |
. . . . . . . . . . 11
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℕ) → ((𝐴↑3) / 3) ∈
ℝ) |
82 | 8, 80, 81 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
83 | 82 | recnd 10748 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℂ) |
84 | 83 | 2halvesd 11963 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) / 2)) = ((𝐴↑3) / 3)) |
85 | 79, 84 | eqtrd 2773 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((𝐴↑3) / 3)) |
86 | 85 | oveq2d 7187 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6))) = (𝐴 − ((𝐴↑3) / 3))) |
87 | 67, 86 | eqtrd 2773 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − ((𝐴↑3) / 3))) |
88 | 87 | breq1d 5041 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ↔ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴))) |
89 | 15, 66 | npcand 11080 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) = 𝐴) |
90 | 89 | breq2d 5043 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) ↔ (sin‘𝐴) < 𝐴)) |
91 | 88, 90 | anbi12d 634 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
92 | 65, 91 | bitrd 282 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) |
93 | 63, 92 | mpbid 235 |
1
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |