Step | Hyp | Ref
| Expression |
1 | | cnvimass 6034 |
. . . 4
β’ (β‘β β π·) β dom β |
2 | | eff1olem.2 |
. . . 4
β’ π = (β‘β β π·) |
3 | | imf 15004 |
. . . . . 6
β’
β:ββΆβ |
4 | 3 | fdmi 6681 |
. . . . 5
β’ dom
β = β |
5 | 4 | eqcomi 2742 |
. . . 4
β’ β =
dom β |
6 | 1, 2, 5 | 3sstr4i 3988 |
. . 3
β’ π β
β |
7 | | eff2 15986 |
. . . . . . 7
β’
exp:ββΆ(β β {0}) |
8 | 7 | a1i 11 |
. . . . . 6
β’ (π β β β
exp:ββΆ(β β {0})) |
9 | 8 | feqmptd 6911 |
. . . . 5
β’ (π β β β exp =
(π¦ β β β¦
(expβπ¦))) |
10 | 9 | reseq1d 5937 |
. . . 4
β’ (π β β β (exp
βΎ π) = ((π¦ β β β¦
(expβπ¦)) βΎ
π)) |
11 | | resmpt 5992 |
. . . 4
β’ (π β β β ((π¦ β β β¦
(expβπ¦)) βΎ
π) = (π¦ β π β¦ (expβπ¦))) |
12 | 10, 11 | eqtrd 2773 |
. . 3
β’ (π β β β (exp
βΎ π) = (π¦ β π β¦ (expβπ¦))) |
13 | 6, 12 | ax-mp 5 |
. 2
β’ (exp
βΎ π) = (π¦ β π β¦ (expβπ¦)) |
14 | 6 | sseli 3941 |
. . . 4
β’ (π¦ β π β π¦ β β) |
15 | 7 | ffvelcdmi 7035 |
. . . 4
β’ (π¦ β β β
(expβπ¦) β
(β β {0})) |
16 | 14, 15 | syl 17 |
. . 3
β’ (π¦ β π β (expβπ¦) β (β β
{0})) |
17 | 16 | adantl 483 |
. 2
β’ ((π β§ π¦ β π) β (expβπ¦) β (β β
{0})) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β β {0})) β π₯ β (β β
{0})) |
19 | | eldifsn 4748 |
. . . . . . . . . 10
β’ (π₯ β (β β {0})
β (π₯ β β
β§ π₯ β
0)) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β β {0})) β (π₯ β β β§ π₯ β 0)) |
21 | 20 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β π₯ β
β) |
22 | 20 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β π₯ β 0) |
23 | 21, 22 | absrpcld 15339 |
. . . . . . 7
β’ ((π β§ π₯ β (β β {0})) β
(absβπ₯) β
β+) |
24 | | reeff1o 25822 |
. . . . . . . . 9
β’ (exp
βΎ β):ββ1-1-ontoββ+ |
25 | | f1ocnv 6797 |
. . . . . . . . 9
β’ ((exp
βΎ β):ββ1-1-ontoββ+ β β‘(exp βΎ
β):β+β1-1-ontoββ) |
26 | | f1of 6785 |
. . . . . . . . 9
β’ (β‘(exp βΎ
β):β+β1-1-ontoββ β β‘(exp βΎ
β):β+βΆβ) |
27 | 24, 25, 26 | mp2b 10 |
. . . . . . . 8
β’ β‘(exp βΎ
β):β+βΆβ |
28 | 27 | ffvelcdmi 7035 |
. . . . . . 7
β’
((absβπ₯)
β β+ β (β‘(exp βΎ β)β(absβπ₯)) β
β) |
29 | 23, 28 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β (β β {0})) β (β‘(exp βΎ β)β(absβπ₯)) β
β) |
30 | 29 | recnd 11188 |
. . . . 5
β’ ((π β§ π₯ β (β β {0})) β (β‘(exp βΎ β)β(absβπ₯)) β
β) |
31 | | ax-icn 11115 |
. . . . . 6
β’ i β
β |
32 | | eff1olem.3 |
. . . . . . . . 9
β’ (π β π· β β) |
33 | 32 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β π· β
β) |
34 | | eff1olem.1 |
. . . . . . . . . . . 12
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) |
35 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (β‘abs β {1}) = (β‘abs β {1}) |
36 | | eff1olem.4 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) |
37 | | eff1olem.5 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β
β€) |
38 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (sin
βΎ (-(Ο / 2)[,](Ο / 2))) = (sin βΎ (-(Ο / 2)[,](Ο /
2))) |
39 | 34, 35, 32, 36, 37, 38 | efif1olem4 25917 |
. . . . . . . . . . 11
β’ (π β πΉ:π·β1-1-ontoβ(β‘abs
β {1})) |
40 | | f1ocnv 6797 |
. . . . . . . . . . 11
β’ (πΉ:π·β1-1-ontoβ(β‘abs
β {1}) β β‘πΉ:(β‘abs β {1})β1-1-ontoβπ·) |
41 | | f1of 6785 |
. . . . . . . . . . 11
β’ (β‘πΉ:(β‘abs β {1})β1-1-ontoβπ· β β‘πΉ:(β‘abs β {1})βΆπ·) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . 10
β’ (π β β‘πΉ:(β‘abs β {1})βΆπ·) |
43 | 42 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β β {0})) β β‘πΉ:(β‘abs β {1})βΆπ·) |
44 | 21 | abscld 15327 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (β β {0})) β
(absβπ₯) β
β) |
45 | 44 | recnd 11188 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β β {0})) β
(absβπ₯) β
β) |
46 | 21, 22 | absne0d 15338 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β β {0})) β
(absβπ₯) β
0) |
47 | 21, 45, 46 | divcld 11936 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β β {0})) β (π₯ / (absβπ₯)) β β) |
48 | 21, 45, 46 | absdivd 15346 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β β {0})) β
(absβ(π₯ /
(absβπ₯))) =
((absβπ₯) /
(absβ(absβπ₯)))) |
49 | | absidm 15214 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
(absβ(absβπ₯)) =
(absβπ₯)) |
50 | 21, 49 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (β β {0})) β
(absβ(absβπ₯)) =
(absβπ₯)) |
51 | 50 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β β {0})) β
((absβπ₯) /
(absβ(absβπ₯)))
= ((absβπ₯) /
(absβπ₯))) |
52 | 45, 46 | dividd 11934 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β β {0})) β
((absβπ₯) /
(absβπ₯)) =
1) |
53 | 48, 51, 52 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β β {0})) β
(absβ(π₯ /
(absβπ₯))) =
1) |
54 | | absf 15228 |
. . . . . . . . . . 11
β’
abs:ββΆβ |
55 | | ffn 6669 |
. . . . . . . . . . 11
β’
(abs:ββΆβ β abs Fn β) |
56 | | fniniseg 7011 |
. . . . . . . . . . 11
β’ (abs Fn
β β ((π₯ /
(absβπ₯)) β
(β‘abs β {1}) β ((π₯ / (absβπ₯)) β β β§ (absβ(π₯ / (absβπ₯))) = 1))) |
57 | 54, 55, 56 | mp2b 10 |
. . . . . . . . . 10
β’ ((π₯ / (absβπ₯)) β (β‘abs β {1}) β ((π₯ / (absβπ₯)) β β β§ (absβ(π₯ / (absβπ₯))) = 1)) |
58 | 47, 53, 57 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β β {0})) β (π₯ / (absβπ₯)) β (β‘abs β {1})) |
59 | 43, 58 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β (β‘πΉβ(π₯ / (absβπ₯))) β π·) |
60 | 33, 59 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ π₯ β (β β {0})) β (β‘πΉβ(π₯ / (absβπ₯))) β β) |
61 | 60 | recnd 11188 |
. . . . . 6
β’ ((π β§ π₯ β (β β {0})) β (β‘πΉβ(π₯ / (absβπ₯))) β β) |
62 | | mulcl 11140 |
. . . . . 6
β’ ((i
β β β§ (β‘πΉβ(π₯ / (absβπ₯))) β β) β (i Β· (β‘πΉβ(π₯ / (absβπ₯)))) β β) |
63 | 31, 61, 62 | sylancr 588 |
. . . . 5
β’ ((π β§ π₯ β (β β {0})) β (i
Β· (β‘πΉβ(π₯ / (absβπ₯)))) β β) |
64 | 30, 63 | addcld 11179 |
. . . 4
β’ ((π β§ π₯ β (β β {0})) β ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β β) |
65 | 29, 60 | crimd 15123 |
. . . . 5
β’ ((π β§ π₯ β (β β {0})) β
(ββ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) = (β‘πΉβ(π₯ / (absβπ₯)))) |
66 | 65, 59 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π₯ β (β β {0})) β
(ββ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) β π·) |
67 | | ffn 6669 |
. . . . 5
β’
(β:ββΆβ β β Fn
β) |
68 | | elpreima 7009 |
. . . . 5
β’ (β
Fn β β (((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β (β‘β β π·) β (((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β β β§
(ββ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) β π·))) |
69 | 3, 67, 68 | mp2b 10 |
. . . 4
β’ (((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β (β‘β β π·) β (((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β β β§
(ββ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) β π·)) |
70 | 64, 66, 69 | sylanbrc 584 |
. . 3
β’ ((π β§ π₯ β (β β {0})) β ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β (β‘β β π·)) |
71 | 70, 2 | eleqtrrdi 2845 |
. 2
β’ ((π β§ π₯ β (β β {0})) β ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β π) |
72 | | efadd 15981 |
. . . . . . 7
β’ (((β‘(exp βΎ β)β(absβπ₯)) β β β§ (i
Β· (β‘πΉβ(π₯ / (absβπ₯)))) β β) β
(expβ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) = ((expβ(β‘(exp βΎ β)β(absβπ₯))) Β· (expβ(i
Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
73 | 30, 63, 72 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β (β β {0})) β
(expβ((β‘(exp βΎ
β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) = ((expβ(β‘(exp βΎ β)β(absβπ₯))) Β· (expβ(i
Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
74 | 29 | fvresd 6863 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β ((exp
βΎ β)β(β‘(exp βΎ
β)β(absβπ₯))) = (expβ(β‘(exp βΎ β)β(absβπ₯)))) |
75 | | f1ocnvfv2 7224 |
. . . . . . . . 9
β’ (((exp
βΎ β):ββ1-1-ontoββ+ β§
(absβπ₯) β
β+) β ((exp βΎ β)β(β‘(exp βΎ β)β(absβπ₯))) = (absβπ₯)) |
76 | 24, 23, 75 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β ((exp
βΎ β)β(β‘(exp βΎ
β)β(absβπ₯))) = (absβπ₯)) |
77 | 74, 76 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ π₯ β (β β {0})) β
(expβ(β‘(exp βΎ
β)β(absβπ₯))) = (absβπ₯)) |
78 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π§ = (β‘πΉβ(π₯ / (absβπ₯))) β (i Β· π§) = (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) |
79 | 78 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π§ = (β‘πΉβ(π₯ / (absβπ₯))) β (expβ(i Β· π§)) = (expβ(i Β·
(β‘πΉβ(π₯ / (absβπ₯)))))) |
80 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β (i Β· π€) = (i Β· π§)) |
81 | 80 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π€ = π§ β (expβ(i Β· π€)) = (expβ(i Β·
π§))) |
82 | 81 | cbvmptv 5219 |
. . . . . . . . . . 11
β’ (π€ β π· β¦ (expβ(i Β· π€))) = (π§ β π· β¦ (expβ(i Β· π§))) |
83 | 34, 82 | eqtri 2761 |
. . . . . . . . . 10
β’ πΉ = (π§ β π· β¦ (expβ(i Β· π§))) |
84 | | fvex 6856 |
. . . . . . . . . 10
β’
(expβ(i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β V |
85 | 79, 83, 84 | fvmpt 6949 |
. . . . . . . . 9
β’ ((β‘πΉβ(π₯ / (absβπ₯))) β π· β (πΉβ(β‘πΉβ(π₯ / (absβπ₯)))) = (expβ(i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) |
86 | 59, 85 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β (πΉβ(β‘πΉβ(π₯ / (absβπ₯)))) = (expβ(i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) |
87 | 39 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β β {0})) β πΉ:π·β1-1-ontoβ(β‘abs
β {1})) |
88 | | f1ocnvfv2 7224 |
. . . . . . . . 9
β’ ((πΉ:π·β1-1-ontoβ(β‘abs
β {1}) β§ (π₯ /
(absβπ₯)) β
(β‘abs β {1})) β (πΉβ(β‘πΉβ(π₯ / (absβπ₯)))) = (π₯ / (absβπ₯))) |
89 | 87, 58, 88 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β (β β {0})) β (πΉβ(β‘πΉβ(π₯ / (absβπ₯)))) = (π₯ / (absβπ₯))) |
90 | 86, 89 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ π₯ β (β β {0})) β
(expβ(i Β· (β‘πΉβ(π₯ / (absβπ₯))))) = (π₯ / (absβπ₯))) |
91 | 77, 90 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ π₯ β (β β {0})) β
((expβ(β‘(exp βΎ
β)β(absβπ₯))) Β· (expβ(i Β· (β‘πΉβ(π₯ / (absβπ₯)))))) = ((absβπ₯) Β· (π₯ / (absβπ₯)))) |
92 | 21, 45, 46 | divcan2d 11938 |
. . . . . 6
β’ ((π β§ π₯ β (β β {0})) β
((absβπ₯) Β·
(π₯ / (absβπ₯))) = π₯) |
93 | 73, 91, 92 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ π₯ β (β β {0})) β π₯ = (expβ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
94 | 93 | adantrl 715 |
. . . 4
β’ ((π β§ (π¦ β π β§ π₯ β (β β {0}))) β π₯ = (expβ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
95 | | fveq2 6843 |
. . . . 5
β’ (π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β (expβπ¦) = (expβ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
96 | 95 | eqeq2d 2744 |
. . . 4
β’ (π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β (π₯ = (expβπ¦) β π₯ = (expβ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯)))))))) |
97 | 94, 96 | syl5ibrcom 247 |
. . 3
β’ ((π β§ (π¦ β π β§ π₯ β (β β {0}))) β (π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β π₯ = (expβπ¦))) |
98 | 14 | adantl 483 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β β) |
99 | 98 | replimd 15088 |
. . . . . 6
β’ ((π β§ π¦ β π) β π¦ = ((ββπ¦) + (i Β· (ββπ¦)))) |
100 | | absef 16084 |
. . . . . . . . . . 11
β’ (π¦ β β β
(absβ(expβπ¦)) =
(expβ(ββπ¦))) |
101 | 98, 100 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β (absβ(expβπ¦)) =
(expβ(ββπ¦))) |
102 | 98 | recld 15085 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (ββπ¦) β β) |
103 | 102 | fvresd 6863 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β ((exp βΎ
β)β(ββπ¦)) = (expβ(ββπ¦))) |
104 | 101, 103 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (absβ(expβπ¦)) = ((exp βΎ
β)β(ββπ¦))) |
105 | 104 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (β‘(exp βΎ
β)β(absβ(expβπ¦))) = (β‘(exp βΎ β)β((exp βΎ
β)β(ββπ¦)))) |
106 | | f1ocnvfv1 7223 |
. . . . . . . . 9
β’ (((exp
βΎ β):ββ1-1-ontoββ+ β§
(ββπ¦) β
β) β (β‘(exp βΎ
β)β((exp βΎ β)β(ββπ¦))) = (ββπ¦)) |
107 | 24, 102, 106 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (β‘(exp βΎ β)β((exp βΎ
β)β(ββπ¦))) = (ββπ¦)) |
108 | 105, 107 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (β‘(exp βΎ
β)β(absβ(expβπ¦))) = (ββπ¦)) |
109 | 98 | imcld 15086 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β π) β (ββπ¦) β β) |
110 | 109 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π) β (ββπ¦) β β) |
111 | | mulcl 11140 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ (ββπ¦) β β) β (i Β·
(ββπ¦)) β
β) |
112 | 31, 110, 111 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π) β (i Β· (ββπ¦)) β
β) |
113 | | efcl 15970 |
. . . . . . . . . . . . 13
β’ ((i
Β· (ββπ¦))
β β β (expβ(i Β· (ββπ¦))) β β) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (expβ(i Β·
(ββπ¦))) β
β) |
115 | 102 | recnd 11188 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π) β (ββπ¦) β β) |
116 | | efcl 15970 |
. . . . . . . . . . . . 13
β’
((ββπ¦)
β β β (expβ(ββπ¦)) β β) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (expβ(ββπ¦)) β
β) |
118 | | efne0 15984 |
. . . . . . . . . . . . 13
β’
((ββπ¦)
β β β (expβ(ββπ¦)) β 0) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (expβ(ββπ¦)) β 0) |
120 | 114, 117,
119 | divcan3d 11941 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (((expβ(ββπ¦)) Β· (expβ(i
Β· (ββπ¦)))) / (expβ(ββπ¦))) = (expβ(i Β·
(ββπ¦)))) |
121 | 99 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π) β (expβπ¦) = (expβ((ββπ¦) + (i Β·
(ββπ¦))))) |
122 | | efadd 15981 |
. . . . . . . . . . . . . 14
β’
(((ββπ¦)
β β β§ (i Β· (ββπ¦)) β β) β
(expβ((ββπ¦) + (i Β· (ββπ¦)))) =
((expβ(ββπ¦)) Β· (expβ(i Β·
(ββπ¦))))) |
123 | 115, 112,
122 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π) β (expβ((ββπ¦) + (i Β·
(ββπ¦)))) =
((expβ(ββπ¦)) Β· (expβ(i Β·
(ββπ¦))))) |
124 | 121, 123 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (expβπ¦) = ((expβ(ββπ¦)) Β· (expβ(i
Β· (ββπ¦))))) |
125 | 124, 101 | oveq12d 7376 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β ((expβπ¦) / (absβ(expβπ¦))) = (((expβ(ββπ¦)) Β· (expβ(i
Β· (ββπ¦)))) / (expβ(ββπ¦)))) |
126 | | elpreima 7009 |
. . . . . . . . . . . . . . . 16
β’ (β
Fn β β (π¦ β
(β‘β β π·) β (π¦ β β β§ (ββπ¦) β π·))) |
127 | 3, 67, 126 | mp2b 10 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (β‘β β π·) β (π¦ β β β§ (ββπ¦) β π·)) |
128 | 127 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π¦ β (β‘β β π·) β (ββπ¦) β π·) |
129 | 128, 2 | eleq2s 2852 |
. . . . . . . . . . . . 13
β’ (π¦ β π β (ββπ¦) β π·) |
130 | 129 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (ββπ¦) β π·) |
131 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π€ = (ββπ¦) β (i Β· π€) = (i Β·
(ββπ¦))) |
132 | 131 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π€ = (ββπ¦) β (expβ(i Β·
π€)) = (expβ(i
Β· (ββπ¦)))) |
133 | | fvex 6856 |
. . . . . . . . . . . . 13
β’
(expβ(i Β· (ββπ¦))) β V |
134 | 132, 34, 133 | fvmpt 6949 |
. . . . . . . . . . . 12
β’
((ββπ¦)
β π· β (πΉβ(ββπ¦)) = (expβ(i Β·
(ββπ¦)))) |
135 | 130, 134 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (πΉβ(ββπ¦)) = (expβ(i Β·
(ββπ¦)))) |
136 | 120, 125,
135 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β ((expβπ¦) / (absβ(expβπ¦))) = (πΉβ(ββπ¦))) |
137 | 136 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (β‘πΉβ((expβπ¦) / (absβ(expβπ¦)))) = (β‘πΉβ(πΉβ(ββπ¦)))) |
138 | | f1ocnvfv1 7223 |
. . . . . . . . . 10
β’ ((πΉ:π·β1-1-ontoβ(β‘abs
β {1}) β§ (ββπ¦) β π·) β (β‘πΉβ(πΉβ(ββπ¦))) = (ββπ¦)) |
139 | 39, 129, 138 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (β‘πΉβ(πΉβ(ββπ¦))) = (ββπ¦)) |
140 | 137, 139 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (β‘πΉβ((expβπ¦) / (absβ(expβπ¦)))) = (ββπ¦)) |
141 | 140 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦))))) = (i Β· (ββπ¦))) |
142 | 108, 141 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ π¦ β π) β ((β‘(exp βΎ
β)β(absβ(expβπ¦))) + (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦)))))) = ((ββπ¦) + (i Β· (ββπ¦)))) |
143 | 99, 142 | eqtr4d 2776 |
. . . . 5
β’ ((π β§ π¦ β π) β π¦ = ((β‘(exp βΎ
β)β(absβ(expβπ¦))) + (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦))))))) |
144 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = (expβπ¦) β (absβπ₯) = (absβ(expβπ¦))) |
145 | 144 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = (expβπ¦) β (β‘(exp βΎ β)β(absβπ₯)) = (β‘(exp βΎ
β)β(absβ(expβπ¦)))) |
146 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = (expβπ¦) β π₯ = (expβπ¦)) |
147 | 146, 144 | oveq12d 7376 |
. . . . . . . . 9
β’ (π₯ = (expβπ¦) β (π₯ / (absβπ₯)) = ((expβπ¦) / (absβ(expβπ¦)))) |
148 | 147 | fveq2d 6847 |
. . . . . . . 8
β’ (π₯ = (expβπ¦) β (β‘πΉβ(π₯ / (absβπ₯))) = (β‘πΉβ((expβπ¦) / (absβ(expβπ¦))))) |
149 | 148 | oveq2d 7374 |
. . . . . . 7
β’ (π₯ = (expβπ¦) β (i Β· (β‘πΉβ(π₯ / (absβπ₯)))) = (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦)))))) |
150 | 145, 149 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = (expβπ¦) β ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) = ((β‘(exp βΎ
β)β(absβ(expβπ¦))) + (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦))))))) |
151 | 150 | eqeq2d 2744 |
. . . . 5
β’ (π₯ = (expβπ¦) β (π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β π¦ = ((β‘(exp βΎ
β)β(absβ(expβπ¦))) + (i Β· (β‘πΉβ((expβπ¦) / (absβ(expβπ¦)))))))) |
152 | 143, 151 | syl5ibrcom 247 |
. . . 4
β’ ((π β§ π¦ β π) β (π₯ = (expβπ¦) β π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
153 | 152 | adantrr 716 |
. . 3
β’ ((π β§ (π¦ β π β§ π₯ β (β β {0}))) β (π₯ = (expβπ¦) β π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))))) |
154 | 97, 153 | impbid 211 |
. 2
β’ ((π β§ (π¦ β π β§ π₯ β (β β {0}))) β (π¦ = ((β‘(exp βΎ β)β(absβπ₯)) + (i Β· (β‘πΉβ(π₯ / (absβπ₯))))) β π₯ = (expβπ¦))) |
155 | 13, 17, 71, 154 | f1o2d 7608 |
1
β’ (π β (exp βΎ π):πβ1-1-ontoβ(β β {0})) |