| Step | Hyp | Ref
| Expression |
| 1 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 2 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 3 | | elioc2 13450 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
| 4 | 2, 1, 3 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
| 5 | 4 | simp1bi 1146 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
| 6 | 5 | resqcld 14165 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℝ) |
| 7 | 6 | rehalfcld 12513 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℝ) |
| 8 | | resubcl 11573 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ ((𝐴↑2) / 2) ∈ ℝ) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
| 9 | 1, 7, 8 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
| 10 | 9 | recnd 11289 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℂ) |
| 11 | | ax-icn 11214 |
. . . . . . . . 9
⊢ i ∈
ℂ |
| 12 | 5 | recnd 11289 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
| 13 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 14 | 11, 12, 13 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
| 15 | | 4nn0 12545 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
| 16 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
| 17 | 16 | eftlcl 16143 |
. . . . . . . 8
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
| 18 | 14, 15, 17 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
| 19 | 18 | recld 15233 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
| 20 | 19 | recnd 11289 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
| 21 | 16 | recos4p 16175 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) = ((1 −
((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
| 22 | 5, 21 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) = ((1 −
((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
| 23 | 10, 20, 22 | mvrladdd 11676 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) − (1
− ((𝐴↑2) / 2)))
= (ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 24 | 23 | fveq2d 6910 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) =
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
| 25 | 20 | abscld 15475 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
| 26 | 18 | abscld 15475 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
| 27 | | 6nn 12355 |
. . . . 5
⊢ 6 ∈
ℕ |
| 28 | | nndivre 12307 |
. . . . 5
⊢ (((𝐴↑2) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑2) / 6) ∈
ℝ) |
| 29 | 6, 27, 28 | sylancl 586 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℝ) |
| 30 | | absrele 15347 |
. . . . 5
⊢
(Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 31 | 18, 30 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 32 | | reexpcl 14119 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
| 33 | 5, 15, 32 | sylancl 586 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
| 34 | | nndivre 12307 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
| 35 | 33, 27, 34 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
| 36 | 16 | ef01bndlem 16220 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
| 37 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 38 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 2 ∈
ℕ0) |
| 39 | | 4z 12651 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
| 40 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 41 | | 4re 12350 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
| 42 | | 2lt4 12441 |
. . . . . . . . . 10
⊢ 2 <
4 |
| 43 | 40, 41, 42 | ltleii 11384 |
. . . . . . . . 9
⊢ 2 ≤
4 |
| 44 | | 2z 12649 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
| 45 | 44 | eluz1i 12886 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘2) ↔ (4 ∈ ℤ ∧ 2 ≤
4)) |
| 46 | 39, 43, 45 | mpbir2an 711 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘2) |
| 47 | 46 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘2)) |
| 48 | 4 | simp2bi 1147 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
| 49 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 50 | | ltle 11349 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
| 51 | 49, 5, 50 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
| 52 | 48, 51 | mpd 15 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
| 53 | 4 | simp3bi 1148 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
| 54 | 5, 38, 47, 52, 53 | leexp2rd 14294 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑2)) |
| 55 | | 6re 12356 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
| 56 | 55 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
| 57 | | 6pos 12376 |
. . . . . . . 8
⊢ 0 <
6 |
| 58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
| 59 | | lediv1 12133 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑2) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
| 60 | 33, 6, 56, 58, 59 | syl112anc 1376 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
| 61 | 54, 60 | mpbid 232 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6)) |
| 62 | 26, 35, 29, 36, 61 | ltletrd 11421 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑2) / 6)) |
| 63 | 25, 26, 29, 31, 62 | lelttrd 11419 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑2) / 6)) |
| 64 | 24, 63 | eqbrtrd 5165 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6)) |
| 65 | 5 | recoscld 16180 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) ∈
ℝ) |
| 66 | 65, 9, 29 | absdifltd 15472 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ (((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) <
(cos‘𝐴) ∧
(cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) /
6))))) |
| 67 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℂ) |
| 68 | 7 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℂ) |
| 69 | 29 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℂ) |
| 70 | 67, 68, 69 | subsub4d 11651 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (((𝐴↑2) /
2) + ((𝐴↑2) /
6)))) |
| 71 | | halfpm6th 12487 |
. . . . . . . . . . 11
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |
| 72 | 71 | simpri 485 |
. . . . . . . . . 10
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
| 73 | 72 | oveq2i 7442 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2) + (1
/ 6))) = ((𝐴↑2)
· (2 / 3)) |
| 74 | 6 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℂ) |
| 75 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 76 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 77 | 75, 76 | reccli 11997 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
| 78 | | 6cn 12357 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
| 79 | 27 | nnne0i 12306 |
. . . . . . . . . . . 12
⊢ 6 ≠
0 |
| 80 | 78, 79 | reccli 11997 |
. . . . . . . . . . 11
⊢ (1 / 6)
∈ ℂ |
| 81 | | adddi 11244 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) + (1 / 6))) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
| 82 | 77, 80, 81 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) · ((1 /
2) + (1 / 6))) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 /
6)))) |
| 83 | 74, 82 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2) + (1
/ 6))) = (((𝐴↑2)
· (1 / 2)) + ((𝐴↑2) · (1 /
6)))) |
| 84 | 73, 83 | eqtr3id 2791 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
| 85 | | 3cn 12347 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
| 86 | | 3ne0 12372 |
. . . . . . . . . . 11
⊢ 3 ≠
0 |
| 87 | 85, 86 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
| 88 | | div12 11944 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝐴↑2) ∈ ℂ ∧ (3 ∈
ℂ ∧ 3 ≠ 0)) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3))) |
| 89 | 75, 87, 88 | mp3an13 1454 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
(2 · ((𝐴↑2) /
3)) = ((𝐴↑2) ·
(2 / 3))) |
| 90 | 74, 89 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (2
· ((𝐴↑2) / 3))
= ((𝐴↑2) · (2 /
3))) |
| 91 | | divrec 11938 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2))) |
| 92 | 75, 76, 91 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
| 93 | 74, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
| 94 | | divrec 11938 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 ≠ 0) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6))) |
| 95 | 78, 79, 94 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
| 96 | 74, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
| 97 | 93, 96 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2)) +
((𝐴↑2) · (1 /
6)))) |
| 98 | 84, 90, 97 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (2 ·
((𝐴↑2) /
3))) |
| 99 | 98 | oveq2d 7447 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2) +
((𝐴↑2) / 6))) = (1
− (2 · ((𝐴↑2) / 3)))) |
| 100 | 70, 99 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (2 · ((𝐴↑2) / 3)))) |
| 101 | 100 | breq1d 5153 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6))
< (cos‘𝐴) ↔
(1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴))) |
| 102 | 67, 68, 69 | subsubd 11648 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= ((1 − ((𝐴↑2) /
2)) + ((𝐴↑2) /
6))) |
| 103 | 71 | simpli 483 |
. . . . . . . . . 10
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
| 104 | 103 | oveq2i 7442 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2)
− (1 / 6))) = ((𝐴↑2) · (1 / 3)) |
| 105 | | subdi 11696 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) − (1 / 6)))
= (((𝐴↑2) · (1
/ 2)) − ((𝐴↑2)
· (1 / 6)))) |
| 106 | 77, 80, 105 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) · ((1 /
2) − (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 /
6)))) |
| 107 | 74, 106 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2)
− (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 /
6)))) |
| 108 | 104, 107 | eqtr3id 2791 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (1 / 3)) =
(((𝐴↑2) · (1 /
2)) − ((𝐴↑2)
· (1 / 6)))) |
| 109 | | divrec 11938 |
. . . . . . . . . 10
⊢ (((𝐴↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3))) |
| 110 | 85, 86, 109 | mp3an23 1455 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
| 111 | 74, 110 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
| 112 | 93, 96 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2))
− ((𝐴↑2)
· (1 / 6)))) |
| 113 | 108, 111,
112 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = ((𝐴↑2) / 3)) |
| 114 | 113 | oveq2d 7447 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= (1 − ((𝐴↑2) /
3))) |
| 115 | 102, 114 | eqtr3d 2779 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) = (1
− ((𝐴↑2) /
3))) |
| 116 | 115 | breq2d 5155 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) ↔
(cos‘𝐴) < (1
− ((𝐴↑2) /
3)))) |
| 117 | 101, 116 | anbi12d 632 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6))
< (cos‘𝐴) ∧
(cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6))) ↔
((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) /
3))))) |
| 118 | 66, 117 | bitrd 279 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ ((1 − (2 ·
((𝐴↑2) / 3))) <
(cos‘𝐴) ∧
(cos‘𝐴) < (1
− ((𝐴↑2) /
3))))) |
| 119 | 64, 118 | mpbid 232 |
1
⊢ (𝐴 ∈ (0(,]1) → ((1
− (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) /
3)))) |