Proof of Theorem tangtx
| Step | Hyp | Ref
| Expression |
| 1 | | elioore 13417 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℝ) |
| 2 | 1 | recoscld 16180 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) ∈
ℝ) |
| 3 | 1, 2 | remulcld 11291 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) ∈
ℝ) |
| 4 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 5 | | rehalfcl 12492 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
| 6 | 1, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
ℝ) |
| 7 | 6 | resqcld 14165 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑2) ∈
ℝ) |
| 8 | | 3nn 12345 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
| 9 | | nndivre 12307 |
. . . . . . . 8
⊢ ((((𝐴 / 2)↑2) ∈ ℝ
∧ 3 ∈ ℕ) → (((𝐴 / 2)↑2) / 3) ∈
ℝ) |
| 10 | 7, 8, 9 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) / 3)
∈ ℝ) |
| 11 | | resubcl 11573 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
| 12 | 4, 10, 11 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
| 13 | 1, 12 | remulcld 11291 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
∈ ℝ) |
| 14 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 15 | | remulcl 11240 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (2 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
| 16 | 14, 10, 15 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
| 17 | | resubcl 11573 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℝ) |
| 18 | 4, 16, 17 | sylancr 587 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℝ) |
| 19 | 13, 18 | remulcld 11291 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈
ℝ) |
| 20 | 1 | resincld 16179 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘𝐴) ∈
ℝ) |
| 21 | 12 | resqcld 14165 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) ∈ ℝ) |
| 22 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ)
→ (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈
ℝ) |
| 23 | 14, 21, 22 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈
ℝ) |
| 24 | | resubcl 11573 |
. . . . . . . 8
⊢ (((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) ∈ ℝ ∧ 1 ∈ ℝ) → ((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) − 1) ∈ ℝ) |
| 25 | 23, 4, 24 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1)
∈ ℝ) |
| 26 | 12, 18 | remulcld 11291 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈
ℝ) |
| 27 | 1 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℂ) |
| 28 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 ∈ ℂ) |
| 30 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 31 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 ≠ 0) |
| 32 | 27, 29, 31 | divcan2d 12045 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (𝐴 / 2)) =
𝐴) |
| 33 | 32 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(2 · (𝐴 /
2))) = (cos‘𝐴)) |
| 34 | 6 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
ℂ) |
| 35 | | cos2t 16214 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) |
| 37 | 33, 36 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) = ((2
· ((cos‘(𝐴 /
2))↑2)) − 1)) |
| 38 | 6 | recoscld 16180 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) ∈
ℝ) |
| 39 | 38 | resqcld 14165 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 /
2))↑2) ∈ ℝ) |
| 40 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℝ) → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℝ) |
| 41 | 14, 39, 40 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((cos‘(𝐴
/ 2))↑2)) ∈ ℝ) |
| 42 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
1 ∈ ℝ) |
| 43 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
2 ∈ ℝ) |
| 44 | | eliooord 13446 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < 𝐴 ∧ 𝐴 < (π /
2))) |
| 45 | 44 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 𝐴) |
| 46 | | 2pos 12369 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
| 47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 2) |
| 48 | 1, 43, 45, 47 | divgt0d 12203 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (𝐴 /
2)) |
| 49 | | pire 26500 |
. . . . . . . . . . . . . . . . . . 19
⊢ π
∈ ℝ |
| 50 | | rehalfcl 12492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π
∈ ℝ → (π / 2) ∈ ℝ) |
| 51 | 49, 50 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(π / 2) ∈ ℝ) |
| 52 | 44 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (π /
2)) |
| 53 | | pigt2lt4 26498 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 <
π ∧ π < 4) |
| 54 | 53 | simpri 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ π <
4 |
| 55 | | 2t2e4 12430 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 2) = 4 |
| 56 | 54, 55 | breqtrri 5170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ π <
(2 · 2) |
| 57 | 14, 46 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 58 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((π
∈ ℝ ∧ 2 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2))
→ ((π / 2) < 2 ↔ π < (2 · 2))) |
| 59 | 49, 14, 57, 58 | mp3an 1463 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((π /
2) < 2 ↔ π < (2 · 2)) |
| 60 | 56, 59 | mpbir 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π /
2) < 2 |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(π / 2) < 2) |
| 62 | 1, 51, 43, 52, 61 | lttrd 11422 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < 2) |
| 63 | 28 | mullidi 11266 |
. . . . . . . . . . . . . . . . 17
⊢ (1
· 2) = 2 |
| 64 | 62, 63 | breqtrrdi 5185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (1 ·
2)) |
| 65 | | ltdivmul2 12145 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐴 / 2) < 1 ↔ 𝐴 < (1 · 2))) |
| 66 | 1, 42, 43, 47, 65 | syl112anc 1376 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) < 1 ↔
𝐴 < (1 ·
2))) |
| 67 | 64, 66 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) <
1) |
| 68 | 6, 42, 67 | ltled 11409 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ≤
1) |
| 69 | | 0xr 11308 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* |
| 70 | | elioc2 13450 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((𝐴 / 2) ∈ (0(,]1) ↔ ((𝐴 / 2) ∈ ℝ ∧ 0
< (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1))) |
| 71 | 69, 4, 70 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 / 2) ∈ (0(,]1) ↔
((𝐴 / 2) ∈ ℝ
∧ 0 < (𝐴 / 2) ∧
(𝐴 / 2) ≤
1)) |
| 72 | 6, 48, 68, 71 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ∈
(0(,]1)) |
| 73 | | cos01bnd 16222 |
. . . . . . . . . . . . 13
⊢ ((𝐴 / 2) ∈ (0(,]1) → ((1
− (2 · (((𝐴 /
2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3)))) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) /
3)))) |
| 75 | 74 | simprd 495 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) < (1
− (((𝐴 / 2)↑2) /
3))) |
| 76 | | cos01gt0 16227 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 / 2) ∈ (0(,]1) → 0
< (cos‘(𝐴 /
2))) |
| 77 | 72, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (cos‘(𝐴 /
2))) |
| 78 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 79 | | ltle 11349 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → (0 <
(cos‘(𝐴 / 2)) →
0 ≤ (cos‘(𝐴 /
2)))) |
| 80 | 78, 38, 79 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (cos‘(𝐴 / 2))
→ 0 ≤ (cos‘(𝐴
/ 2)))) |
| 81 | 77, 80 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ≤ (cos‘(𝐴 /
2))) |
| 82 | 78 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ∈ ℝ) |
| 83 | 82, 38, 12, 77, 75 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (1 − (((𝐴 /
2)↑2) / 3))) |
| 84 | 82, 12, 83 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 ≤ (1 − (((𝐴 /
2)↑2) / 3))) |
| 85 | 38, 12, 81, 84 | lt2sqd 14295 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 / 2)) <
(1 − (((𝐴 /
2)↑2) / 3)) ↔ ((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) /
3))↑2))) |
| 86 | 75, 85 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((cos‘(𝐴 /
2))↑2) < ((1 − (((𝐴 / 2)↑2) /
3))↑2)) |
| 87 | | ltmul2 12118 |
. . . . . . . . . . 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 1376 |
. . . . . . . . . 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 232 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((cos‘(𝐴
/ 2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) /
3))↑2))) |
| 90 | 41, 23, 42, 89 | ltsub1dd 11875 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((cos‘(𝐴
/ 2))↑2)) − 1) < ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) −
1)) |
| 91 | 37, 90 | eqbrtrd 5165 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) < ((2
· ((1 − (((𝐴 /
2)↑2) / 3))↑2)) − 1)) |
| 92 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 93 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((3
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (3 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
| 94 | 92, 10, 93 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
| 95 | | 4re 12350 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
| 96 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℝ) → (4 · (((𝐴 / 2)↑2) / 3)) ∈
ℝ) |
| 97 | 95, 10, 96 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(4 · (((𝐴 /
2)↑2) / 3)) ∈ ℝ) |
| 98 | 10 | resqcld 14165 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) ∈ ℝ) |
| 99 | | remulcl 11240 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ ((((𝐴
/ 2)↑2) / 3)↑2) ∈ ℝ) → (2 · ((((𝐴 / 2)↑2) / 3)↑2))
∈ ℝ) |
| 100 | 14, 98, 99 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) ∈ ℝ) |
| 101 | | readdcl 11238 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℝ)
→ (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈
ℝ) |
| 102 | 4, 100, 101 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) ∈ ℝ) |
| 103 | | 3lt4 12440 |
. . . . . . . . . 10
⊢ 3 <
4 |
| 104 | 92 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 ∈ ℝ) |
| 105 | 95 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
4 ∈ ℝ) |
| 106 | 48 | gt0ne0d 11827 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 / 2) ≠
0) |
| 107 | 6, 106 | sqgt0d 14289 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < ((𝐴 /
2)↑2)) |
| 108 | | 3pos 12371 |
. . . . . . . . . . . . 13
⊢ 0 <
3 |
| 109 | 108 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < 3) |
| 110 | 7, 104, 107, 109 | divgt0d 12203 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (((𝐴 / 2)↑2) /
3)) |
| 111 | | ltmul1 12117 |
. . . . . . . . . . 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 1376 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 < 4 ↔ (3 · (((𝐴 / 2)↑2) / 3)) < (4 ·
(((𝐴 / 2)↑2) /
3)))) |
| 113 | 103, 112 | mpbii 233 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) < (4 · (((𝐴 / 2)↑2) / 3))) |
| 114 | 94, 97, 102, 113 | ltsub2dd 11876 |
. . . . . . . 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 11289 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
1 ∈ ℂ) |
| 116 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 117 | 100 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) ∈ ℂ) |
| 118 | | addcl 11237 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ)
→ (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈
ℂ) |
| 119 | 116, 117,
118 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) ∈ ℂ) |
| 120 | 97 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(4 · (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
| 121 | 119, 120 | subcld 11620 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) ∈
ℂ) |
| 122 | | sq1 14234 |
. . . . . . . . . . . . . . 15
⊢
(1↑2) = 1 |
| 123 | 122 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1↑2) = 1) |
| 124 | 10 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) / 3)
∈ ℂ) |
| 125 | 124 | mullidd 11279 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 · (((𝐴 /
2)↑2) / 3)) = (((𝐴 /
2)↑2) / 3)) |
| 126 | 125 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) /
3))) |
| 127 | 123, 126 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) = (1 − (2
· (((𝐴 / 2)↑2)
/ 3)))) |
| 128 | 127 | oveq1d 7446 |
. . . . . . . . . . . 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 14259 |
. . . . . . . . . . . . 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 587 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) = (((1↑2) − (2 · (1 ·
(((𝐴 / 2)↑2) / 3)))) +
((((𝐴 / 2)↑2) /
3)↑2))) |
| 131 | 98 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) ∈ ℂ) |
| 132 | 16 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
| 133 | 115, 131,
132 | addsubd 11641 |
. . . . . . . . . . . 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 2787 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3))↑2) = ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2
· (((𝐴 / 2)↑2)
/ 3)))) |
| 135 | 134 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) = (2 ·
((1 + ((((𝐴 / 2)↑2) /
3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3))))) |
| 136 | | addcl 11237 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ((((𝐴
/ 2)↑2) / 3)↑2) ∈ ℂ) → (1 + ((((𝐴 / 2)↑2) / 3)↑2)) ∈
ℂ) |
| 137 | 116, 131,
136 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 + ((((𝐴 / 2)↑2) /
3)↑2)) ∈ ℂ) |
| 138 | 29, 137, 132 | subdid 11719 |
. . . . . . . . . 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 11285 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) = ((2 · 1) + (2 · ((((𝐴 / 2)↑2) /
3)↑2)))) |
| 140 | 116 | 2timesi 12404 |
. . . . . . . . . . . . . . 15
⊢ (2
· 1) = (1 + 1) |
| 141 | 140 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((2
· 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = ((1 + 1) + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))) |
| 142 | 115, 115,
117 | addassd 11283 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))))) |
| 143 | 141, 142 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2
· ((((𝐴 / 2)↑2)
/ 3)↑2))))) |
| 144 | 139, 143 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (1 + ((((𝐴 /
2)↑2) / 3)↑2))) = (1 + (1 + (2 · ((((𝐴 / 2)↑2) /
3)↑2))))) |
| 145 | 29, 29, 124 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · 2) · (((𝐴 / 2)↑2) / 3)) = (2 · (2
· (((𝐴 / 2)↑2)
/ 3)))) |
| 146 | 55 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((2
· 2) · (((𝐴 /
2)↑2) / 3)) = (4 · (((𝐴 / 2)↑2) / 3)) |
| 147 | 145, 146 | eqtr3di 2792 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (2 · (((𝐴 / 2)↑2) / 3))) = (4 · (((𝐴 / 2)↑2) /
3))) |
| 148 | 144, 147 | oveq12d 7449 |
. . . . . . . . . . 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 11677 |
. . . . . . . . . 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 2781 |
. . . . . . . . 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 11676 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) =
((1 + (2 · ((((𝐴 /
2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))) |
| 152 | | subcl 11507 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (((𝐴 /
2)↑2) / 3) ∈ ℂ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈
ℂ) |
| 153 | 116, 124,
152 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (((𝐴 /
2)↑2) / 3)) ∈ ℂ) |
| 154 | 153, 115,
132 | subdid 11719 |
. . . . . . . . 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 | mulridd 11278 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · 1) = (1 − (((𝐴 / 2)↑2) / 3))) |
| 156 | 115, 124,
132 | subdird 11720 |
. . . . . . . . . . 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 | mullidd 11279 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 · (2 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) /
3))) |
| 158 | 124, 29, 124 | mul12d 11470 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) / 3)
· (2 · (((𝐴 /
2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) /
3)))) |
| 159 | 124 | sqvald 14183 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) /
3)↑2) = ((((𝐴 /
2)↑2) / 3) · (((𝐴 / 2)↑2) / 3))) |
| 160 | 159 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((((𝐴 /
2)↑2) / 3)↑2)) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) /
3)))) |
| 161 | 158, 160 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((((𝐴 / 2)↑2) / 3)
· (2 · (((𝐴 /
2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) /
3)↑2))) |
| 162 | 157, 161 | oveq12d 7449 |
. . . . . . . . . . 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 2777 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 − (((𝐴 /
2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3))) = ((2 · (((𝐴 / 2)↑2) / 3)) − (2
· ((((𝐴 / 2)↑2)
/ 3)↑2)))) |
| 164 | 155, 163 | oveq12d 7449 |
. . . . . . . . 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 11668 |
. . . . . . . . . 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 12330 |
. . . . . . . . . . . . . 14
⊢ 3 = (2 +
1) |
| 167 | 28, 116 | addcomi 11452 |
. . . . . . . . . . . . . 14
⊢ (2 + 1) =
(1 + 2) |
| 168 | 166, 167 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 3 = (1 +
2) |
| 169 | 168 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (3
· (((𝐴 / 2)↑2)
/ 3)) = ((1 + 2) · (((𝐴 / 2)↑2) / 3)) |
| 170 | 125 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 · (((𝐴 /
2)↑2) / 3)) + (2 · (((𝐴 / 2)↑2) / 3))) = ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) /
3)))) |
| 171 | 115, 124,
29, 170 | joinlmuladdmuld 11288 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((1 + 2) · (((𝐴 /
2)↑2) / 3)) = ((((𝐴 /
2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))) |
| 172 | 169, 171 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(3 · (((𝐴 /
2)↑2) / 3)) = ((((𝐴 /
2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))) |
| 173 | 172 | oveq2d 7447 |
. . . . . . . . . 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 2780 |
. . . . . . . . 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 2781 |
. . . . . . . 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 5175 |
. . . . . . 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 11422 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) < ((1
− (((𝐴 / 2)↑2) /
3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3))))) |
| 178 | | ltmul2 12118 |
. . . . . . 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 1376 |
. . . . . 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 232 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1
− (2 · (((𝐴 /
2)↑2) / 3)))))) |
| 181 | 18 | recnd 11289 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) ∈ ℂ) |
| 182 | 27, 153, 181 | mulassd 11284 |
. . . . 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 5171 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1
− (2 · (((𝐴 /
2)↑2) / 3))))) |
| 184 | 13, 38 | remulcld 11291 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
| 185 | 74 | simpld 494 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(1 − (2 · (((𝐴
/ 2)↑2) / 3))) < (cos‘(𝐴 / 2))) |
| 186 | 1, 12, 45, 83 | mulgt0d 11416 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (𝐴 · (1
− (((𝐴 / 2)↑2) /
3)))) |
| 187 | | ltmul2 12118 |
. . . . . . 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 1376 |
. . . . . 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 232 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ·
(cos‘(𝐴 /
2)))) |
| 190 | 29, 34, 153 | mulassd 11284 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (𝐴 / 2))
· (1 − (((𝐴 /
2)↑2) / 3))) = (2 · ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) /
3))))) |
| 191 | 32 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (𝐴 / 2))
· (1 − (((𝐴 /
2)↑2) / 3))) = (𝐴
· (1 − (((𝐴 /
2)↑2) / 3)))) |
| 192 | 34, 115, 124 | subdid 11719 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (1
− (((𝐴 / 2)↑2) /
3))) = (((𝐴 / 2) ·
1) − ((𝐴 / 2)
· (((𝐴 / 2)↑2)
/ 3)))) |
| 193 | 34 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · 1) =
(𝐴 / 2)) |
| 194 | 166 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 / 2)↑3) = ((𝐴 / 2)↑(2 +
1)) |
| 195 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ0 |
| 196 | | expp1 14109 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 / 2) ∈ ℂ ∧ 2
∈ ℕ0) → ((𝐴 / 2)↑(2 + 1)) = (((𝐴 / 2)↑2) · (𝐴 / 2))) |
| 197 | 34, 195, 196 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑(2 + 1)) =
(((𝐴 / 2)↑2) ·
(𝐴 / 2))) |
| 198 | 194, 197 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) = (((𝐴 / 2)↑2) · (𝐴 / 2))) |
| 199 | 7 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑2) ∈
ℂ) |
| 200 | 199, 34 | mulcomd 11282 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑2) ·
(𝐴 / 2)) = ((𝐴 / 2) · ((𝐴 / 2)↑2))) |
| 201 | 198, 200 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) = ((𝐴 / 2) · ((𝐴 / 2)↑2))) |
| 202 | 201 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑3) / 3) =
(((𝐴 / 2) · ((𝐴 / 2)↑2)) /
3)) |
| 203 | | 3cn 12347 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
| 204 | 203 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 ∈ ℂ) |
| 205 | | 3ne0 12372 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
0 |
| 206 | 205 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (0(,)(π / 2)) →
3 ≠ 0) |
| 207 | 34, 199, 204, 206 | divassd 12078 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) · ((𝐴 / 2)↑2)) / 3) = ((𝐴 / 2) · (((𝐴 / 2)↑2) /
3))) |
| 208 | 202, 207 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (((𝐴 / 2)↑2) / 3)) = (((𝐴 / 2)↑3) /
3)) |
| 209 | 193, 208 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) · 1)
− ((𝐴 / 2) ·
(((𝐴 / 2)↑2) / 3))) =
((𝐴 / 2) − (((𝐴 / 2)↑3) /
3))) |
| 210 | 192, 209 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) · (1
− (((𝐴 / 2)↑2) /
3))) = ((𝐴 / 2) −
(((𝐴 / 2)↑3) /
3))) |
| 211 | 210 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((𝐴 / 2)
· (1 − (((𝐴 /
2)↑2) / 3)))) = (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)))) |
| 212 | 190, 191,
211 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3))) =
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3)))) |
| 213 | | sin01bnd 16221 |
. . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ (0(,]1) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ∧
(sin‘(𝐴 / 2)) <
(𝐴 / 2))) |
| 214 | 72, 213 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ∧
(sin‘(𝐴 / 2)) <
(𝐴 / 2))) |
| 215 | 214 | simpld 494 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 /
2))) |
| 216 | | 3nn0 12544 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
| 217 | | reexpcl 14119 |
. . . . . . . . . . . . 13
⊢ (((𝐴 / 2) ∈ ℝ ∧ 3
∈ ℕ0) → ((𝐴 / 2)↑3) ∈
ℝ) |
| 218 | 6, 216, 217 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2)↑3) ∈
ℝ) |
| 219 | | nndivre 12307 |
. . . . . . . . . . . 12
⊢ ((((𝐴 / 2)↑3) ∈ ℝ
∧ 3 ∈ ℕ) → (((𝐴 / 2)↑3) / 3) ∈
ℝ) |
| 220 | 218, 8, 219 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2)↑3) / 3)
∈ ℝ) |
| 221 | 6, 220 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈
ℝ) |
| 222 | 6 | resincld 16179 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(𝐴 / 2)) ∈
ℝ) |
| 223 | | ltmul2 12118 |
. . . . . . . . . 10
⊢ ((((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈
ℝ ∧ (sin‘(𝐴
/ 2)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ↔
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2))))) |
| 224 | 221, 222,
43, 47, 223 | syl112anc 1376 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) <
(sin‘(𝐴 / 2)) ↔
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2))))) |
| 225 | 215, 224 | mpbid 232 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · ((𝐴 / 2)
− (((𝐴 / 2)↑3) /
3))) < (2 · (sin‘(𝐴 / 2)))) |
| 226 | 212, 225 | eqbrtrd 5165 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
< (2 · (sin‘(𝐴 / 2)))) |
| 227 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (sin‘(𝐴 / 2)) ∈ ℝ) → (2 ·
(sin‘(𝐴 / 2))) ∈
ℝ) |
| 228 | 14, 222, 227 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(2 · (sin‘(𝐴 /
2))) ∈ ℝ) |
| 229 | | ltmul1 12117 |
. . . . . . . 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))))) |
| 230 | 13, 228, 38, 77, 229 | syl112anc 1376 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
< (2 · (sin‘(𝐴 / 2))) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ·
(cos‘(𝐴 / 2))) <
((2 · (sin‘(𝐴
/ 2))) · (cos‘(𝐴 / 2))))) |
| 231 | 226, 230 | mpbid 232 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2)))) |
| 232 | 222 | recnd 11289 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(𝐴 / 2)) ∈
ℂ) |
| 233 | 38 | recnd 11289 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘(𝐴 / 2)) ∈
ℂ) |
| 234 | 29, 232, 233 | mulassd 11284 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((2 · (sin‘(𝐴
/ 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 /
2))))) |
| 235 | | sin2t 16213 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 236 | 34, 235 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 237 | 32 | fveq2d 6910 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘(2 · (𝐴 /
2))) = (sin‘𝐴)) |
| 238 | 234, 236,
237 | 3eqtr2rd 2784 |
. . . . . 6
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(sin‘𝐴) = ((2
· (sin‘(𝐴 /
2))) · (cos‘(𝐴
/ 2)))) |
| 239 | 231, 238 | breqtrrd 5171 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (cos‘(𝐴 /
2))) < (sin‘𝐴)) |
| 240 | 19, 184, 20, 189, 239 | lttrd 11422 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 · (1 −
(((𝐴 / 2)↑2) / 3)))
· (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < (sin‘𝐴)) |
| 241 | 3, 19, 20, 183, 240 | lttrd 11422 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴)) |
| 242 | | sincosq1sgn 26540 |
. . . . 5
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
| 243 | 242 | simprd 495 |
. . . 4
⊢ (𝐴 ∈ (0(,)(π / 2)) →
0 < (cos‘𝐴)) |
| 244 | | ltmuldiv 12141 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(sin‘𝐴) ∈
ℝ ∧ ((cos‘𝐴) ∈ ℝ ∧ 0 <
(cos‘𝐴))) →
((𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴)))) |
| 245 | 1, 20, 2, 243, 244 | syl112anc 1376 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
((𝐴 ·
(cos‘𝐴)) <
(sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴)))) |
| 246 | 241, 245 | mpbid 232 |
. 2
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < ((sin‘𝐴) / (cos‘𝐴))) |
| 247 | 243 | gt0ne0d 11827 |
. . 3
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(cos‘𝐴) ≠
0) |
| 248 | | tanval 16164 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
| 249 | 27, 247, 248 | syl2anc 584 |
. 2
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
| 250 | 246, 249 | breqtrrd 5171 |
1
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 < (tan‘𝐴)) |