| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0xr 11309 | . . . . . . . . 9
⊢ 0 ∈
ℝ* | 
| 2 |  | 1re 11262 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 3 |  | elioc2 13451 | . . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) | 
| 4 | 1, 2, 3 | mp2an 692 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) | 
| 5 | 4 | simp1bi 1145 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) | 
| 6 |  | 3nn0 12546 | . . . . . . . . 9
⊢ 3 ∈
ℕ0 | 
| 7 |  | reexpcl 14120 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) | 
| 8 | 5, 6, 7 | sylancl 586 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) | 
| 9 |  | 6nn 12356 | . . . . . . . 8
⊢ 6 ∈
ℕ | 
| 10 |  | nndivre 12308 | . . . . . . . 8
⊢ (((𝐴↑3) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑3) / 6) ∈
ℝ) | 
| 11 | 8, 9, 10 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℝ) | 
| 12 | 5, 11 | resubcld 11692 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℝ) | 
| 13 | 12 | recnd 11290 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 6)) ∈
ℂ) | 
| 14 |  | ax-icn 11215 | . . . . . . . . 9
⊢ i ∈
ℂ | 
| 15 | 5 | recnd 11290 | . . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) | 
| 16 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 17 | 14, 15, 16 | sylancr 587 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) | 
| 18 |  | 4nn0 12547 | . . . . . . . 8
⊢ 4 ∈
ℕ0 | 
| 19 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) | 
| 20 | 19 | eftlcl 16144 | . . . . . . . 8
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) | 
| 21 | 17, 18, 20 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) | 
| 22 | 21 | imcld 15235 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) | 
| 23 | 22 | recnd 11290 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) | 
| 24 | 19 | resin4p 16175 | . . . . . 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 11677 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) −
(𝐴 − ((𝐴↑3) / 6))) =
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) | 
| 27 | 26 | fveq2d 6909 | . . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) =
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) | 
| 28 | 23 | abscld 15476 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) | 
| 29 | 21 | abscld 15476 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) | 
| 30 |  | absimle 15349 | . . . . 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 14120 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) | 
| 33 | 5, 18, 32 | sylancl 586 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) | 
| 34 |  | nndivre 12308 | . . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) | 
| 35 | 33, 9, 34 | sylancl 586 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) | 
| 36 | 19 | ef01bndlem 16221 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) | 
| 37 | 6 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
ℕ0) | 
| 38 |  | 4z 12653 | . . . . . . . . 9
⊢ 4 ∈
ℤ | 
| 39 |  | 3re 12347 | . . . . . . . . . 10
⊢ 3 ∈
ℝ | 
| 40 |  | 4re 12351 | . . . . . . . . . 10
⊢ 4 ∈
ℝ | 
| 41 |  | 3lt4 12441 | . . . . . . . . . 10
⊢ 3 <
4 | 
| 42 | 39, 40, 41 | ltleii 11385 | . . . . . . . . 9
⊢ 3 ≤
4 | 
| 43 |  | 3z 12652 | . . . . . . . . . 10
⊢ 3 ∈
ℤ | 
| 44 | 43 | eluz1i 12887 | . . . . . . . . 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 1146 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) | 
| 48 |  | 0re 11264 | . . . . . . . . 9
⊢ 0 ∈
ℝ | 
| 49 |  | ltle 11350 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) | 
| 50 | 48, 5, 49 | sylancr 587 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) | 
| 51 | 47, 50 | mpd 15 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) | 
| 52 | 4 | simp3bi 1147 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) | 
| 53 | 5, 37, 46, 51, 52 | leexp2rd 14295 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑3)) | 
| 54 |  | 6re 12357 | . . . . . . . 8
⊢ 6 ∈
ℝ | 
| 55 | 54 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) | 
| 56 |  | 6pos 12377 | . . . . . . . 8
⊢ 0 <
6 | 
| 57 | 56 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) | 
| 58 |  | lediv1 12134 | . . . . . . 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 232 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑3) / 6)) | 
| 61 | 29, 35, 11, 36, 60 | ltletrd 11422 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑3) / 6)) | 
| 62 | 28, 29, 11, 31, 61 | lelttrd 11420 | . . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℑ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑3) / 6)) | 
| 63 | 27, 62 | eqbrtrd 5164 | . 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6)) | 
| 64 | 5 | resincld 16180 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) | 
| 65 | 64, 12, 11 | absdifltd 15473 | . . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))))) | 
| 66 | 11 | recnd 11290 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) ∈
ℂ) | 
| 67 | 15, 66, 66 | subsub4d 11652 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6)))) | 
| 68 | 8 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) | 
| 69 |  | 3cn 12348 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℂ | 
| 70 |  | 3ne0 12373 | . . . . . . . . . . . . 13
⊢ 3 ≠
0 | 
| 71 | 69, 70 | pm3.2i 470 | . . . . . . . . . . . 12
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) | 
| 72 |  | 2cnne0 12477 | . . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 73 |  | divdiv1 11979 | . . . . . . . . . . . 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 12433 | . . . . . . . . . . 11
⊢ (3
· 2) = 6 | 
| 77 | 76 | oveq2i 7443 | . . . . . . . . . 10
⊢ ((𝐴↑3) / (3 · 2)) =
((𝐴↑3) /
6) | 
| 78 | 75, 77 | eqtr2di 2793 | . . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 6) = (((𝐴↑3) / 3) /
2)) | 
| 79 | 78, 78 | oveq12d 7450 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) /
2))) | 
| 80 |  | 3nn 12346 | . . . . . . . . . . 11
⊢ 3 ∈
ℕ | 
| 81 |  | nndivre 12308 | . . . . . . . . . . 11
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℕ) → ((𝐴↑3) / 3) ∈
ℝ) | 
| 82 | 8, 80, 81 | sylancl 586 | . . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) | 
| 83 | 82 | recnd 11290 | . . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℂ) | 
| 84 | 83 | 2halvesd 12514 | . . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴↑3) / 3) / 2) + (((𝐴↑3) / 3) / 2)) = ((𝐴↑3) / 3)) | 
| 85 | 79, 84 | eqtrd 2776 | . . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 6) + ((𝐴↑3) / 6)) = ((𝐴↑3) / 3)) | 
| 86 | 85 | oveq2d 7448 | . . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − (((𝐴↑3) / 6) + ((𝐴↑3) / 6))) = (𝐴 − ((𝐴↑3) / 3))) | 
| 87 | 67, 86 | eqtrd 2776 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) = (𝐴 − ((𝐴↑3) / 3))) | 
| 88 | 87 | breq1d 5152 | . . . 4
⊢ (𝐴 ∈ (0(,]1) → (((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ↔ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴))) | 
| 89 | 15, 66 | npcand 11625 | . . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) = 𝐴) | 
| 90 | 89 | breq2d 5154 | . . . 4
⊢ (𝐴 ∈ (0(,]1) →
((sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6)) ↔ (sin‘𝐴) < 𝐴)) | 
| 91 | 88, 90 | anbi12d 632 | . . 3
⊢ (𝐴 ∈ (0(,]1) → ((((𝐴 − ((𝐴↑3) / 6)) − ((𝐴↑3) / 6)) < (sin‘𝐴) ∧ (sin‘𝐴) < ((𝐴 − ((𝐴↑3) / 6)) + ((𝐴↑3) / 6))) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) | 
| 92 | 65, 91 | bitrd 279 | . 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((sin‘𝐴)
− (𝐴 − ((𝐴↑3) / 6)))) < ((𝐴↑3) / 6) ↔ ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴))) | 
| 93 | 63, 92 | mpbid 232 | 1
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |