Proof of Theorem tangtx
Step | Hyp | Ref
| Expression |
1 | | elioore 9840 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℝ) |
2 | 1 | recoscld 11655 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) ∈
ℝ) |
3 | 1, 2 | remulcld 7921 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) ∈
ℝ) |
4 | | 1re 7890 |
. . . . . . 7
⊢ 1 ∈
ℝ |
5 | | rehalfcl 9076 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
6 | 1, 5 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
ℝ) |
7 | 6 | resqcld 10604 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑2) ∈
ℝ) |
8 | | 3nn 9011 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
9 | | nndivre 8885 |
. . . . . . . 8
⊢ ((((𝐴 / 2)↑2) ∈ ℝ
∧ 3 ∈ ℕ) → (((𝐴 / 2)↑2) / 3) ∈
ℝ) |
10 | 7, 8, 9 | sylancl 410 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) / 3)
∈ ℝ) |
11 | | resubcl 8154 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
12 | 4, 10, 11 | sylancr 411 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
13 | 1, 12 | remulcld 7921 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
∈ ℝ) |
14 | | 2re 8919 |
. . . . . . 7
⊢ 2 ∈
ℝ |
15 | | remulcl 7873 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (2 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
16 | 14, 10, 15 | sylancr 411 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
17 | | resubcl 8154 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℝ) |
18 | 4, 16, 17 | sylancr 411 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℝ) |
19 | 13, 18 | remulcld 7921 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈
ℝ) |
20 | 1 | resincld 11654 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘𝐴) ∈
ℝ) |
21 | 12 | resqcld 10604 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) ∈ ℝ) |
22 | | remulcl 7873 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ)
→ (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈
ℝ) |
23 | 14, 21, 22 | sylancr 411 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈
ℝ) |
24 | | resubcl 8154 |
. . . . . . . 8
⊢ (((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) ∈ ℝ ∧ 1 ∈ ℝ) → ((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) − 1) ∈ ℝ) |
25 | 23, 4, 24 | sylancl 410 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1)
∈ ℝ) |
26 | 12, 18 | remulcld 7921 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈
ℝ) |
27 | 1 | recnd 7919 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℂ) |
28 | | 2cn 8920 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
29 | 28 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 ∈ ℂ) |
30 | | 2ap0 8942 |
. . . . . . . . . . . 12
⊢ 2 #
0 |
31 | 30 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 # 0) |
32 | 27, 29, 31 | divcanap2d 8680 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (𝐴 / 2)) =
𝐴) |
33 | 32 | fveq2d 5485 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(2 · (𝐴 /
2))) = (cos‘𝐴)) |
34 | 6 | recnd 7919 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
ℂ) |
35 | | cos2t 11681 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) |
36 | 34, 35 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) |
37 | 33, 36 | eqtr3d 2199 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) = ((2
· ((cos‘(𝐴 /
2))↑2)) − 1)) |
38 | 6 | recoscld 11655 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) ∈
ℝ) |
39 | 38 | resqcld 10604 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 /
2))↑2) ∈ ℝ) |
40 | | remulcl 7873 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℝ) → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℝ) |
41 | 14, 39, 40 | sylancr 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((cos‘(𝐴
/ 2))↑2)) ∈ ℝ) |
42 | 4 | a1i 9 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
1 ∈ ℝ) |
43 | 14 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 ∈ ℝ) |
44 | | eliooord 9856 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < 𝐴 ∧ 𝐴 < (π /
2))) |
45 | 44 | simpld 111 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 𝐴) |
46 | | 2pos 8940 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
47 | 46 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 2) |
48 | 1, 43, 45, 47 | divgt0d 8822 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (𝐴 /
2)) |
49 | | pire 13274 |
. . . . . . . . . . . . . . . . . . 19
⊢ π
∈ ℝ |
50 | | rehalfcl 9076 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π
∈ ℝ → (π / 2) ∈ ℝ) |
51 | 49, 50 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(π / 2) ∈ ℝ) |
52 | 44 | simprd 113 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (π /
2)) |
53 | | pigt2lt4 13272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 <
π ∧ π < 4) |
54 | 53 | simpri 112 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ π <
4 |
55 | | 2t2e4 9003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 2) = 4 |
56 | 54, 55 | breqtrri 4004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ π <
(2 · 2) |
57 | 14, 46 | pm3.2i 270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ ∧ 0 < 2) |
58 | | ltdivmul 8763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((π
∈ ℝ ∧ 2 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2))
→ ((π / 2) < 2 ↔ π < (2 · 2))) |
59 | 49, 14, 57, 58 | mp3an 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((π /
2) < 2 ↔ π < (2 · 2)) |
60 | 56, 59 | mpbir 145 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π /
2) < 2 |
61 | 60 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(π / 2) < 2) |
62 | 1, 51, 43, 52, 61 | lttrd 8016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < 2) |
63 | 28 | mulid2i 7894 |
. . . . . . . . . . . . . . . . 17
⊢ (1
· 2) = 2 |
64 | 62, 63 | breqtrrdi 4019 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (1 ·
2)) |
65 | | ltdivmul2 8765 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐴 / 2) < 1 ↔ 𝐴 < (1 · 2))) |
66 | 1, 42, 43, 47, 65 | syl112anc 1231 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) < 1 ↔
𝐴 < (1 ·
2))) |
67 | 64, 66 | mpbird 166 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) <
1) |
68 | 6, 42, 67 | ltled 8009 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ≤
1) |
69 | | 0xr 7937 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* |
70 | | elioc2 9864 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((𝐴 / 2) ∈ (0(,]1) ↔ ((𝐴 / 2) ∈ ℝ ∧ 0
< (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1))) |
71 | 69, 4, 70 | mp2an 423 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 / 2) ∈ (0(,]1) ↔
((𝐴 / 2) ∈ ℝ
∧ 0 < (𝐴 / 2) ∧
(𝐴 / 2) ≤
1)) |
72 | 6, 48, 68, 71 | syl3anbrc 1170 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
(0(,]1)) |
73 | | cos01bnd 11689 |
. . . . . . . . . . . . 13
⊢ ((𝐴 / 2) ∈ (0(,]1) → ((1
− (2 · (((𝐴 /
2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3)))) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) /
3)))) |
75 | 74 | simprd 113 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) < (1
− (((𝐴 / 2)↑2) /
3))) |
76 | | cos01gt0 11693 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 / 2) ∈ (0(,]1) → 0
< (cos‘(𝐴 /
2))) |
77 | 72, 76 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (cos‘(𝐴 /
2))) |
78 | | 0re 7891 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
79 | | ltle 7978 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → (0 <
(cos‘(𝐴 / 2)) →
0 ≤ (cos‘(𝐴 /
2)))) |
80 | 78, 38, 79 | sylancr 411 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (cos‘(𝐴 / 2))
→ 0 ≤ (cos‘(𝐴
/ 2)))) |
81 | 77, 80 | mpd 13 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ≤ (cos‘(𝐴 /
2))) |
82 | 78 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ∈ ℝ) |
83 | 82, 38, 12, 77, 75 | lttrd 8016 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (1 − (((𝐴 /
2)↑2) / 3))) |
84 | 82, 12, 83 | ltled 8009 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ≤ (1 − (((𝐴 /
2)↑2) / 3))) |
85 | 38, 12, 81, 84 | lt2sqd 10609 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 / 2)) <
(1 − (((𝐴 /
2)↑2) / 3)) ↔ ((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) /
3))↑2))) |
86 | 75, 85 | mpbid 146 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 /
2))↑2) < ((1 − (((𝐴 / 2)↑2) /
3))↑2)) |
87 | | ltmul2 8743 |
. . . . . . . . . . 11
⊢
((((cos‘(𝐴 /
2))↑2) ∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → (((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2)
↔ (2 · ((cos‘(𝐴 / 2))↑2)) < (2 · ((1 −
(((𝐴 / 2)↑2) /
3))↑2)))) |
88 | 39, 21, 43, 47, 87 | syl112anc 1231 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((cos‘(𝐴 /
2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2) ↔ (2
· ((cos‘(𝐴 /
2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) /
3))↑2)))) |
89 | 86, 88 | mpbid 146 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((cos‘(𝐴
/ 2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) /
3))↑2))) |
90 | 41, 23, 42, 89 | ltsub1dd 8447 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((cos‘(𝐴
/ 2))↑2)) − 1) < ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) −
1)) |
91 | 37, 90 | eqbrtrd 3999 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) < ((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) − 1)) |
92 | | 3re 8923 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
93 | | remulcl 7873 |
. . . . . . . . . 10
⊢ ((3
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (3 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
94 | 92, 10, 93 | sylancr 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
95 | | 4re 8926 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
96 | | remulcl 7873 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (4 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
97 | 95, 10, 96 | sylancr 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(4 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
98 | 10 | resqcld 10604 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) ∈ ℝ) |
99 | | remulcl 7873 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ ((((𝐴
/ 2)↑2) / 3)↑2) ∈ ℝ) → (2 · ((((𝐴 / 2)↑2) / 3)↑2))
∈ ℝ) |
100 | 14, 98, 99 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) ∈ ℝ) |
101 | | readdcl 7871 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℝ)
→ (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈
ℝ) |
102 | 4, 100, 101 | sylancr 411 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) ∈ ℝ) |
103 | | 3lt4 9021 |
. . . . . . . . . 10
⊢ 3 <
4 |
104 | 92 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 ∈ ℝ) |
105 | 95 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
4 ∈ ℝ) |
106 | 6, 48 | gt0ap0d 8519 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) #
0) |
107 | 6, 106 | sqgt0apd 10606 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < ((𝐴 /
2)↑2)) |
108 | | 3pos 8943 |
. . . . . . . . . . . . 13
⊢ 0 <
3 |
109 | 108 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 3) |
110 | 7, 104, 107, 109 | divgt0d 8822 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (((𝐴 / 2)↑2) /
3)) |
111 | | ltmul1 8482 |
. . . . . . . . . . 11
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ ∧ ((((𝐴 / 2)↑2) / 3) ∈ ℝ ∧ 0
< (((𝐴 / 2)↑2) /
3))) → (3 < 4 ↔ (3 · (((𝐴 / 2)↑2) / 3)) < (4 ·
(((𝐴 / 2)↑2) /
3)))) |
112 | 104, 105,
10, 110, 111 | syl112anc 1231 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 < 4 ↔ (3 · (((𝐴 / 2)↑2) / 3)) < (4 ·
(((𝐴 / 2)↑2) /
3)))) |
113 | 103, 112 | mpbii 147 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) < (4 · (((𝐴 / 2)↑2) / 3))) |
114 | 94, 97, 102, 113 | ltsub2dd 8448 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) < ((1 + (2 ·
((((𝐴 / 2)↑2) /
3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3)))) |
115 | 42 | recnd 7919 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
1 ∈ ℂ) |
116 | | ax-1cn 7838 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
117 | 100 | recnd 7919 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) ∈ ℂ) |
118 | | addcl 7870 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ)
→ (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈
ℂ) |
119 | 116, 117,
118 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) ∈ ℂ) |
120 | 97 | recnd 7919 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(4 · (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
121 | 119, 120 | subcld 8201 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) ∈
ℂ) |
122 | | sq1 10539 |
. . . . . . . . . . . . . . 15
⊢
(1↑2) = 1 |
123 | 122 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1↑2) = 1) |
124 | 10 | recnd 7919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) / 3)
∈ ℂ) |
125 | 124 | mulid2d 7909 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 · (((𝐴 /
2)↑2) / 3)) = (((𝐴 /
2)↑2) / 3)) |
126 | 125 | oveq2d 5853 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) /
3))) |
127 | 123, 126 | oveq12d 5855 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) = (1 − (2
· (((𝐴 / 2)↑2)
/ 3)))) |
128 | 127 | oveq1d 5852 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) + ((((𝐴 / 2)↑2) / 3)↑2)) =
((1 − (2 · (((𝐴 / 2)↑2) / 3))) + ((((𝐴 / 2)↑2) /
3)↑2))) |
129 | | binom2sub 10558 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℂ) → ((1 − (((𝐴 / 2)↑2) / 3))↑2) = (((1↑2)
− (2 · (1 · (((𝐴 / 2)↑2) / 3)))) + ((((𝐴 / 2)↑2) /
3)↑2))) |
130 | 116, 124,
129 | sylancr 411 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) = (((1↑2) − (2 · (1 ·
(((𝐴 / 2)↑2) / 3)))) +
((((𝐴 / 2)↑2) /
3)↑2))) |
131 | 98 | recnd 7919 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) ∈ ℂ) |
132 | 16 | recnd 7919 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
133 | 115, 131,
132 | addsubd 8222 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + ((((𝐴 / 2)↑2) /
3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3))) = ((1 − (2
· (((𝐴 / 2)↑2)
/ 3))) + ((((𝐴 / 2)↑2)
/ 3)↑2))) |
134 | 128, 130,
133 | 3eqtr4d 2207 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) = ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2
· (((𝐴 / 2)↑2)
/ 3)))) |
135 | 134 | oveq2d 5853 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) = (2 ·
((1 + ((((𝐴 / 2)↑2) /
3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3))))) |
136 | | addcl 7870 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ((((𝐴
/ 2)↑2) / 3)↑2) ∈ ℂ) → (1 + ((((𝐴 / 2)↑2) / 3)↑2)) ∈
ℂ) |
137 | 116, 131,
136 | sylancr 411 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + ((((𝐴 / 2)↑2) /
3)↑2)) ∈ ℂ) |
138 | 29, 137, 132 | subdid 8304 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 + ((((𝐴 /
2)↑2) / 3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3)))) = ((2 · (1 +
((((𝐴 / 2)↑2) /
3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3))))) |
139 | 29, 115, 131 | adddid 7915 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) = ((2 · 1) + (2 · ((((𝐴 / 2)↑2) /
3)↑2)))) |
140 | 116 | 2timesi 8979 |
. . . . . . . . . . . . . . 15
⊢ (2
· 1) = (1 + 1) |
141 | 140 | oveq1i 5847 |
. . . . . . . . . . . . . 14
⊢ ((2
· 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = ((1 + 1) + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))) |
142 | 115, 115,
117 | addassd 7913 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))))) |
143 | 141, 142 | syl5eq 2209 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))))) |
144 | 139, 143 | eqtrd 2197 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) = (1 + (1 + (2 · ((((𝐴 / 2)↑2) /
3)↑2))))) |
145 | 29, 29, 124 | mulassd 7914 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · 2) · (((𝐴 / 2)↑2) / 3)) = (2 · (2
· (((𝐴 / 2)↑2)
/ 3)))) |
146 | 55 | oveq1i 5847 |
. . . . . . . . . . . . 13
⊢ ((2
· 2) · (((𝐴 /
2)↑2) / 3)) = (4 · (((𝐴 / 2)↑2) / 3)) |
147 | 145, 146 | eqtr3di 2212 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (2 · (((𝐴 / 2)↑2) / 3))) = (4 · (((𝐴 / 2)↑2) /
3))) |
148 | 144, 147 | oveq12d 5855 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3)))) = ((1 + (1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2)))) − (4 · (((𝐴 / 2)↑2) / 3)))) |
149 | 115, 119,
120, 148 | assraddsubd 8258 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3)))) = (1 + ((1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))))) |
150 | 135, 138,
149 | 3eqtrd 2201 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) = (1 + ((1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))))) |
151 | 115, 121,
150 | mvrladdd 8257 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) =
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))) |
152 | | subcl 8089 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℂ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈
ℂ) |
153 | 116, 124,
152 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
154 | 153, 115,
132 | subdid 8304 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = (((1 −
(((𝐴 / 2)↑2) / 3))
· 1) − ((1 − (((𝐴 / 2)↑2) / 3)) · (2 ·
(((𝐴 / 2)↑2) /
3))))) |
155 | 153 | mulid1d 7908 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · 1) = (1 − (((𝐴 / 2)↑2) / 3))) |
156 | 115, 124,
132 | subdird 8305 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3))) = ((1 · (2
· (((𝐴 / 2)↑2)
/ 3))) − ((((𝐴 /
2)↑2) / 3) · (2 · (((𝐴 / 2)↑2) / 3))))) |
157 | 132 | mulid2d 7909 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 · (2 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) /
3))) |
158 | 124, 29, 124 | mul12d 8042 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) / 3)
· (2 · (((𝐴 /
2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) /
3)))) |
159 | 124 | sqvald 10575 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) = ((((𝐴 /
2)↑2) / 3) · (((𝐴 / 2)↑2) / 3))) |
160 | 159 | oveq2d 5853 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) /
3)))) |
161 | 158, 160 | eqtr4d 2200 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) / 3)
· (2 · (((𝐴 /
2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) /
3)↑2))) |
162 | 157, 161 | oveq12d 5855 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 · (2 · (((𝐴 / 2)↑2) / 3))) − ((((𝐴 / 2)↑2) / 3) · (2
· (((𝐴 / 2)↑2)
/ 3)))) = ((2 · (((𝐴
/ 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) /
3)↑2)))) |
163 | 156, 162 | eqtrd 2197 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3))) = ((2 · (((𝐴 / 2)↑2) / 3)) − (2
· ((((𝐴 / 2)↑2)
/ 3)↑2)))) |
164 | 155, 163 | oveq12d 5855 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((1 − (((𝐴 /
2)↑2) / 3)) · 1) − ((1 − (((𝐴 / 2)↑2) / 3)) · (2 ·
(((𝐴 / 2)↑2) / 3)))) =
((1 − (((𝐴 /
2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 ·
((((𝐴 / 2)↑2) /
3)↑2))))) |
165 | 115, 124,
132, 117 | subadd4d 8249 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 ·
((((𝐴 / 2)↑2) /
3)↑2)))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) −
((((𝐴 / 2)↑2) / 3) +
(2 · (((𝐴 /
2)↑2) / 3))))) |
166 | | df-3 8909 |
. . . . . . . . . . . . . 14
⊢ 3 = (2 +
1) |
167 | 28, 116 | addcomi 8034 |
. . . . . . . . . . . . . 14
⊢ (2 + 1) =
(1 + 2) |
168 | 166, 167 | eqtri 2185 |
. . . . . . . . . . . . 13
⊢ 3 = (1 +
2) |
169 | 168 | oveq1i 5847 |
. . . . . . . . . . . 12
⊢ (3
· (((𝐴 / 2)↑2)
/ 3)) = ((1 + 2) · (((𝐴 / 2)↑2) / 3)) |
170 | 125 | oveq1d 5852 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 · (((𝐴 /
2)↑2) / 3)) + (2 · (((𝐴 / 2)↑2) / 3))) = ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) /
3)))) |
171 | 115, 124,
29, 170 | joinlmuladdmuld 7918 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + 2) · (((𝐴 /
2)↑2) / 3)) = ((((𝐴 /
2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))) |
172 | 169, 171 | syl5eq 2209 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) = ((((𝐴 /
2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))) |
173 | 172 | oveq2d 5853 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3))) = ((1 + (2 ·
((((𝐴 / 2)↑2) /
3)↑2))) − ((((𝐴
/ 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3))))) |
174 | 165, 173 | eqtr4d 2200 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 ·
((((𝐴 / 2)↑2) /
3)↑2)))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (3
· (((𝐴 / 2)↑2)
/ 3)))) |
175 | 154, 164,
174 | 3eqtrd 2201 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = ((1 + (2 ·
((((𝐴 / 2)↑2) /
3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3)))) |
176 | 114, 151,
175 | 3brtr4d 4009 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) <
((1 − (((𝐴 /
2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3))))) |
177 | 2, 25, 26, 91, 176 | lttrd 8016 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) < ((1
− (((𝐴 / 2)↑2) /
3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3))))) |
178 | | ltmul2 8743 |
. . . . . . 7
⊢
(((cos‘𝐴)
∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2
· (((𝐴 / 2)↑2)
/ 3)))) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((cos‘𝐴) < ((1 − (((𝐴 / 2)↑2) / 3)) · (1
− (2 · (((𝐴 /
2)↑2) / 3)))) ↔ (𝐴 · (cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2
· (((𝐴 / 2)↑2)
/ 3))))))) |
179 | 2, 26, 1, 45, 178 | syl112anc 1231 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘𝐴) < ((1
− (((𝐴 / 2)↑2) /
3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ↔ (𝐴 · (cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2
· (((𝐴 / 2)↑2)
/ 3))))))) |
180 | 177, 179 | mpbid 146 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1
− (2 · (((𝐴 /
2)↑2) / 3)))))) |
181 | 18 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℂ) |
182 | 27, 153, 181 | mulassd 7914 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2
· (((𝐴 / 2)↑2)
/ 3)))))) |
183 | 180, 182 | breqtrrd 4005 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1
− (2 · (((𝐴 /
2)↑2) / 3))))) |
184 | 13, 38 | remulcld 7921 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
185 | 74 | simpld 111 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) < (cos‘(𝐴 / 2))) |
186 | 1, 12, 45, 83 | mulgt0d 8013 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (𝐴 · (1
− (((𝐴 / 2)↑2) /
3)))) |
187 | | ltmul2 8743 |
. . . . . . 7
⊢ (((1
− (2 · (((𝐴 /
2)↑2) / 3))) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ ∧ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ∈
ℝ ∧ 0 < (𝐴
· (1 − (((𝐴 /
2)↑2) / 3))))) → ((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1
− (2 · (((𝐴 /
2)↑2) / 3)))) < ((𝐴
· (1 − (((𝐴 /
2)↑2) / 3))) · (cos‘(𝐴 / 2))))) |
188 | 18, 38, 13, 186, 187 | syl112anc 1231 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1
− (2 · (((𝐴 /
2)↑2) / 3)))) < ((𝐴
· (1 − (((𝐴 /
2)↑2) / 3))) · (cos‘(𝐴 / 2))))) |
189 | 185, 188 | mpbid 146 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ·
(cos‘(𝐴 /
2)))) |
190 | 29, 34, 153 | mulassd 7914 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (𝐴 / 2))
· (1 − (((𝐴 /
2)↑2) / 3))) = (2 · ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) /
3))))) |
191 | 32 | oveq1d 5852 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (𝐴 / 2))
· (1 − (((𝐴 /
2)↑2) / 3))) = (𝐴
· (1 − (((𝐴 /
2)↑2) / 3)))) |
192 | 34, 115, 124 | subdid 8304 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (1
− (((𝐴 / 2)↑2) /
3))) = (((𝐴 / 2) ·
1) − ((𝐴 / 2)
· (((𝐴 / 2)↑2)
/ 3)))) |
193 | 34 | mulid1d 7908 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · 1) =
(𝐴 / 2)) |
194 | 166 | oveq2i 5848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 / 2)↑3) = ((𝐴 / 2)↑(2 +
1)) |
195 | | 2nn0 9123 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ0 |
196 | | expp1 10453 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 / 2) ∈ ℂ ∧ 2
∈ ℕ0) → ((𝐴 / 2)↑(2 + 1)) = (((𝐴 / 2)↑2) · (𝐴 / 2))) |
197 | 34, 195, 196 | sylancl 410 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑(2 + 1)) =
(((𝐴 / 2)↑2) ·
(𝐴 / 2))) |
198 | 194, 197 | syl5eq 2209 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) = (((𝐴 / 2)↑2) · (𝐴 / 2))) |
199 | 7 | recnd 7919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑2) ∈
ℂ) |
200 | 199, 34 | mulcomd 7912 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) ·
(𝐴 / 2)) = ((𝐴 / 2) · ((𝐴 / 2)↑2))) |
201 | 198, 200 | eqtrd 2197 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) = ((𝐴 / 2) · ((𝐴 / 2)↑2))) |
202 | 201 | oveq1d 5852 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑3) / 3) =
(((𝐴 / 2) · ((𝐴 / 2)↑2)) /
3)) |
203 | | 3cn 8924 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
204 | 203 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 ∈ ℂ) |
205 | 104, 109 | gt0ap0d 8519 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 # 0) |
206 | 34, 199, 204, 205 | divassapd 8714 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) · ((𝐴 / 2)↑2)) / 3) = ((𝐴 / 2) · (((𝐴 / 2)↑2) /
3))) |
207 | 202, 206 | eqtr2d 2198 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (((𝐴 / 2)↑2) / 3)) = (((𝐴 / 2)↑3) /
3)) |
208 | 193, 207 | oveq12d 5855 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) · 1)
− ((𝐴 / 2) ·
(((𝐴 / 2)↑2) / 3))) =
((𝐴 / 2) − (((𝐴 / 2)↑3) /
3))) |
209 | 192, 208 | eqtrd 2197 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (1
− (((𝐴 / 2)↑2) /
3))) = ((𝐴 / 2) −
(((𝐴 / 2)↑3) /
3))) |
210 | 209 | oveq2d 5853 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((𝐴 / 2)
· (1 − (((𝐴 /
2)↑2) / 3)))) = (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)))) |
211 | 190, 191,
210 | 3eqtr3d 2205 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3))) =
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3)))) |
212 | | sin01bnd 11688 |
. . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ (0(,]1) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ∧
(sin‘(𝐴 / 2)) <
(𝐴 / 2))) |
213 | 72, 212 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ∧
(sin‘(𝐴 / 2)) <
(𝐴 / 2))) |
214 | 213 | simpld 111 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 /
2))) |
215 | | 3nn0 9124 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
216 | | reexpcl 10463 |
. . . . . . . . . . . . 13
⊢ (((𝐴 / 2) ∈ ℝ ∧ 3
∈ ℕ0) → ((𝐴 / 2)↑3) ∈
ℝ) |
217 | 6, 215, 216 | sylancl 410 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) ∈
ℝ) |
218 | | nndivre 8885 |
. . . . . . . . . . . 12
⊢ ((((𝐴 / 2)↑3) ∈ ℝ
∧ 3 ∈ ℕ) → (((𝐴 / 2)↑3) / 3) ∈
ℝ) |
219 | 217, 8, 218 | sylancl 410 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑3) / 3)
∈ ℝ) |
220 | 6, 219 | resubcld 8271 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈
ℝ) |
221 | 6 | resincld 11654 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(𝐴 / 2)) ∈
ℝ) |
222 | | ltmul2 8743 |
. . . . . . . . . 10
⊢ ((((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈
ℝ ∧ (sin‘(𝐴
/ 2)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ↔
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2))))) |
223 | 220, 221,
43, 47, 222 | syl112anc 1231 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ↔
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2))))) |
224 | 214, 223 | mpbid 146 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2)))) |
225 | 211, 224 | eqbrtrd 3999 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
< (2 · (sin‘(𝐴 / 2)))) |
226 | | remulcl 7873 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (sin‘(𝐴 / 2)) ∈ ℝ) → (2 ·
(sin‘(𝐴 / 2))) ∈
ℝ) |
227 | 14, 221, 226 | sylancr 411 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (sin‘(𝐴 /
2))) ∈ ℝ) |
228 | | ltmul1 8482 |
. . . . . . . 8
⊢ (((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ∈
ℝ ∧ (2 · (sin‘(𝐴 / 2))) ∈ ℝ ∧
((cos‘(𝐴 / 2)) ∈
ℝ ∧ 0 < (cos‘(𝐴 / 2)))) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) < (2 ·
(sin‘(𝐴 / 2))) ↔
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))))) |
229 | 13, 227, 38, 77, 228 | syl112anc 1231 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
< (2 · (sin‘(𝐴 / 2))) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ·
(cos‘(𝐴 / 2))) <
((2 · (sin‘(𝐴
/ 2))) · (cos‘(𝐴 / 2))))) |
230 | 225, 229 | mpbid 146 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2)))) |
231 | 221 | recnd 7919 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(𝐴 / 2)) ∈
ℂ) |
232 | 38 | recnd 7919 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) ∈
ℂ) |
233 | 29, 231, 232 | mulassd 7914 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (sin‘(𝐴
/ 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 /
2))))) |
234 | | sin2t 11680 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
235 | 34, 234 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
236 | 32 | fveq2d 5485 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(2 · (𝐴 /
2))) = (sin‘𝐴)) |
237 | 233, 235,
236 | 3eqtr2rd 2204 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘𝐴) = ((2
· (sin‘(𝐴 /
2))) · (cos‘(𝐴
/ 2)))) |
238 | 230, 237 | breqtrrd 4005 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) < (sin‘𝐴)) |
239 | 19, 184, 20, 189, 238 | lttrd 8016 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < (sin‘𝐴)) |
240 | 3, 19, 20, 183, 239 | lttrd 8016 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴)) |
241 | | sincosq1sgn 13314 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
242 | 241 | simprd 113 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (cos‘𝐴)) |
243 | | ltmuldiv 8761 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(sin‘𝐴) ∈
ℝ ∧ ((cos‘𝐴) ∈ ℝ ∧ 0 <
(cos‘𝐴))) →
((𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴)))) |
244 | 1, 20, 2, 242, 243 | syl112anc 1231 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴)))) |
245 | 240, 244 | mpbid 146 |
. 2
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < ((sin‘𝐴) / (cos‘𝐴))) |
246 | 2, 242 | gt0ap0d 8519 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) #
0) |
247 | | tanvalap 11639 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) # 0) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
248 | 27, 246, 247 | syl2anc 409 |
. 2
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
249 | 245, 248 | breqtrrd 4005 |
1
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (tan‘𝐴)) |