Step | Hyp | Ref
| Expression |
1 | | 1re 10976 |
. . . . . . 7
⊢ 1 ∈
ℝ |
2 | | 0xr 11023 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
3 | | elioc2 13141 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 2, 1, 3 | mp2an 689 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1144 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | 5 | resqcld 13963 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℝ) |
7 | 6 | rehalfcld 12220 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℝ) |
8 | | resubcl 11285 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ ((𝐴↑2) / 2) ∈ ℝ) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
9 | 1, 7, 8 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
10 | 9 | recnd 11004 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℂ) |
11 | | ax-icn 10931 |
. . . . . . . . 9
⊢ i ∈
ℂ |
12 | 5 | recnd 11004 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
13 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
14 | 11, 12, 13 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
15 | | 4nn0 12252 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
16 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
17 | 16 | eftlcl 15814 |
. . . . . . . 8
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
18 | 14, 15, 17 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
19 | 18 | recld 14903 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
20 | 19 | recnd 11004 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
21 | 16 | recos4p 15846 |
. . . . . 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 11388 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) − (1
− ((𝐴↑2) / 2)))
= (ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
24 | 23 | fveq2d 6775 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) =
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
25 | 20 | abscld 15146 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
26 | 18 | abscld 15146 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
27 | | 6nn 12062 |
. . . . 5
⊢ 6 ∈
ℕ |
28 | | nndivre 12014 |
. . . . 5
⊢ (((𝐴↑2) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑2) / 6) ∈
ℝ) |
29 | 6, 27, 28 | sylancl 586 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℝ) |
30 | | absrele 15018 |
. . . . 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 13797 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
33 | 5, 15, 32 | sylancl 586 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
34 | | nndivre 12014 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
35 | 33, 27, 34 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
36 | 16 | ef01bndlem 15891 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
37 | | 2nn0 12250 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 2 ∈
ℕ0) |
39 | | 4z 12354 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
40 | | 2re 12047 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
41 | | 4re 12057 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
42 | | 2lt4 12148 |
. . . . . . . . . 10
⊢ 2 <
4 |
43 | 40, 41, 42 | ltleii 11098 |
. . . . . . . . 9
⊢ 2 ≤
4 |
44 | | 2z 12352 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
45 | 44 | eluz1i 12589 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘2) ↔ (4 ∈ ℤ ∧ 2 ≤
4)) |
46 | 39, 43, 45 | mpbir2an 708 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘2) |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘2)) |
48 | 4 | simp2bi 1145 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
49 | | 0re 10978 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
50 | | ltle 11064 |
. . . . . . . . 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 1146 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
54 | 5, 38, 47, 52, 53 | leexp2rd 13970 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑2)) |
55 | | 6re 12063 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
56 | 55 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
57 | | 6pos 12083 |
. . . . . . . 8
⊢ 0 <
6 |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
59 | | lediv1 11840 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑2) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
60 | 33, 6, 56, 58, 59 | syl112anc 1373 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
61 | 54, 60 | mpbid 231 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6)) |
62 | 26, 35, 29, 36, 61 | ltletrd 11135 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑2) / 6)) |
63 | 25, 26, 29, 31, 62 | lelttrd 11133 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑2) / 6)) |
64 | 24, 63 | eqbrtrd 5101 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6)) |
65 | 5 | recoscld 15851 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) ∈
ℝ) |
66 | 65, 9, 29 | absdifltd 15143 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ (((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) <
(cos‘𝐴) ∧
(cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) /
6))))) |
67 | | 1cnd 10971 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℂ) |
68 | 7 | recnd 11004 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℂ) |
69 | 29 | recnd 11004 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℂ) |
70 | 67, 68, 69 | subsub4d 11363 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (((𝐴↑2) /
2) + ((𝐴↑2) /
6)))) |
71 | | halfpm6th 12194 |
. . . . . . . . . . 11
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |
72 | 71 | simpri 486 |
. . . . . . . . . 10
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
73 | 72 | oveq2i 7282 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2) + (1
/ 6))) = ((𝐴↑2)
· (2 / 3)) |
74 | 6 | recnd 11004 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℂ) |
75 | | 2cn 12048 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
76 | | 2ne0 12077 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
77 | 75, 76 | reccli 11705 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
78 | | 6cn 12064 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
79 | 27 | nnne0i 12013 |
. . . . . . . . . . . 12
⊢ 6 ≠
0 |
80 | 78, 79 | reccli 11705 |
. . . . . . . . . . 11
⊢ (1 / 6)
∈ ℂ |
81 | | adddi 10961 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) + (1 / 6))) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
82 | 77, 80, 81 | mp3an23 1452 |
. . . . . . . . . 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 2794 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
85 | | 3cn 12054 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
86 | | 3ne0 12079 |
. . . . . . . . . . 11
⊢ 3 ≠
0 |
87 | 85, 86 | pm3.2i 471 |
. . . . . . . . . 10
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
88 | | div12 11655 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝐴↑2) ∈ ℂ ∧ (3 ∈
ℂ ∧ 3 ≠ 0)) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3))) |
89 | 75, 87, 88 | mp3an13 1451 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
(2 · ((𝐴↑2) /
3)) = ((𝐴↑2) ·
(2 / 3))) |
90 | 74, 89 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (2
· ((𝐴↑2) / 3))
= ((𝐴↑2) · (2 /
3))) |
91 | | divrec 11649 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2))) |
92 | 75, 76, 91 | mp3an23 1452 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
93 | 74, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
94 | | divrec 11649 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 ≠ 0) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6))) |
95 | 78, 79, 94 | mp3an23 1452 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
96 | 74, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
97 | 93, 96 | oveq12d 7289 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2)) +
((𝐴↑2) · (1 /
6)))) |
98 | 84, 90, 97 | 3eqtr4rd 2791 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (2 ·
((𝐴↑2) /
3))) |
99 | 98 | oveq2d 7287 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2) +
((𝐴↑2) / 6))) = (1
− (2 · ((𝐴↑2) / 3)))) |
100 | 70, 99 | eqtrd 2780 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (2 · ((𝐴↑2) / 3)))) |
101 | 100 | breq1d 5089 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6))
< (cos‘𝐴) ↔
(1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴))) |
102 | 67, 68, 69 | subsubd 11360 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= ((1 − ((𝐴↑2) /
2)) + ((𝐴↑2) /
6))) |
103 | 71 | simpli 484 |
. . . . . . . . . 10
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
104 | 103 | oveq2i 7282 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2)
− (1 / 6))) = ((𝐴↑2) · (1 / 3)) |
105 | | subdi 11408 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) − (1 / 6)))
= (((𝐴↑2) · (1
/ 2)) − ((𝐴↑2)
· (1 / 6)))) |
106 | 77, 80, 105 | mp3an23 1452 |
. . . . . . . . . 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 2794 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (1 / 3)) =
(((𝐴↑2) · (1 /
2)) − ((𝐴↑2)
· (1 / 6)))) |
109 | | divrec 11649 |
. . . . . . . . . 10
⊢ (((𝐴↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3))) |
110 | 85, 86, 109 | mp3an23 1452 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
111 | 74, 110 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
112 | 93, 96 | oveq12d 7289 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2))
− ((𝐴↑2)
· (1 / 6)))) |
113 | 108, 111,
112 | 3eqtr4rd 2791 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = ((𝐴↑2) / 3)) |
114 | 113 | oveq2d 7287 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= (1 − ((𝐴↑2) /
3))) |
115 | 102, 114 | eqtr3d 2782 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) = (1
− ((𝐴↑2) /
3))) |
116 | 115 | breq2d 5091 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) ↔
(cos‘𝐴) < (1
− ((𝐴↑2) /
3)))) |
117 | 101, 116 | anbi12d 631 |
. . 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 278 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ ((1 − (2 ·
((𝐴↑2) / 3))) <
(cos‘𝐴) ∧
(cos‘𝐴) < (1
− ((𝐴↑2) /
3))))) |
119 | 64, 118 | mpbid 231 |
1
⊢ (𝐴 ∈ (0(,]1) → ((1
− (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) /
3)))) |