Step | Hyp | Ref
| Expression |
1 | | resinval 16024 |
. 2
β’ (π΄ β β β
(sinβπ΄) =
(ββ(expβ(i Β· π΄)))) |
2 | | recn 11148 |
. . . . 5
β’ (π΄ β β β π΄ β
β) |
3 | | efi4p.1 |
. . . . . 6
β’ πΉ = (π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ))) |
4 | 3 | efi4p 16026 |
. . . . 5
β’ (π΄ β β β
(expβ(i Β· π΄))
= (((1 β ((π΄β2)
/ 2)) + (i Β· (π΄
β ((π΄β3) / 6))))
+ Ξ£π β
(β€β₯β4)(πΉβπ))) |
5 | 2, 4 | syl 17 |
. . . 4
β’ (π΄ β β β
(expβ(i Β· π΄))
= (((1 β ((π΄β2)
/ 2)) + (i Β· (π΄
β ((π΄β3) / 6))))
+ Ξ£π β
(β€β₯β4)(πΉβπ))) |
6 | 5 | fveq2d 6851 |
. . 3
β’ (π΄ β β β
(ββ(expβ(i Β· π΄))) = (ββ(((1 β ((π΄β2) / 2)) + (i Β·
(π΄ β ((π΄β3) / 6)))) + Ξ£π β
(β€β₯β4)(πΉβπ)))) |
7 | | 1re 11162 |
. . . . . . 7
β’ 1 β
β |
8 | | resqcl 14036 |
. . . . . . . 8
β’ (π΄ β β β (π΄β2) β
β) |
9 | 8 | rehalfcld 12407 |
. . . . . . 7
β’ (π΄ β β β ((π΄β2) / 2) β
β) |
10 | | resubcl 11472 |
. . . . . . 7
β’ ((1
β β β§ ((π΄β2) / 2) β β) β (1
β ((π΄β2) / 2))
β β) |
11 | 7, 9, 10 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (1
β ((π΄β2) / 2))
β β) |
12 | 11 | recnd 11190 |
. . . . 5
β’ (π΄ β β β (1
β ((π΄β2) / 2))
β β) |
13 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
14 | | 3nn0 12438 |
. . . . . . . . . 10
β’ 3 β
β0 |
15 | | reexpcl 13991 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 3 β
β0) β (π΄β3) β β) |
16 | 14, 15 | mpan2 690 |
. . . . . . . . 9
β’ (π΄ β β β (π΄β3) β
β) |
17 | | 6re 12250 |
. . . . . . . . . 10
β’ 6 β
β |
18 | | 6pos 12270 |
. . . . . . . . . . 11
β’ 0 <
6 |
19 | 17, 18 | gt0ne0ii 11698 |
. . . . . . . . . 10
β’ 6 β
0 |
20 | | redivcl 11881 |
. . . . . . . . . 10
β’ (((π΄β3) β β β§ 6
β β β§ 6 β 0) β ((π΄β3) / 6) β
β) |
21 | 17, 19, 20 | mp3an23 1454 |
. . . . . . . . 9
β’ ((π΄β3) β β β
((π΄β3) / 6) β
β) |
22 | 16, 21 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β ((π΄β3) / 6) β
β) |
23 | | resubcl 11472 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π΄β3) / 6) β β)
β (π΄ β ((π΄β3) / 6)) β
β) |
24 | 22, 23 | mpdan 686 |
. . . . . . 7
β’ (π΄ β β β (π΄ β ((π΄β3) / 6)) β
β) |
25 | 24 | recnd 11190 |
. . . . . 6
β’ (π΄ β β β (π΄ β ((π΄β3) / 6)) β
β) |
26 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ (π΄
β ((π΄β3) / 6))
β β) β (i Β· (π΄ β ((π΄β3) / 6))) β
β) |
27 | 13, 25, 26 | sylancr 588 |
. . . . 5
β’ (π΄ β β β (i
Β· (π΄ β ((π΄β3) / 6))) β
β) |
28 | 12, 27 | addcld 11181 |
. . . 4
β’ (π΄ β β β ((1
β ((π΄β2) / 2)) +
(i Β· (π΄ β
((π΄β3) / 6)))) β
β) |
29 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
30 | 13, 2, 29 | sylancr 588 |
. . . . 5
β’ (π΄ β β β (i
Β· π΄) β
β) |
31 | | 4nn0 12439 |
. . . . 5
β’ 4 β
β0 |
32 | 3 | eftlcl 15996 |
. . . . 5
β’ (((i
Β· π΄) β β
β§ 4 β β0) β Ξ£π β
(β€β₯β4)(πΉβπ) β β) |
33 | 30, 31, 32 | sylancl 587 |
. . . 4
β’ (π΄ β β β
Ξ£π β
(β€β₯β4)(πΉβπ) β β) |
34 | 28, 33 | imaddd 15107 |
. . 3
β’ (π΄ β β β
(ββ(((1 β ((π΄β2) / 2)) + (i Β· (π΄ β ((π΄β3) / 6)))) + Ξ£π β
(β€β₯β4)(πΉβπ))) = ((ββ((1 β ((π΄β2) / 2)) + (i Β·
(π΄ β ((π΄β3) / 6))))) +
(ββΞ£π
β (β€β₯β4)(πΉβπ)))) |
35 | 11, 24 | crimd 15124 |
. . . 4
β’ (π΄ β β β
(ββ((1 β ((π΄β2) / 2)) + (i Β· (π΄ β ((π΄β3) / 6))))) = (π΄ β ((π΄β3) / 6))) |
36 | 35 | oveq1d 7377 |
. . 3
β’ (π΄ β β β
((ββ((1 β ((π΄β2) / 2)) + (i Β· (π΄ β ((π΄β3) / 6))))) +
(ββΞ£π
β (β€β₯β4)(πΉβπ))) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β
(β€β₯β4)(πΉβπ)))) |
37 | 6, 34, 36 | 3eqtrd 2781 |
. 2
β’ (π΄ β β β
(ββ(expβ(i Β· π΄))) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β
(β€β₯β4)(πΉβπ)))) |
38 | 1, 37 | eqtrd 2777 |
1
β’ (π΄ β β β
(sinβπ΄) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β
(β€β₯β4)(πΉβπ)))) |