Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cos01bnd GIF version

Theorem cos01bnd 11465
 Description: Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
Assertion
Ref Expression
cos01bnd (𝐴 ∈ (0(,]1) → ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3))))

Proof of Theorem cos01bnd
Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0xr 7812 . . . . . . . . 9 0 ∈ ℝ*
2 1re 7765 . . . . . . . . 9 1 ∈ ℝ
3 elioc2 9719 . . . . . . . . 9 ((0 ∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 1)))
41, 2, 3mp2an 422 . . . . . . . 8 (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 1))
54simp1bi 996 . . . . . . 7 (𝐴 ∈ (0(,]1) → 𝐴 ∈ ℝ)
6 eqid 2139 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))
76recos4p 11426 . . . . . . 7 (𝐴 ∈ ℝ → (cos‘𝐴) = ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))))
85, 7syl 14 . . . . . 6 (𝐴 ∈ (0(,]1) → (cos‘𝐴) = ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))))
98eqcomd 2145 . . . . 5 (𝐴 ∈ (0(,]1) → ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (cos‘𝐴))
105recoscld 11431 . . . . . . 7 (𝐴 ∈ (0(,]1) → (cos‘𝐴) ∈ ℝ)
1110recnd 7794 . . . . . 6 (𝐴 ∈ (0(,]1) → (cos‘𝐴) ∈ ℂ)
125resqcld 10450 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈ ℝ)
1312rehalfcld 8966 . . . . . . . 8 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈ ℝ)
14 resubcl 8026 . . . . . . . 8 ((1 ∈ ℝ ∧ ((𝐴↑2) / 2) ∈ ℝ) → (1 − ((𝐴↑2) / 2)) ∈ ℝ)
152, 13, 14sylancr 410 . . . . . . 7 (𝐴 ∈ (0(,]1) → (1 − ((𝐴↑2) / 2)) ∈ ℝ)
1615recnd 7794 . . . . . 6 (𝐴 ∈ (0(,]1) → (1 − ((𝐴↑2) / 2)) ∈ ℂ)
17 ax-icn 7715 . . . . . . . . . 10 i ∈ ℂ
185recnd 7794 . . . . . . . . . 10 (𝐴 ∈ (0(,]1) → 𝐴 ∈ ℂ)
19 mulcl 7747 . . . . . . . . . 10 ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
2017, 18, 19sylancr 410 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → (i · 𝐴) ∈ ℂ)
21 4nn0 8996 . . . . . . . . 9 4 ∈ ℕ0
226eftlcl 11394 . . . . . . . . 9 (((i · 𝐴) ∈ ℂ ∧ 4 ∈ ℕ0) → Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ)
2320, 21, 22sylancl 409 . . . . . . . 8 (𝐴 ∈ (0(,]1) → Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ)
2423recld 10710 . . . . . . 7 (𝐴 ∈ (0(,]1) → (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ)
2524recnd 7794 . . . . . 6 (𝐴 ∈ (0(,]1) → (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℂ)
2611, 16, 25subaddd 8091 . . . . 5 (𝐴 ∈ (0(,]1) → (((cos‘𝐴) − (1 − ((𝐴↑2) / 2))) = (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ↔ ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) = (cos‘𝐴)))
279, 26mpbird 166 . . . 4 (𝐴 ∈ (0(,]1) → ((cos‘𝐴) − (1 − ((𝐴↑2) / 2))) = (ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))
2827fveq2d 5425 . . 3 (𝐴 ∈ (0(,]1) → (abs‘((cos‘𝐴) − (1 − ((𝐴↑2) / 2)))) = (abs‘(ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))))
2925abscld 10953 . . . 4 (𝐴 ∈ (0(,]1) → (abs‘(ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ∈ ℝ)
3023abscld 10953 . . . 4 (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) ∈ ℝ)
31 6nn 8885 . . . . 5 6 ∈ ℕ
32 nndivre 8756 . . . . 5 (((𝐴↑2) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝐴↑2) / 6) ∈ ℝ)
3312, 31, 32sylancl 409 . . . 4 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈ ℝ)
34 absrele 10855 . . . . 5 𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ → (abs‘(ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))
3523, 34syl 14 . . . 4 (𝐴 ∈ (0(,]1) → (abs‘(ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) ≤ (abs‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)))
36 reexpcl 10310 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 4 ∈ ℕ0) → (𝐴↑4) ∈ ℝ)
375, 21, 36sylancl 409 . . . . . 6 (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈ ℝ)
38 nndivre 8756 . . . . . 6 (((𝐴↑4) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝐴↑4) / 6) ∈ ℝ)
3937, 31, 38sylancl 409 . . . . 5 (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈ ℝ)
406ef01bndlem 11463 . . . . 5 (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑4) / 6))
41 2nn0 8994 . . . . . . . 8 2 ∈ ℕ0
4241a1i 9 . . . . . . 7 (𝐴 ∈ (0(,]1) → 2 ∈ ℕ0)
43 4z 9084 . . . . . . . . 9 4 ∈ ℤ
44 2re 8790 . . . . . . . . . 10 2 ∈ ℝ
45 4re 8797 . . . . . . . . . 10 4 ∈ ℝ
46 2lt4 8893 . . . . . . . . . 10 2 < 4
4744, 45, 46ltleii 7866 . . . . . . . . 9 2 ≤ 4
48 2z 9082 . . . . . . . . . 10 2 ∈ ℤ
4948eluz1i 9333 . . . . . . . . 9 (4 ∈ (ℤ‘2) ↔ (4 ∈ ℤ ∧ 2 ≤ 4))
5043, 47, 49mpbir2an 926 . . . . . . . 8 4 ∈ (ℤ‘2)
5150a1i 9 . . . . . . 7 (𝐴 ∈ (0(,]1) → 4 ∈ (ℤ‘2))
524simp2bi 997 . . . . . . . 8 (𝐴 ∈ (0(,]1) → 0 < 𝐴)
53 0re 7766 . . . . . . . . 9 0 ∈ ℝ
54 ltle 7851 . . . . . . . . 9 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
5553, 5, 54sylancr 410 . . . . . . . 8 (𝐴 ∈ (0(,]1) → (0 < 𝐴 → 0 ≤ 𝐴))
5652, 55mpd 13 . . . . . . 7 (𝐴 ∈ (0(,]1) → 0 ≤ 𝐴)
574simp3bi 998 . . . . . . 7 (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1)
585, 42, 51, 56, 57leexp2rd 10454 . . . . . 6 (𝐴 ∈ (0(,]1) → (𝐴↑4) ≤ (𝐴↑2))
59 6re 8801 . . . . . . . 8 6 ∈ ℝ
6059a1i 9 . . . . . . 7 (𝐴 ∈ (0(,]1) → 6 ∈ ℝ)
61 6pos 8821 . . . . . . . 8 0 < 6
6261a1i 9 . . . . . . 7 (𝐴 ∈ (0(,]1) → 0 < 6)
63 lediv1 8627 . . . . . . 7 (((𝐴↑4) ∈ ℝ ∧ (𝐴↑2) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6)))
6437, 12, 60, 62, 63syl112anc 1220 . . . . . 6 (𝐴 ∈ (0(,]1) → ((𝐴↑4) ≤ (𝐴↑2) ↔ ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6)))
6558, 64mpbid 146 . . . . 5 (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ≤ ((𝐴↑2) / 6))
6630, 39, 33, 40, 65ltletrd 8185 . . . 4 (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘)) < ((𝐴↑2) / 6))
6729, 30, 33, 35, 66lelttrd 7887 . . 3 (𝐴 ∈ (0(,]1) → (abs‘(ℜ‘Σ𝑘 ∈ (ℤ‘4)((𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))‘𝑘))) < ((𝐴↑2) / 6))
6828, 67eqbrtrd 3950 . 2 (𝐴 ∈ (0(,]1) → (abs‘((cos‘𝐴) − (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6))
6910, 15, 33absdifltd 10950 . . 3 (𝐴 ∈ (0(,]1) → ((abs‘((cos‘𝐴) − (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ (((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) < (cos‘𝐴) ∧ (cos‘𝐴) < ((1 − ((𝐴↑2) / 2)) + ((𝐴↑2) / 6)))))
70 1cnd 7782 . . . . . . 7 (𝐴 ∈ (0(,]1) → 1 ∈ ℂ)
7113recnd 7794 . . . . . . 7 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) ∈ ℂ)
7233recnd 7794 . . . . . . 7 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) ∈ ℂ)
7370, 71, 72subsub4d 8104 . . . . . 6 (𝐴 ∈ (0(,]1) → ((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) = (1 − (((𝐴↑2) / 2) + ((𝐴↑2) / 6))))
74 halfpm6th 8940 . . . . . . . . . . 11 (((1 / 2) − (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 / 3))
7574simpri 112 . . . . . . . . . 10 ((1 / 2) + (1 / 6)) = (2 / 3)
7675oveq2i 5785 . . . . . . . . 9 ((𝐴↑2) · ((1 / 2) + (1 / 6))) = ((𝐴↑2) · (2 / 3))
7712recnd 7794 . . . . . . . . . 10 (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈ ℂ)
78 2cn 8791 . . . . . . . . . . . 12 2 ∈ ℂ
79 2ap0 8813 . . . . . . . . . . . 12 2 # 0
8078, 79recclapi 8502 . . . . . . . . . . 11 (1 / 2) ∈ ℂ
81 6cn 8802 . . . . . . . . . . . 12 6 ∈ ℂ
8231nnap0i 8751 . . . . . . . . . . . 12 6 # 0
8381, 82recclapi 8502 . . . . . . . . . . 11 (1 / 6) ∈ ℂ
84 adddi 7752 . . . . . . . . . . 11 (((𝐴↑2) ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) + (1 / 6))) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 / 6))))
8580, 83, 84mp3an23 1307 . . . . . . . . . 10 ((𝐴↑2) ∈ ℂ → ((𝐴↑2) · ((1 / 2) + (1 / 6))) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 / 6))))
8677, 85syl 14 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2) + (1 / 6))) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 / 6))))
8776, 86syl5eqr 2186 . . . . . . . 8 (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 / 6))))
88 3cn 8795 . . . . . . . . . . 11 3 ∈ ℂ
89 3ap0 8816 . . . . . . . . . . 11 3 # 0
9088, 89pm3.2i 270 . . . . . . . . . 10 (3 ∈ ℂ ∧ 3 # 0)
91 div12ap 8454 . . . . . . . . . 10 ((2 ∈ ℂ ∧ (𝐴↑2) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
9278, 90, 91mp3an13 1306 . . . . . . . . 9 ((𝐴↑2) ∈ ℂ → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
9377, 92syl 14 . . . . . . . 8 (𝐴 ∈ (0(,]1) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
94 divrecap 8448 . . . . . . . . . . 11 (((𝐴↑2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 # 0) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2)))
9578, 79, 94mp3an23 1307 . . . . . . . . . 10 ((𝐴↑2) ∈ ℂ → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2)))
9677, 95syl 14 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 2) = ((𝐴↑2) · (1 / 2)))
97 divrecap 8448 . . . . . . . . . . 11 (((𝐴↑2) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 # 0) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6)))
9881, 82, 97mp3an23 1307 . . . . . . . . . 10 ((𝐴↑2) ∈ ℂ → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6)))
9977, 98syl 14 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 6) = ((𝐴↑2) · (1 / 6)))
10096, 99oveq12d 5792 . . . . . . . 8 (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2)) + ((𝐴↑2) · (1 / 6))))
10187, 93, 1003eqtr4rd 2183 . . . . . . 7 (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) + ((𝐴↑2) / 6)) = (2 · ((𝐴↑2) / 3)))
102101oveq2d 5790 . . . . . 6 (𝐴 ∈ (0(,]1) → (1 − (((𝐴↑2) / 2) + ((𝐴↑2) / 6))) = (1 − (2 · ((𝐴↑2) / 3))))
10373, 102eqtrd 2172 . . . . 5 (𝐴 ∈ (0(,]1) → ((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) = (1 − (2 · ((𝐴↑2) / 3))))
104103breq1d 3939 . . . 4 (𝐴 ∈ (0(,]1) → (((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) < (cos‘𝐴) ↔ (1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴)))
10570, 71, 72subsubd 8101 . . . . . 6 (𝐴 ∈ (0(,]1) → (1 − (((𝐴↑2) / 2) − ((𝐴↑2) / 6))) = ((1 − ((𝐴↑2) / 2)) + ((𝐴↑2) / 6)))
10674simpli 110 . . . . . . . . . 10 ((1 / 2) − (1 / 6)) = (1 / 3)
107106oveq2i 5785 . . . . . . . . 9 ((𝐴↑2) · ((1 / 2) − (1 / 6))) = ((𝐴↑2) · (1 / 3))
108 subdi 8147 . . . . . . . . . . 11 (((𝐴↑2) ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝐴↑2) · ((1 / 2) − (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 / 6))))
10980, 83, 108mp3an23 1307 . . . . . . . . . 10 ((𝐴↑2) ∈ ℂ → ((𝐴↑2) · ((1 / 2) − (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 / 6))))
11077, 109syl 14 . . . . . . . . 9 (𝐴 ∈ (0(,]1) → ((𝐴↑2) · ((1 / 2) − (1 / 6))) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 / 6))))
111107, 110syl5eqr 2186 . . . . . . . 8 (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (1 / 3)) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 / 6))))
112 divrecap 8448 . . . . . . . . . 10 (((𝐴↑2) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 # 0) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3)))
11388, 89, 112mp3an23 1307 . . . . . . . . 9 ((𝐴↑2) ∈ ℂ → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3)))
11477, 113syl 14 . . . . . . . 8 (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 3) = ((𝐴↑2) · (1 / 3)))
11596, 99oveq12d 5792 . . . . . . . 8 (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = (((𝐴↑2) · (1 / 2)) − ((𝐴↑2) · (1 / 6))))
116111, 114, 1153eqtr4rd 2183 . . . . . . 7 (𝐴 ∈ (0(,]1) → (((𝐴↑2) / 2) − ((𝐴↑2) / 6)) = ((𝐴↑2) / 3))
117116oveq2d 5790 . . . . . 6 (𝐴 ∈ (0(,]1) → (1 − (((𝐴↑2) / 2) − ((𝐴↑2) / 6))) = (1 − ((𝐴↑2) / 3)))
118105, 117eqtr3d 2174 . . . . 5 (𝐴 ∈ (0(,]1) → ((1 − ((𝐴↑2) / 2)) + ((𝐴↑2) / 6)) = (1 − ((𝐴↑2) / 3)))
119118breq2d 3941 . . . 4 (𝐴 ∈ (0(,]1) → ((cos‘𝐴) < ((1 − ((𝐴↑2) / 2)) + ((𝐴↑2) / 6)) ↔ (cos‘𝐴) < (1 − ((𝐴↑2) / 3))))
120104, 119anbi12d 464 . . 3 (𝐴 ∈ (0(,]1) → ((((1 − ((𝐴↑2) / 2)) − ((𝐴↑2) / 6)) < (cos‘𝐴) ∧ (cos‘𝐴) < ((1 − ((𝐴↑2) / 2)) + ((𝐴↑2) / 6))) ↔ ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3)))))
12169, 120bitrd 187 . 2 (𝐴 ∈ (0(,]1) → ((abs‘((cos‘𝐴) − (1 − ((𝐴↑2) / 2)))) < ((𝐴↑2) / 6) ↔ ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3)))))
12268, 121mpbid 146 1 (𝐴 ∈ (0(,]1) → ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962   = wceq 1331   ∈ wcel 1480   class class class wbr 3929   ↦ cmpt 3989  ‘cfv 5123  (class class class)co 5774  ℂcc 7618  ℝcr 7619  0cc0 7620  1c1 7621  ici 7622   + caddc 7623   · cmul 7625  ℝ*cxr 7799   < clt 7800   ≤ cle 7801   − cmin 7933   # cap 8343   / cdiv 8432  ℕcn 8720  2c2 8771  3c3 8772  4c4 8773  6c6 8775  ℕ0cn0 8977  ℤcz 9054  ℤ≥cuz 9326  (,]cioc 9672  ↑cexp 10292  !cfa 10471  ℜcre 10612  abscabs 10769  Σcsu 11122  cosccos 11351 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-mulrcl 7719  ax-addcom 7720  ax-mulcom 7721  ax-addass 7722  ax-mulass 7723  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-1rid 7727  ax-0id 7728  ax-rnegex 7729  ax-precex 7730  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-apti 7735  ax-pre-ltadd 7736  ax-pre-mulgt0 7737  ax-pre-mulext 7738  ax-arch 7739  ax-caucvg 7740 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-reap 8337  df-ap 8344  df-div 8433  df-inn 8721  df-2 8779  df-3 8780  df-4 8781  df-5 8782  df-6 8783  df-7 8784  df-8 8785  df-n0 8978  df-z 9055  df-uz 9327  df-q 9412  df-rp 9442  df-ioc 9676  df-ico 9677  df-fz 9791  df-fzo 9920  df-seqfrec 10219  df-exp 10293  df-fac 10472  df-ihash 10522  df-shft 10587  df-cj 10614  df-re 10615  df-im 10616  df-rsqrt 10770  df-abs 10771  df-clim 11048  df-sumdc 11123  df-ef 11354  df-cos 11357 This theorem is referenced by:  cos1bnd  11466  cos01gt0  11469  tangtx  12919
 Copyright terms: Public domain W3C validator