Step |
Hyp |
Ref |
Expression |
1 |
|
mbflim.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
mbflim.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
mbflim.4 |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> C ) |
4 |
|
mbflim.5 |
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn ) |
5 |
|
mbflim.6 |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. V ) |
6 |
1
|
fvexi |
|- Z e. _V |
7 |
6
|
mptex |
|- ( n e. Z |-> ( Re ` B ) ) e. _V |
8 |
7
|
a1i |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Re ` B ) ) e. _V ) |
9 |
2
|
adantr |
|- ( ( ph /\ x e. A ) -> M e. ZZ ) |
10 |
5
|
anassrs |
|- ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V ) |
11 |
4 10
|
mbfmptcl |
|- ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. CC ) |
12 |
11
|
an32s |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. CC ) |
13 |
12
|
fmpttd |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> CC ) |
14 |
13
|
ffvelrnda |
|- ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> B ) ` k ) e. CC ) |
15 |
|
simpr |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> n e. Z ) |
16 |
12
|
recld |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Re ` B ) e. RR ) |
17 |
|
eqid |
|- ( n e. Z |-> ( Re ` B ) ) = ( n e. Z |-> ( Re ` B ) ) |
18 |
17
|
fvmpt2 |
|- ( ( n e. Z /\ ( Re ` B ) e. RR ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` B ) ) |
19 |
15 16 18
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` B ) ) |
20 |
|
eqid |
|- ( n e. Z |-> B ) = ( n e. Z |-> B ) |
21 |
20
|
fvmpt2 |
|- ( ( n e. Z /\ B e. CC ) -> ( ( n e. Z |-> B ) ` n ) = B ) |
22 |
15 12 21
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B ) |
23 |
22
|
fveq2d |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Re ` ( ( n e. Z |-> B ) ` n ) ) = ( Re ` B ) ) |
24 |
19 23
|
eqtr4d |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) |
25 |
24
|
ralrimiva |
|- ( ( ph /\ x e. A ) -> A. n e. Z ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) |
26 |
|
nffvmpt1 |
|- F/_ n ( ( n e. Z |-> ( Re ` B ) ) ` k ) |
27 |
|
nfcv |
|- F/_ n Re |
28 |
|
nffvmpt1 |
|- F/_ n ( ( n e. Z |-> B ) ` k ) |
29 |
27 28
|
nffv |
|- F/_ n ( Re ` ( ( n e. Z |-> B ) ` k ) ) |
30 |
26 29
|
nfeq |
|- F/ n ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) |
31 |
|
nfv |
|- F/ k ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) |
32 |
|
fveq2 |
|- ( k = n -> ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( ( n e. Z |-> ( Re ` B ) ) ` n ) ) |
33 |
|
2fveq3 |
|- ( k = n -> ( Re ` ( ( n e. Z |-> B ) ` k ) ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) |
34 |
32 33
|
eqeq12d |
|- ( k = n -> ( ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) <-> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) ) |
35 |
30 31 34
|
cbvralw |
|- ( A. k e. Z ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) <-> A. n e. Z ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) |
36 |
25 35
|
sylibr |
|- ( ( ph /\ x e. A ) -> A. k e. Z ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) ) |
37 |
36
|
r19.21bi |
|- ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) ) |
38 |
1 3 8 9 14 37
|
climre |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Re ` B ) ) ~~> ( Re ` C ) ) |
39 |
11
|
ismbfcn2 |
|- ( ( ph /\ n e. Z ) -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) ) |
40 |
4 39
|
mpbid |
|- ( ( ph /\ n e. Z ) -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) |
41 |
40
|
simpld |
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> ( Re ` B ) ) e. MblFn ) |
42 |
11
|
anasss |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. CC ) |
43 |
42
|
recld |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> ( Re ` B ) e. RR ) |
44 |
1 2 38 41 43
|
mbflimlem |
|- ( ph -> ( x e. A |-> ( Re ` C ) ) e. MblFn ) |
45 |
6
|
mptex |
|- ( n e. Z |-> ( Im ` B ) ) e. _V |
46 |
45
|
a1i |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Im ` B ) ) e. _V ) |
47 |
12
|
imcld |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Im ` B ) e. RR ) |
48 |
|
eqid |
|- ( n e. Z |-> ( Im ` B ) ) = ( n e. Z |-> ( Im ` B ) ) |
49 |
48
|
fvmpt2 |
|- ( ( n e. Z /\ ( Im ` B ) e. RR ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` B ) ) |
50 |
15 47 49
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` B ) ) |
51 |
22
|
fveq2d |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Im ` ( ( n e. Z |-> B ) ` n ) ) = ( Im ` B ) ) |
52 |
50 51
|
eqtr4d |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) |
53 |
52
|
ralrimiva |
|- ( ( ph /\ x e. A ) -> A. n e. Z ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) |
54 |
|
nffvmpt1 |
|- F/_ n ( ( n e. Z |-> ( Im ` B ) ) ` k ) |
55 |
|
nfcv |
|- F/_ n Im |
56 |
55 28
|
nffv |
|- F/_ n ( Im ` ( ( n e. Z |-> B ) ` k ) ) |
57 |
54 56
|
nfeq |
|- F/ n ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) |
58 |
|
nfv |
|- F/ k ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) |
59 |
|
fveq2 |
|- ( k = n -> ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( ( n e. Z |-> ( Im ` B ) ) ` n ) ) |
60 |
|
2fveq3 |
|- ( k = n -> ( Im ` ( ( n e. Z |-> B ) ` k ) ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) |
61 |
59 60
|
eqeq12d |
|- ( k = n -> ( ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) <-> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) ) |
62 |
57 58 61
|
cbvralw |
|- ( A. k e. Z ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) <-> A. n e. Z ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) |
63 |
53 62
|
sylibr |
|- ( ( ph /\ x e. A ) -> A. k e. Z ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) ) |
64 |
63
|
r19.21bi |
|- ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) ) |
65 |
1 3 46 9 14 64
|
climim |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Im ` B ) ) ~~> ( Im ` C ) ) |
66 |
40
|
simprd |
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> ( Im ` B ) ) e. MblFn ) |
67 |
42
|
imcld |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> ( Im ` B ) e. RR ) |
68 |
1 2 65 66 67
|
mbflimlem |
|- ( ph -> ( x e. A |-> ( Im ` C ) ) e. MblFn ) |
69 |
|
climcl |
|- ( ( n e. Z |-> B ) ~~> C -> C e. CC ) |
70 |
3 69
|
syl |
|- ( ( ph /\ x e. A ) -> C e. CC ) |
71 |
70
|
ismbfcn2 |
|- ( ph -> ( ( x e. A |-> C ) e. MblFn <-> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) ) ) |
72 |
44 68 71
|
mpbir2and |
|- ( ph -> ( x e. A |-> C ) e. MblFn ) |