Step | Hyp | Ref
| Expression |
1 | | 0xr 7937 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
2 | | 1re 7890 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | | elioc2 9864 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 423 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1001 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | eqid 2164 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
7 | 6 | recos4p 11647 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) = ((1 −
((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
8 | 5, 7 | syl 14 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) = ((1 −
((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
9 | 8 | eqcomd 2170 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (cos‘𝐴)) |
10 | 5 | recoscld 11652 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) ∈
ℝ) |
11 | 10 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(cos‘𝐴) ∈
ℂ) |
12 | 5 | resqcld 10604 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℝ) |
13 | 12 | rehalfcld 9095 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℝ) |
14 | | resubcl 8154 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ ((𝐴↑2) / 2) ∈ ℝ) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
15 | 2, 13, 14 | sylancr 411 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℝ) |
16 | 15 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− ((𝐴↑2) / 2))
∈ ℂ) |
17 | | ax-icn 7840 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
18 | 5 | recnd 7919 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
19 | | mulcl 7872 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
20 | 17, 18, 19 | sylancr 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
21 | | 4nn0 9125 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
22 | 6 | eftlcl 11616 |
. . . . . . . . 9
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
23 | 20, 21, 22 | sylancl 410 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
24 | 23 | recld 10867 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
25 | 24 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ) |
26 | 11, 16, 25 | subaddd 8219 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(((cos‘𝐴) − (1
− ((𝐴↑2) / 2)))
= (ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ↔ ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (cos‘𝐴))) |
27 | 9, 26 | mpbird 166 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) − (1
− ((𝐴↑2) / 2)))
= (ℜ‘Σ𝑘
∈ (ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
28 | 27 | fveq2d 5485 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) =
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))) |
29 | 25 | abscld 11110 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ) |
30 | 23 | abscld 11110 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ) |
31 | | 6nn 9014 |
. . . . 5
⊢ 6 ∈
ℕ |
32 | | nndivre 8885 |
. . . . 5
⊢ (((𝐴↑2) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑2) / 6) ∈
ℝ) |
33 | 12, 31, 32 | sylancl 410 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℝ) |
34 | | absrele 11012 |
. . . . 5
⊢
(Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
35 | 23, 34 | syl 14 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) |
36 | | reexpcl 10463 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
37 | 5, 21, 36 | sylancl 410 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
38 | | nndivre 8885 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
39 | 37, 31, 38 | sylancl 410 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
40 | 6 | ef01bndlem 11684 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6)) |
41 | | 2nn0 9123 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
42 | 41 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 2 ∈
ℕ0) |
43 | | 4z 9213 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
44 | | 2re 8919 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
45 | | 4re 8926 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
46 | | 2lt4 9022 |
. . . . . . . . . 10
⊢ 2 <
4 |
47 | 44, 45, 46 | ltleii 7993 |
. . . . . . . . 9
⊢ 2 ≤
4 |
48 | | 2z 9211 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
49 | 48 | eluz1i 9465 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘2) ↔ (4 ∈ ℤ ∧ 2 ≤
4)) |
50 | 43, 47, 49 | mpbir2an 931 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘2) |
51 | 50 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
(ℤ≥‘2)) |
52 | 4 | simp2bi 1002 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
53 | | 0re 7891 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
54 | | ltle 7978 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
55 | 53, 5, 54 | sylancr 411 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
56 | 52, 55 | mpd 13 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
57 | 4 | simp3bi 1003 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
58 | 5, 42, 51, 56, 57 | leexp2rd 10608 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑2)) |
59 | | 6re 8930 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
60 | 59 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 6 ∈
ℝ) |
61 | | 6pos 8950 |
. . . . . . . 8
⊢ 0 <
6 |
62 | 61 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
6) |
63 | | lediv1 8756 |
. . . . . . 7
⊢ (((𝐴↑4) ∈ ℝ ∧
(𝐴↑2) ∈ ℝ
∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
64 | 37, 12, 60, 62, 63 | syl112anc 1231 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))) |
65 | 58, 64 | mpbid 146 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6)) |
66 | 30, 39, 33, 40, 65 | ltletrd 8313 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑2) / 6)) |
67 | 29, 30, 33, 35, 66 | lelttrd 8015 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(ℜ‘Σ𝑘 ∈
(ℤ≥‘4)((𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑2) / 6)) |
68 | 28, 67 | eqbrtrd 3999 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6)) |
69 | 10, 15, 33 | absdifltd 11107 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ (((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) <
(cos‘𝐴) ∧
(cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) /
6))))) |
70 | | 1cnd 7907 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℂ) |
71 | 13 | recnd 7919 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈
ℂ) |
72 | 33 | recnd 7919 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈
ℂ) |
73 | 70, 71, 72 | subsub4d 8232 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (((𝐴↑2) /
2) + ((𝐴↑2) /
6)))) |
74 | | halfpm6th 9069 |
. . . . . . . . . . 11
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |
75 | 74 | simpri 112 |
. . . . . . . . . 10
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
76 | 75 | oveq2i 5848 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2) + (1
/ 6))) = ((𝐴↑2)
· (2 / 3)) |
77 | 12 | recnd 7919 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈
ℂ) |
78 | | 2cn 8920 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
79 | | 2ap0 8942 |
. . . . . . . . . . . 12
⊢ 2 #
0 |
80 | 78, 79 | recclapi 8630 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
81 | | 6cn 8931 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
82 | 31 | nnap0i 8880 |
. . . . . . . . . . . 12
⊢ 6 #
0 |
83 | 81, 82 | recclapi 8630 |
. . . . . . . . . . 11
⊢ (1 / 6)
∈ ℂ |
84 | | adddi 7877 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) + (1 / 6))) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
85 | 80, 83, 84 | mp3an23 1318 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) · ((1 /
2) + (1 / 6))) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 /
6)))) |
86 | 77, 85 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2) + (1
/ 6))) = (((𝐴↑2)
· (1 / 2)) + ((𝐴↑2) · (1 /
6)))) |
87 | 76, 86 | eqtr3id 2211 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) =
(((𝐴↑2) · (1 /
2)) + ((𝐴↑2) ·
(1 / 6)))) |
88 | | 3cn 8924 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
89 | | 3ap0 8945 |
. . . . . . . . . . 11
⊢ 3 #
0 |
90 | 88, 89 | pm3.2i 270 |
. . . . . . . . . 10
⊢ (3 ∈
ℂ ∧ 3 # 0) |
91 | | div12ap 8582 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝐴↑2) ∈ ℂ ∧ (3 ∈
ℂ ∧ 3 # 0)) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3))) |
92 | 78, 90, 91 | mp3an13 1317 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
(2 · ((𝐴↑2) /
3)) = ((𝐴↑2) ·
(2 / 3))) |
93 | 77, 92 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (2
· ((𝐴↑2) / 3))
= ((𝐴↑2) · (2 /
3))) |
94 | | divrecap 8576 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 # 0) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2))) |
95 | 78, 79, 94 | mp3an23 1318 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
96 | 77, 95 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 /
2))) |
97 | | divrecap 8576 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 # 0) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6))) |
98 | 81, 82, 97 | mp3an23 1318 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
99 | 77, 98 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 /
6))) |
100 | 96, 99 | oveq12d 5855 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2)) +
((𝐴↑2) · (1 /
6)))) |
101 | 87, 93, 100 | 3eqtr4rd 2208 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (2 ·
((𝐴↑2) /
3))) |
102 | 101 | oveq2d 5853 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2) +
((𝐴↑2) / 6))) = (1
− (2 · ((𝐴↑2) / 3)))) |
103 | 73, 102 | eqtrd 2197 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6)) =
(1 − (2 · ((𝐴↑2) / 3)))) |
104 | 103 | breq1d 3987 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6))
< (cos‘𝐴) ↔
(1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴))) |
105 | 70, 71, 72 | subsubd 8229 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= ((1 − ((𝐴↑2) /
2)) + ((𝐴↑2) /
6))) |
106 | 74 | simpli 110 |
. . . . . . . . . 10
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
107 | 106 | oveq2i 5848 |
. . . . . . . . 9
⊢ ((𝐴↑2) · ((1 / 2)
− (1 / 6))) = ((𝐴↑2) · (1 / 3)) |
108 | | subdi 8275 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℂ ∧ (1
/ 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) − (1 / 6)))
= (((𝐴↑2) · (1
/ 2)) − ((𝐴↑2)
· (1 / 6)))) |
109 | 80, 83, 108 | mp3an23 1318 |
. . . . . . . . . 10
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) · ((1 /
2) − (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 /
6)))) |
110 | 77, 109 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2)
− (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 /
6)))) |
111 | 107, 110 | eqtr3id 2211 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (1 / 3)) =
(((𝐴↑2) · (1 /
2)) − ((𝐴↑2)
· (1 / 6)))) |
112 | | divrecap 8576 |
. . . . . . . . . 10
⊢ (((𝐴↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 # 0) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3))) |
113 | 88, 89, 112 | mp3an23 1318 |
. . . . . . . . 9
⊢ ((𝐴↑2) ∈ ℂ →
((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
114 | 77, 113 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 /
3))) |
115 | 96, 99 | oveq12d 5855 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2))
− ((𝐴↑2)
· (1 / 6)))) |
116 | 111, 114,
115 | 3eqtr4rd 2208 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = ((𝐴↑2) / 3)) |
117 | 116 | oveq2d 5853 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
− (((𝐴↑2) / 2)
− ((𝐴↑2) / 6)))
= (1 − ((𝐴↑2) /
3))) |
118 | 105, 117 | eqtr3d 2199 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) = (1
− ((𝐴↑2) /
3))) |
119 | 118 | breq2d 3989 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6)) ↔
(cos‘𝐴) < (1
− ((𝐴↑2) /
3)))) |
120 | 104, 119 | anbi12d 465 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((((1
− ((𝐴↑2) / 2))
− ((𝐴↑2) / 6))
< (cos‘𝐴) ∧
(cos‘𝐴) < ((1
− ((𝐴↑2) / 2)) +
((𝐴↑2) / 6))) ↔
((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) /
3))))) |
121 | 69, 120 | bitrd 187 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
((abs‘((cos‘𝐴)
− (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ ((1 − (2 ·
((𝐴↑2) / 3))) <
(cos‘𝐴) ∧
(cos‘𝐴) < (1
− ((𝐴↑2) /
3))))) |
122 | 68, 121 | mpbid 146 |
1
⊢ (𝐴 ∈ (0(,]1) → ((1
− (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) /
3)))) |