Step | Hyp | Ref
| Expression |
1 | | atantayl2.1 |
. . . 4
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, ((-1β((π β 1) / 2)) Β·
((π΄βπ) / π)))) |
2 | | ax-icn 11171 |
. . . . . . . . . . . . . . . 16
β’ i β
β |
3 | 2 | negcli 11530 |
. . . . . . . . . . . . . . 15
β’ -i β
β |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β -i β
β) |
5 | | nnnn0 12481 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β0) |
6 | 5 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β π β
β0) |
7 | 4, 6 | expcld 14113 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(-iβπ) β
β) |
8 | | sqneg 14083 |
. . . . . . . . . . . . . . . . 17
β’ (i β
β β (-iβ2) = (iβ2)) |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(-iβ2) = (iβ2) |
10 | 9 | oveq1i 7421 |
. . . . . . . . . . . . . . 15
β’
((-iβ2)β(π
/ 2)) = ((iβ2)β(π
/ 2)) |
11 | | ine0 11651 |
. . . . . . . . . . . . . . . . . 18
β’ i β
0 |
12 | 2, 11 | negne0i 11537 |
. . . . . . . . . . . . . . . . 17
β’ -i β
0 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β -i β
0) |
14 | | 2z 12596 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β€ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β 2 β
β€) |
16 | | 2ne0 12318 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
0 |
17 | | nnz 12581 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β€) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β
β€) |
19 | | dvdsval2 16202 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β€ β§ 2 β 0 β§ π β β€) β (2 β₯ π β (π / 2) β β€)) |
20 | 14, 16, 18, 19 | mp3an12i 1465 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β (2
β₯ π β (π / 2) β
β€)) |
21 | 20 | biimpa 477 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (π / 2) β
β€) |
22 | | expmulz 14076 |
. . . . . . . . . . . . . . . 16
β’ (((-i
β β β§ -i β 0) β§ (2 β β€ β§ (π / 2) β β€)) β
(-iβ(2 Β· (π /
2))) = ((-iβ2)β(π
/ 2))) |
23 | 4, 13, 15, 21, 22 | syl22anc 837 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(-iβ(2 Β· (π /
2))) = ((-iβ2)β(π
/ 2))) |
24 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β i β
β) |
25 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β i β
0) |
26 | | expmulz 14076 |
. . . . . . . . . . . . . . . 16
β’ (((i
β β β§ i β 0) β§ (2 β β€ β§ (π / 2) β β€)) β
(iβ(2 Β· (π /
2))) = ((iβ2)β(π
/ 2))) |
27 | 24, 25, 15, 21, 26 | syl22anc 837 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(iβ(2 Β· (π /
2))) = ((iβ2)β(π
/ 2))) |
28 | 10, 23, 27 | 3eqtr4a 2798 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(-iβ(2 Β· (π /
2))) = (iβ(2 Β· (π / 2)))) |
29 | | nncn 12222 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
30 | 29 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β π β
β) |
31 | | 2cnd 12292 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β 2 β
β) |
32 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β 2 β
0) |
33 | 30, 31, 32 | divcan2d 11994 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (2
Β· (π / 2)) = π) |
34 | 33 | oveq2d 7427 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(-iβ(2 Β· (π /
2))) = (-iβπ)) |
35 | 33 | oveq2d 7427 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(iβ(2 Β· (π /
2))) = (iβπ)) |
36 | 28, 34, 35 | 3eqtr3d 2780 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
(-iβπ) = (iβπ)) |
37 | 7, 36 | subeq0bd 11642 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β
((-iβπ) β
(iβπ)) =
0) |
38 | 37 | oveq2d 7427 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (i
Β· ((-iβπ)
β (iβπ))) = (i
Β· 0)) |
39 | | it0e0 12436 |
. . . . . . . . . . 11
β’ (i
Β· 0) = 0 |
40 | 38, 39 | eqtrdi 2788 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (i
Β· ((-iβπ)
β (iβπ))) =
0) |
41 | 40 | oveq1d 7426 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β ((i
Β· ((-iβπ)
β (iβπ))) / 2) =
(0 / 2)) |
42 | | 2cn 12289 |
. . . . . . . . . 10
β’ 2 β
β |
43 | 42, 16 | div0i 11950 |
. . . . . . . . 9
β’ (0 / 2) =
0 |
44 | 41, 43 | eqtrdi 2788 |
. . . . . . . 8
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β ((i
Β· ((-iβπ)
β (iβπ))) / 2) =
0) |
45 | 44 | oveq1d 7426 |
. . . . . . 7
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (((i
Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π)) = (0 Β· ((π΄βπ) / π))) |
46 | | simplll 773 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β π΄ β
β) |
47 | 46, 6 | expcld 14113 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (π΄βπ) β β) |
48 | | nnne0 12248 |
. . . . . . . . . 10
β’ (π β β β π β 0) |
49 | 48 | ad2antlr 725 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β π β 0) |
50 | 47, 30, 49 | divcld 11992 |
. . . . . . . 8
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β ((π΄βπ) / π) β β) |
51 | 50 | mul02d 11414 |
. . . . . . 7
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β (0
Β· ((π΄βπ) / π)) = 0) |
52 | 45, 51 | eqtr2d 2773 |
. . . . . 6
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§ 2
β₯ π) β 0 = (((i
Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π))) |
53 | | 2cnd 12292 |
. . . . . . . 8
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β 2
β β) |
54 | | ax-1cn 11170 |
. . . . . . . . . . 11
β’ 1 β
β |
55 | 54 | negcli 11530 |
. . . . . . . . . 10
β’ -1 β
β |
56 | 55 | a1i 11 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
-1 β β) |
57 | | neg1ne0 12330 |
. . . . . . . . . 10
β’ -1 β
0 |
58 | 57 | a1i 11 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
-1 β 0) |
59 | 29 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
π β
β) |
60 | | peano2cn 11388 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) β
β) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(π + 1) β
β) |
62 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β 2
β 0) |
63 | 61, 53, 53, 62 | divsubdird 12031 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(((π + 1) β 2) / 2) =
(((π + 1) / 2) β (2 /
2))) |
64 | | 2div2e1 12355 |
. . . . . . . . . . . . 13
β’ (2 / 2) =
1 |
65 | 64 | oveq2i 7422 |
. . . . . . . . . . . 12
β’ (((π + 1) / 2) β (2 / 2)) =
(((π + 1) / 2) β
1) |
66 | 63, 65 | eqtrdi 2788 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(((π + 1) β 2) / 2) =
(((π + 1) / 2) β
1)) |
67 | | df-2 12277 |
. . . . . . . . . . . . . 14
β’ 2 = (1 +
1) |
68 | 67 | oveq2i 7422 |
. . . . . . . . . . . . 13
β’ ((π + 1) β 2) = ((π + 1) β (1 +
1)) |
69 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β 1
β β) |
70 | 59, 69, 69 | pnpcan2d 11611 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((π + 1) β (1 + 1)) =
(π β
1)) |
71 | 68, 70 | eqtrid 2784 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((π + 1) β 2) =
(π β
1)) |
72 | 71 | oveq1d 7426 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(((π + 1) β 2) / 2) =
((π β 1) /
2)) |
73 | 66, 72 | eqtr3d 2774 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(((π + 1) / 2) β 1) =
((π β 1) /
2)) |
74 | 20 | notbid 317 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(Β¬ 2 β₯ π β
Β¬ (π / 2) β
β€)) |
75 | | zeo 12650 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β ((π / 2) β β€ β¨
((π + 1) / 2) β
β€)) |
76 | 18, 75 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π / 2) β β€
β¨ ((π + 1) / 2) β
β€)) |
77 | 76 | ord 862 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(Β¬ (π / 2) β
β€ β ((π + 1) /
2) β β€)) |
78 | 74, 77 | sylbid 239 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(Β¬ 2 β₯ π β
((π + 1) / 2) β
β€)) |
79 | 78 | imp 407 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((π + 1) / 2) β
β€) |
80 | | peano2zm 12607 |
. . . . . . . . . . 11
β’ (((π + 1) / 2) β β€ β
(((π + 1) / 2) β 1)
β β€) |
81 | 79, 80 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(((π + 1) / 2) β 1)
β β€) |
82 | 73, 81 | eqeltrrd 2834 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((π β 1) / 2) β
β€) |
83 | 56, 58, 82 | expclzd 14118 |
. . . . . . . 8
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-1β((π β 1) /
2)) β β) |
84 | 83 | 2timesd 12457 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(2 Β· (-1β((π
β 1) / 2))) = ((-1β((π β 1) / 2)) + (-1β((π β 1) /
2)))) |
85 | | subcl 11461 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β (π β
1) β β) |
86 | 59, 54, 85 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(π β 1) β
β) |
87 | 86, 53, 62 | divcan2d 11994 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(2 Β· ((π β 1)
/ 2)) = (π β
1)) |
88 | 87 | oveq2d 7427 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-iβ(2 Β· ((π
β 1) / 2))) = (-iβ(π β 1))) |
89 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
-i β β) |
90 | 12 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
-i β 0) |
91 | 17 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
π β
β€) |
92 | 89, 90, 91 | expm1d 14123 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-iβ(π β 1)) =
((-iβπ) /
-i)) |
93 | 88, 92 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-iβ(2 Β· ((π
β 1) / 2))) = ((-iβπ) / -i)) |
94 | 14 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β 2
β β€) |
95 | | expmulz 14076 |
. . . . . . . . . . . . 13
β’ (((-i
β β β§ -i β 0) β§ (2 β β€ β§ ((π β 1) / 2) β
β€)) β (-iβ(2 Β· ((π β 1) / 2))) =
((-iβ2)β((π
β 1) / 2))) |
96 | 89, 90, 94, 82, 95 | syl22anc 837 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-iβ(2 Β· ((π
β 1) / 2))) = ((-iβ2)β((π β 1) / 2))) |
97 | 5 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
π β
β0) |
98 | | expcl 14047 |
. . . . . . . . . . . . . 14
β’ ((-i
β β β§ π
β β0) β (-iβπ) β β) |
99 | 3, 97, 98 | sylancr 587 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-iβπ) β
β) |
100 | 99, 89, 90 | divrec2d 11996 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((-iβπ) / -i) = ((1 /
-i) Β· (-iβπ))) |
101 | 93, 96, 100 | 3eqtr3d 2780 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((-iβ2)β((π
β 1) / 2)) = ((1 / -i) Β· (-iβπ))) |
102 | | i2 14168 |
. . . . . . . . . . . . 13
β’
(iβ2) = -1 |
103 | 9, 102 | eqtri 2760 |
. . . . . . . . . . . 12
β’
(-iβ2) = -1 |
104 | 103 | oveq1i 7421 |
. . . . . . . . . . 11
β’
((-iβ2)β((π β 1) / 2)) = (-1β((π β 1) /
2)) |
105 | | irec 14167 |
. . . . . . . . . . . . . 14
β’ (1 / i) =
-i |
106 | 105 | negeqi 11455 |
. . . . . . . . . . . . 13
β’ -(1 / i)
= --i |
107 | | divneg2 11940 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ i β β β§ i β 0) β -(1 / i) = (1 /
-i)) |
108 | 54, 2, 11, 107 | mp3an 1461 |
. . . . . . . . . . . . 13
β’ -(1 / i)
= (1 / -i) |
109 | 2 | negnegi 11532 |
. . . . . . . . . . . . 13
β’ --i =
i |
110 | 106, 108,
109 | 3eqtr3i 2768 |
. . . . . . . . . . . 12
β’ (1 / -i)
= i |
111 | 110 | oveq1i 7421 |
. . . . . . . . . . 11
β’ ((1 / -i)
Β· (-iβπ)) = (i
Β· (-iβπ)) |
112 | 101, 104,
111 | 3eqtr3g 2795 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-1β((π β 1) /
2)) = (i Β· (-iβπ))) |
113 | 87 | oveq2d 7427 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(iβ(2 Β· ((π
β 1) / 2))) = (iβ(π β 1))) |
114 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β i
β β) |
115 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β i
β 0) |
116 | 114, 115,
91 | expm1d 14123 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(iβ(π β 1)) =
((iβπ) /
i)) |
117 | 113, 116 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(iβ(2 Β· ((π
β 1) / 2))) = ((iβπ) / i)) |
118 | | expmulz 14076 |
. . . . . . . . . . . . . 14
β’ (((i
β β β§ i β 0) β§ (2 β β€ β§ ((π β 1) / 2) β
β€)) β (iβ(2 Β· ((π β 1) / 2))) = ((iβ2)β((π β 1) /
2))) |
119 | 114, 115,
94, 82, 118 | syl22anc 837 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(iβ(2 Β· ((π
β 1) / 2))) = ((iβ2)β((π β 1) / 2))) |
120 | | expcl 14047 |
. . . . . . . . . . . . . . 15
β’ ((i
β β β§ π
β β0) β (iβπ) β β) |
121 | 2, 97, 120 | sylancr 587 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(iβπ) β
β) |
122 | 121, 114,
115 | divrec2d 11996 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((iβπ) / i) = ((1 / i)
Β· (iβπ))) |
123 | 117, 119,
122 | 3eqtr3d 2780 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((iβ2)β((π
β 1) / 2)) = ((1 / i) Β· (iβπ))) |
124 | 102 | oveq1i 7421 |
. . . . . . . . . . . 12
β’
((iβ2)β((π
β 1) / 2)) = (-1β((π β 1) / 2)) |
125 | 105 | oveq1i 7421 |
. . . . . . . . . . . 12
β’ ((1 / i)
Β· (iβπ)) = (-i
Β· (iβπ)) |
126 | 123, 124,
125 | 3eqtr3g 2795 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-1β((π β 1) /
2)) = (-i Β· (iβπ))) |
127 | | mulneg1 11652 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (iβπ) β β) β (-i Β·
(iβπ)) = -(i Β·
(iβπ))) |
128 | 2, 121, 127 | sylancr 587 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-i Β· (iβπ)) =
-(i Β· (iβπ))) |
129 | 126, 128 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-1β((π β 1) /
2)) = -(i Β· (iβπ))) |
130 | 112, 129 | oveq12d 7429 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((-1β((π β 1) /
2)) + (-1β((π β
1) / 2))) = ((i Β· (-iβπ)) + -(i Β· (iβπ)))) |
131 | | mulcl 11196 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (-iβπ) β β) β (i Β·
(-iβπ)) β
β) |
132 | 2, 99, 131 | sylancr 587 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(i Β· (-iβπ))
β β) |
133 | | mulcl 11196 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (iβπ) β β) β (i Β·
(iβπ)) β
β) |
134 | 2, 121, 133 | sylancr 587 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(i Β· (iβπ))
β β) |
135 | 132, 134 | negsubd 11579 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((i Β· (-iβπ)) +
-(i Β· (iβπ))) =
((i Β· (-iβπ))
β (i Β· (iβπ)))) |
136 | 114, 99, 121 | subdid 11672 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(i Β· ((-iβπ)
β (iβπ))) = ((i
Β· (-iβπ))
β (i Β· (iβπ)))) |
137 | 135, 136 | eqtr4d 2775 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((i Β· (-iβπ)) +
-(i Β· (iβπ))) =
(i Β· ((-iβπ)
β (iβπ)))) |
138 | 84, 130, 137 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(2 Β· (-1β((π
β 1) / 2))) = (i Β· ((-iβπ) β (iβπ)))) |
139 | 53, 83, 62, 138 | mvllmuld 12048 |
. . . . . . 7
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
(-1β((π β 1) /
2)) = ((i Β· ((-iβπ) β (iβπ))) / 2)) |
140 | 139 | oveq1d 7426 |
. . . . . 6
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
Β¬ 2 β₯ π) β
((-1β((π β 1) /
2)) Β· ((π΄βπ) / π)) = (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))) |
141 | 52, 140 | ifeqda 4564 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
if(2 β₯ π, 0,
((-1β((π β 1) /
2)) Β· ((π΄βπ) / π))) = (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))) |
142 | 141 | mpteq2dva 5248 |
. . . 4
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (π β β
β¦ if(2 β₯ π, 0,
((-1β((π β 1) /
2)) Β· ((π΄βπ) / π)))) = (π β β β¦ (((i Β·
((-iβπ) β
(iβπ))) / 2) Β·
((π΄βπ) / π)))) |
143 | 1, 142 | eqtrid 2784 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β πΉ = (π β β β¦ (((i
Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π)))) |
144 | 143 | seqeq3d 13976 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , πΉ) = seq1(
+ , (π β β
β¦ (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))))) |
145 | | eqid 2732 |
. . 3
β’ (π β β β¦ (((i
Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π))) = (π β β β¦ (((i Β·
((-iβπ) β
(iβπ))) / 2) Β·
((π΄βπ) / π))) |
146 | 145 | atantayl 26449 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π)))) β (arctanβπ΄)) |
147 | 144, 146 | eqbrtrd 5170 |
1
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , πΉ) β
(arctanβπ΄)) |