Metamath Proof Explorer

Theorem climexp

Description: The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climexp.1 
|- F/ k ph
climexp.2 
|- F/_ k F
climexp.3 
|- F/_ k H
climexp.4 
|- Z = ( ZZ>= ` M )
climexp.5 
|- ( ph -> M e. ZZ )
climexp.6 
|- ( ph -> F : Z --> CC )
climexp.7 
|- ( ph -> F ~~> A )
climexp.8 
|- ( ph -> N e. NN0 )
climexp.9 
|- ( ph -> H e. V )
climexp.10 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) ^ N ) )
Assertion climexp 
|- ( ph -> H ~~> ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 climexp.1 
 |-  F/ k ph
2 climexp.2 
 |-  F/_ k F
3 climexp.3 
 |-  F/_ k H
4 climexp.4 
 |-  Z = ( ZZ>= ` M )
5 climexp.5 
 |-  ( ph -> M e. ZZ )
6 climexp.6 
 |-  ( ph -> F : Z --> CC )
7 climexp.7 
 |-  ( ph -> F ~~> A )
8 climexp.8 
 |-  ( ph -> N e. NN0 )
9 climexp.9 
 |-  ( ph -> H e. V )
10 climexp.10 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) ^ N ) )
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 11 expcn 
 |-  ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
13 8 12 syl 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
14 11 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
15 13 14 eleqtrrdi 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
16 climcl 
 |-  ( F ~~> A -> A e. CC )
17 7 16 syl 
 |-  ( ph -> A e. CC )
18 4 5 15 6 7 17 climcncf 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) ~~> ( ( x e. CC |-> ( x ^ N ) ) ` A ) )
19 eqidd 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) = ( x e. CC |-> ( x ^ N ) ) )
20 simpr 
 |-  ( ( ph /\ x = A ) -> x = A )
21 20 oveq1d 
 |-  ( ( ph /\ x = A ) -> ( x ^ N ) = ( A ^ N ) )
22 17 8 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
23 19 21 17 22 fvmptd 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) ` A ) = ( A ^ N ) )
24 18 23 breqtrd 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) ~~> ( A ^ N ) )
25 cnex 
 |-  CC e. _V
26 25 mptex 
 |-  ( x e. CC |-> ( x ^ N ) ) e. _V
27 4 fvexi 
 |-  Z e. _V
28 fex 
 |-  ( ( F : Z --> CC /\ Z e. _V ) -> F e. _V )
29 6 27 28 sylancl 
 |-  ( ph -> F e. _V )
30 coexg 
 |-  ( ( ( x e. CC |-> ( x ^ N ) ) e. _V /\ F e. _V ) -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) e. _V )
31 26 29 30 sylancr 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) e. _V )
32 eqidd 
 |-  ( ( ph /\ j e. Z ) -> ( x e. CC |-> ( x ^ N ) ) = ( x e. CC |-> ( x ^ N ) ) )
33 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ x = ( F ` j ) ) -> x = ( F ` j ) )
34 33 oveq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ x = ( F ` j ) ) -> ( x ^ N ) = ( ( F ` j ) ^ N ) )
35 6 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC )
36 8 adantr 
 |-  ( ( ph /\ j e. Z ) -> N e. NN0 )
37 35 36 expcld 
 |-  ( ( ph /\ j e. Z ) -> ( ( F ` j ) ^ N ) e. CC )
38 32 34 35 37 fvmptd 
 |-  ( ( ph /\ j e. Z ) -> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` j ) ) = ( ( F ` j ) ^ N ) )
39 fvco3 
 |-  ( ( F : Z --> CC /\ j e. Z ) -> ( ( ( x e. CC |-> ( x ^ N ) ) o. F ) ` j ) = ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` j ) ) )
40 6 39 sylan 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( x e. CC |-> ( x ^ N ) ) o. F ) ` j ) = ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` j ) ) )
41 nfv 
 |-  F/ k j e. Z
42 1 41 nfan 
 |-  F/ k ( ph /\ j e. Z )
43 nfcv 
 |-  F/_ k j
44 3 43 nffv 
 |-  F/_ k ( H ` j )
45 2 43 nffv 
 |-  F/_ k ( F ` j )
46 nfcv 
 |-  F/_ k ^
47 nfcv 
 |-  F/_ k N
48 45 46 47 nfov 
 |-  F/_ k ( ( F ` j ) ^ N )
49 44 48 nfeq 
 |-  F/ k ( H ` j ) = ( ( F ` j ) ^ N )
50 42 49 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) ^ N ) )
51 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
52 51 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
53 fveq2 
 |-  ( k = j -> ( H ` k ) = ( H ` j ) )
54 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
55 54 oveq1d 
 |-  ( k = j -> ( ( F ` k ) ^ N ) = ( ( F ` j ) ^ N ) )
56 53 55 eqeq12d 
 |-  ( k = j -> ( ( H ` k ) = ( ( F ` k ) ^ N ) <-> ( H ` j ) = ( ( F ` j ) ^ N ) ) )
57 52 56 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) ^ N ) ) <-> ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) ^ N ) ) ) )
58 50 57 10 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) ^ N ) )
59 38 40 58 3eqtr4rd 
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( ( x e. CC |-> ( x ^ N ) ) o. F ) ` j ) )
60 4 9 31 5 59 climeq 
 |-  ( ph -> ( H ~~> ( A ^ N ) <-> ( ( x e. CC |-> ( x ^ N ) ) o. F ) ~~> ( A ^ N ) ) )
61 24 60 mpbird 
 |-  ( ph -> H ~~> ( A ^ N ) )