Step | Hyp | Ref
| Expression |
1 | | nnuz 12815 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12543 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β 1 β β€) |
3 | | ax-icn 11119 |
. . . 4
β’ i β
β |
4 | | halfcl 12387 |
. . . 4
β’ (i β
β β (i / 2) β β) |
5 | 3, 4 | mp1i 13 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (i / 2) β β) |
6 | | simpl 483 |
. . . . . . . . 9
β’ ((π΄ β β β§
(absβπ΄) < 1)
β π΄ β
β) |
7 | | mulcl 11144 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
8 | 3, 6, 7 | sylancr 587 |
. . . . . . . 8
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (i Β· π΄)
β β) |
9 | 8 | negcld 11508 |
. . . . . . 7
β’ ((π΄ β β β§
(absβπ΄) < 1)
β -(i Β· π΄)
β β) |
10 | 8 | absnegd 15346 |
. . . . . . . . 9
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβ-(i Β· π΄)) = (absβ(i Β· π΄))) |
11 | | absmul 15191 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (absβ(i Β· π΄)) = ((absβi) Β·
(absβπ΄))) |
12 | 3, 6, 11 | sylancr 587 |
. . . . . . . . 9
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβ(i Β· π΄)) = ((absβi) Β·
(absβπ΄))) |
13 | | absi 15183 |
. . . . . . . . . . 11
β’
(absβi) = 1 |
14 | 13 | oveq1i 7372 |
. . . . . . . . . 10
β’
((absβi) Β· (absβπ΄)) = (1 Β· (absβπ΄)) |
15 | | abscl 15175 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
(absβπ΄) β
β) |
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβπ΄) β
β) |
17 | 16 | recnd 11192 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβπ΄) β
β) |
18 | 17 | mullidd 11182 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 Β· (absβπ΄)) = (absβπ΄)) |
19 | 14, 18 | eqtrid 2783 |
. . . . . . . . 9
β’ ((π΄ β β β§
(absβπ΄) < 1)
β ((absβi) Β· (absβπ΄)) = (absβπ΄)) |
20 | 10, 12, 19 | 3eqtrd 2775 |
. . . . . . . 8
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβ-(i Β· π΄)) = (absβπ΄)) |
21 | | simpr 485 |
. . . . . . . 8
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβπ΄) <
1) |
22 | 20, 21 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβ-(i Β· π΄)) < 1) |
23 | | logtayl 26052 |
. . . . . . 7
β’ ((-(i
Β· π΄) β β
β§ (absβ-(i Β· π΄)) < 1) β seq1( + , (π β β β¦ ((-(i
Β· π΄)βπ) / π))) β -(logβ(1 β -(i
Β· π΄)))) |
24 | 9, 22, 23 | syl2anc 584 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ ((-(i Β· π΄)βπ) / π))) β -(logβ(1 β -(i
Β· π΄)))) |
25 | | ax-1cn 11118 |
. . . . . . . . 9
β’ 1 β
β |
26 | | subneg 11459 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β -(i
Β· π΄)) = (1 + (i
Β· π΄))) |
27 | 25, 8, 26 | sylancr 587 |
. . . . . . . 8
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 β -(i Β· π΄)) = (1 + (i Β· π΄))) |
28 | 27 | fveq2d 6851 |
. . . . . . 7
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (logβ(1 β -(i Β· π΄))) = (logβ(1 + (i Β· π΄)))) |
29 | 28 | negeqd 11404 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β -(logβ(1 β -(i Β· π΄))) = -(logβ(1 + (i Β· π΄)))) |
30 | 24, 29 | breqtrd 5136 |
. . . . 5
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ ((-(i Β· π΄)βπ) / π))) β -(logβ(1 + (i Β·
π΄)))) |
31 | | seqex 13918 |
. . . . . 6
β’ seq1( + ,
(π β β β¦
(((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) β V |
32 | 31 | a1i 11 |
. . . . 5
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) β V) |
33 | 10, 22 | eqbrtrrd 5134 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (absβ(i Β· π΄)) < 1) |
34 | | logtayl 26052 |
. . . . . 6
β’ (((i
Β· π΄) β β
β§ (absβ(i Β· π΄)) < 1) β seq1( + , (π β β β¦ (((i
Β· π΄)βπ) / π))) β -(logβ(1 β (i
Β· π΄)))) |
35 | 8, 33, 34 | syl2anc 584 |
. . . . 5
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((i Β· π΄)βπ) / π))) β -(logβ(1 β (i
Β· π΄)))) |
36 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β (-(i Β· π΄)βπ) = (-(i Β· π΄)βπ)) |
37 | | id 22 |
. . . . . . . . . . 11
β’ (π = π β π = π) |
38 | 36, 37 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β ((-(i Β· π΄)βπ) / π) = ((-(i Β· π΄)βπ) / π)) |
39 | | eqid 2731 |
. . . . . . . . . 10
β’ (π β β β¦ ((-(i
Β· π΄)βπ) / π)) = (π β β β¦ ((-(i Β· π΄)βπ) / π)) |
40 | | ovex 7395 |
. . . . . . . . . 10
β’ ((-(i
Β· π΄)βπ) / π) β V |
41 | 38, 39, 40 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ ((-(i
Β· π΄)βπ) / π))βπ) = ((-(i Β· π΄)βπ) / π)) |
42 | 41 | adantl 482 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
((-(i Β· π΄)βπ) / π))βπ) = ((-(i Β· π΄)βπ) / π)) |
43 | | nnnn0 12429 |
. . . . . . . . . 10
β’ (π β β β π β
β0) |
44 | | expcl 13995 |
. . . . . . . . . 10
β’ ((-(i
Β· π΄) β β
β§ π β
β0) β (-(i Β· π΄)βπ) β β) |
45 | 9, 43, 44 | syl2an 596 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(-(i Β· π΄)βπ) β
β) |
46 | | nncn 12170 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
47 | 46 | adantl 482 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β
β) |
48 | | nnne0 12196 |
. . . . . . . . . 10
β’ (π β β β π β 0) |
49 | 48 | adantl 482 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β 0) |
50 | 45, 47, 49 | divcld 11940 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((-(i Β· π΄)βπ) / π) β β) |
51 | 42, 50 | eqeltrd 2832 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
((-(i Β· π΄)βπ) / π))βπ) β β) |
52 | 1, 2, 51 | serf 13946 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ ((-(i Β· π΄)βπ) / π))):ββΆβ) |
53 | 52 | ffvelcdmda 7040 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(seq1( + , (π β
β β¦ ((-(i Β· π΄)βπ) / π)))βπ) β β) |
54 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β ((i Β· π΄)βπ) = ((i Β· π΄)βπ)) |
55 | 54, 37 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (((i Β· π΄)βπ) / π) = (((i Β· π΄)βπ) / π)) |
56 | | eqid 2731 |
. . . . . . . . . 10
β’ (π β β β¦ (((i
Β· π΄)βπ) / π)) = (π β β β¦ (((i Β· π΄)βπ) / π)) |
57 | | ovex 7395 |
. . . . . . . . . 10
β’ (((i
Β· π΄)βπ) / π) β V |
58 | 55, 56, 57 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (((i
Β· π΄)βπ) / π))βπ) = (((i Β· π΄)βπ) / π)) |
59 | 58 | adantl 482 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
(((i Β· π΄)βπ) / π))βπ) = (((i Β· π΄)βπ) / π)) |
60 | | expcl 13995 |
. . . . . . . . . 10
β’ (((i
Β· π΄) β β
β§ π β
β0) β ((i Β· π΄)βπ) β β) |
61 | 8, 43, 60 | syl2an 596 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((i Β· π΄)βπ) β
β) |
62 | 61, 47, 49 | divcld 11940 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((i Β· π΄)βπ) / π) β β) |
63 | 59, 62 | eqeltrd 2832 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
(((i Β· π΄)βπ) / π))βπ) β β) |
64 | 1, 2, 63 | serf 13946 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((i Β· π΄)βπ) / π))):ββΆβ) |
65 | 64 | ffvelcdmda 7040 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(seq1( + , (π β
β β¦ (((i Β· π΄)βπ) / π)))βπ) β β) |
66 | | simpr 485 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β
β) |
67 | 66, 1 | eleqtrdi 2842 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β
(β€β₯β1)) |
68 | | simpl 483 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(π΄ β β β§
(absβπ΄) <
1)) |
69 | | elfznn 13480 |
. . . . . . 7
β’ (π β (1...π) β π β β) |
70 | 68, 69, 51 | syl2an 596 |
. . . . . 6
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
π β (1...π)) β ((π β β β¦ ((-(i Β· π΄)βπ) / π))βπ) β β) |
71 | 68, 69, 63 | syl2an 596 |
. . . . . 6
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
π β (1...π)) β ((π β β β¦ (((i Β· π΄)βπ) / π))βπ) β β) |
72 | 38, 55 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
73 | | eqid 2731 |
. . . . . . . . . 10
β’ (π β β β¦ (((-(i
Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) = (π β β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
74 | | ovex 7395 |
. . . . . . . . . 10
β’ (((-(i
Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)) β V |
75 | 72, 73, 74 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (((-(i
Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
76 | 75 | adantl 482 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
(((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
77 | 42, 59 | oveq12d 7380 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((π β β β¦
((-(i Β· π΄)βπ) / π))βπ) β ((π β β β¦ (((i Β· π΄)βπ) / π))βπ)) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
78 | 76, 77 | eqtr4d 2774 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
(((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ) = (((π β β β¦ ((-(i Β· π΄)βπ) / π))βπ) β ((π β β β¦ (((i Β· π΄)βπ) / π))βπ))) |
79 | 68, 69, 78 | syl2an 596 |
. . . . . 6
β’ ((((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β§
π β (1...π)) β ((π β β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ) = (((π β β β¦ ((-(i Β· π΄)βπ) / π))βπ) β ((π β β β¦ (((i Β· π΄)βπ) / π))βπ))) |
80 | 67, 70, 71, 79 | sersub 13961 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(seq1( + , (π β
β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))))βπ) = ((seq1( + , (π β β β¦ ((-(i Β· π΄)βπ) / π)))βπ) β (seq1( + , (π β β β¦ (((i Β· π΄)βπ) / π)))βπ))) |
81 | 1, 2, 30, 32, 35, 53, 65, 80 | climsub 15528 |
. . . 4
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) β (-(logβ(1 + (i Β·
π΄))) β -(logβ(1
β (i Β· π΄))))) |
82 | | addcl 11142 |
. . . . . . 7
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
83 | 25, 8, 82 | sylancr 587 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 + (i Β· π΄))
β β) |
84 | | bndatandm 26316 |
. . . . . . . 8
β’ ((π΄ β β β§
(absβπ΄) < 1)
β π΄ β dom
arctan) |
85 | | atandm2 26264 |
. . . . . . . 8
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
86 | 84, 85 | sylib 217 |
. . . . . . 7
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (π΄ β β
β§ (1 β (i Β· π΄)) β 0 β§ (1 + (i Β· π΄)) β 0)) |
87 | 86 | simp3d 1144 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 + (i Β· π΄))
β 0) |
88 | 83, 87 | logcld 25963 |
. . . . 5
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (logβ(1 + (i Β· π΄))) β β) |
89 | | subcl 11409 |
. . . . . . 7
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
90 | 25, 8, 89 | sylancr 587 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 β (i Β· π΄)) β β) |
91 | 86 | simp2d 1143 |
. . . . . 6
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (1 β (i Β· π΄)) β 0) |
92 | 90, 91 | logcld 25963 |
. . . . 5
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (logβ(1 β (i Β· π΄))) β β) |
93 | 88, 92 | neg2subd 11538 |
. . . 4
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (-(logβ(1 + (i Β· π΄))) β -(logβ(1 β (i
Β· π΄)))) =
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
94 | 81, 93 | breqtrd 5136 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) β ((logβ(1 β (i
Β· π΄))) β
(logβ(1 + (i Β· π΄))))) |
95 | 50, 62 | subcld 11521 |
. . . 4
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)) β β) |
96 | 76, 95 | eqeltrd 2832 |
. . 3
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π β β β¦
(((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ) β β) |
97 | 3 | a1i 11 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β i
β β) |
98 | | negicn 11411 |
. . . . . . . . 9
β’ -i β
β |
99 | 43 | adantl 482 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π β
β0) |
100 | | expcl 13995 |
. . . . . . . . 9
β’ ((-i
β β β§ π
β β0) β (-iβπ) β β) |
101 | 98, 99, 100 | sylancr 587 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(-iβπ) β
β) |
102 | | expcl 13995 |
. . . . . . . . 9
β’ ((i
β β β§ π
β β0) β (iβπ) β β) |
103 | 3, 99, 102 | sylancr 587 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(iβπ) β
β) |
104 | 101, 103 | subcld 11521 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((-iβπ) β
(iβπ)) β
β) |
105 | | 2cnd 12240 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β 2
β β) |
106 | | 2ne0 12266 |
. . . . . . . 8
β’ 2 β
0 |
107 | 106 | a1i 11 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β 2
β 0) |
108 | 97, 104, 105, 107 | div23d 11977 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((i Β· ((-iβπ)
β (iβπ))) / 2) =
((i / 2) Β· ((-iβπ) β (iβπ)))) |
109 | 108 | oveq1d 7377 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((i Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π)) = (((i / 2) Β· ((-iβπ) β (iβπ))) Β· ((π΄βπ) / π))) |
110 | 5 | adantr 481 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β (i
/ 2) β β) |
111 | | expcl 13995 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β (π΄βπ) β
β) |
112 | 6, 43, 111 | syl2an 596 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(π΄βπ) β β) |
113 | 112, 47, 49 | divcld 11940 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((π΄βπ) / π) β β) |
114 | 110, 104,
113 | mulassd 11187 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((i / 2) Β· ((-iβπ) β (iβπ))) Β· ((π΄βπ) / π)) = ((i / 2) Β· (((-iβπ) β (iβπ)) Β· ((π΄βπ) / π)))) |
115 | 101, 103,
112 | subdird 11621 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((-iβπ) β
(iβπ)) Β· (π΄βπ)) = (((-iβπ) Β· (π΄βπ)) β ((iβπ) Β· (π΄βπ)))) |
116 | 6 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
π΄ β
β) |
117 | | mulneg1 11600 |
. . . . . . . . . . . . 13
β’ ((i
β β β§ π΄
β β) β (-i Β· π΄) = -(i Β· π΄)) |
118 | 3, 116, 117 | sylancr 587 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(-i Β· π΄) = -(i
Β· π΄)) |
119 | 118 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((-i Β· π΄)βπ) = (-(i Β· π΄)βπ)) |
120 | 98 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β -i
β β) |
121 | 120, 116,
99 | mulexpd 14076 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((-i Β· π΄)βπ) = ((-iβπ) Β· (π΄βπ))) |
122 | 119, 121 | eqtr3d 2773 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(-(i Β· π΄)βπ) = ((-iβπ) Β· (π΄βπ))) |
123 | 97, 116, 99 | mulexpd 14076 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((i Β· π΄)βπ) = ((iβπ) Β· (π΄βπ))) |
124 | 122, 123 | oveq12d 7380 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((-(i Β· π΄)βπ) β ((i Β· π΄)βπ)) = (((-iβπ) Β· (π΄βπ)) β ((iβπ) Β· (π΄βπ)))) |
125 | 115, 124 | eqtr4d 2774 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((-iβπ) β
(iβπ)) Β· (π΄βπ)) = ((-(i Β· π΄)βπ) β ((i Β· π΄)βπ))) |
126 | 125 | oveq1d 7377 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((((-iβπ) β
(iβπ)) Β· (π΄βπ)) / π) = (((-(i Β· π΄)βπ) β ((i Β· π΄)βπ)) / π)) |
127 | 104, 112,
47, 49 | divassd 11975 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((((-iβπ) β
(iβπ)) Β· (π΄βπ)) / π) = (((-iβπ) β (iβπ)) Β· ((π΄βπ) / π))) |
128 | 45, 61, 47, 49 | divsubdird 11979 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((-(i Β· π΄)βπ) β ((i Β· π΄)βπ)) / π) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
129 | 126, 127,
128 | 3eqtr3d 2779 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((-iβπ) β
(iβπ)) Β·
((π΄βπ) / π)) = (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π))) |
130 | 129 | oveq2d 7378 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((i / 2) Β· (((-iβπ) β (iβπ)) Β· ((π΄βπ) / π))) = ((i / 2) Β· (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) |
131 | 109, 114,
130 | 3eqtrd 2775 |
. . . 4
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(((i Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π)) = ((i / 2) Β· (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) |
132 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (-iβπ) = (-iβπ)) |
133 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (iβπ) = (iβπ)) |
134 | 132, 133 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((-iβπ) β (iβπ)) = ((-iβπ) β (iβπ))) |
135 | 134 | oveq2d 7378 |
. . . . . . . 8
β’ (π = π β (i Β· ((-iβπ) β (iβπ))) = (i Β·
((-iβπ) β
(iβπ)))) |
136 | 135 | oveq1d 7377 |
. . . . . . 7
β’ (π = π β ((i Β· ((-iβπ) β (iβπ))) / 2) = ((i Β·
((-iβπ) β
(iβπ))) /
2)) |
137 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (π΄βπ) = (π΄βπ)) |
138 | 137, 37 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β ((π΄βπ) / π) = ((π΄βπ) / π)) |
139 | 136, 138 | oveq12d 7380 |
. . . . . 6
β’ (π = π β (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π)) = (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))) |
140 | | atantayl.1 |
. . . . . 6
β’ πΉ = (π β β β¦ (((i Β·
((-iβπ) β
(iβπ))) / 2) Β·
((π΄βπ) / π))) |
141 | | ovex 7395 |
. . . . . 6
β’ (((i
Β· ((-iβπ)
β (iβπ))) / 2)
Β· ((π΄βπ) / π)) β V |
142 | 139, 140,
141 | fvmpt 6953 |
. . . . 5
β’ (π β β β (πΉβπ) = (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))) |
143 | 142 | adantl 482 |
. . . 4
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(πΉβπ) = (((i Β· ((-iβπ) β (iβπ))) / 2) Β· ((π΄βπ) / π))) |
144 | 76 | oveq2d 7378 |
. . . 4
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
((i / 2) Β· ((π
β β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ)) = ((i / 2) Β· (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))) |
145 | 131, 143,
144 | 3eqtr4d 2781 |
. . 3
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β β) β
(πΉβπ) = ((i / 2) Β· ((π β β β¦ (((-(i Β· π΄)βπ) / π) β (((i Β· π΄)βπ) / π)))βπ))) |
146 | 1, 2, 5, 94, 96, 145 | isermulc2 15554 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , πΉ) β
((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
147 | | atanval 26271 |
. . 3
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
148 | 84, 147 | syl 17 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (arctanβπ΄) =
((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
149 | 146, 148 | breqtrrd 5138 |
1
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , πΉ) β
(arctanβπ΄)) |