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 ⊢ Ⅎ 𝑘 𝜑
climexp.2 ⊢ Ⅎ 𝑘 𝐹
climexp.3 ⊢ Ⅎ 𝑘 𝐻
climexp.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climexp.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climexp.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
climexp.7 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climexp.8 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
climexp.9 ⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
climexp.10 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 𝑁 ) )
Assertion climexp ( 𝜑 → 𝐻 ⇝ ( 𝐴 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 climexp.1 ⊢ Ⅎ 𝑘 𝜑
2 climexp.2 ⊢ Ⅎ 𝑘 𝐹
3 climexp.3 ⊢ Ⅎ 𝑘 𝐻
4 climexp.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 climexp.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 climexp.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
7 climexp.7 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
8 climexp.8 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 climexp.9 ⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
10 climexp.10 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 𝑁 ) )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 11 expcn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
13 8 12 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
14 11 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
15 13 14 eleqtrrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
16 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
17 7 16 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
18 4 5 15 6 7 17 climcncf ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ⇝ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ 𝐴 ) )
19 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
21 20 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑥 ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
22 17 8 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
23 19 21 17 22 fvmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ 𝐴 ) = ( 𝐴 ↑ 𝑁 ) )
24 18 23 breqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ⇝ ( 𝐴 ↑ 𝑁 ) )
25 cnex ⊢ ℂ ∈ V
26 25 mptex ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ V
27 4 fvexi ⊢ 𝑍 ∈ V
28 fex ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑍 ∈ V ) → 𝐹 ∈ V )
29 6 27 28 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
30 coexg ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ V ∧ 𝐹 ∈ V ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ∈ V )
31 26 29 30 sylancr ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ∈ V )
32 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑗 ) ) → 𝑥 = ( 𝐹 ‘ 𝑗 ) )
34 33 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑥 ↑ 𝑁 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) )
35 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
36 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑁 ∈ ℕ0 )
37 35 36 expcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) ∈ ℂ )
38 32 34 35 37 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) )
39 fvco3 ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑗 ) ) )
40 6 39 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑗 ) ) )
41 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
42 1 41 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
43 nfcv ⊢ Ⅎ 𝑘 𝑗
44 3 43 nffv ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 )
45 2 43 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
46 nfcv ⊢ Ⅎ 𝑘 ↑
47 nfcv ⊢ Ⅎ 𝑘 𝑁
48 45 46 47 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 )
49 44 48 nfeq ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 )
50 42 49 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) )
51 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
52 51 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
53 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑗 ) )
54 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
55 54 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ↑ 𝑁 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) )
56 53 55 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 𝑁 ) ↔ ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) ) )
57 52 56 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) ) ) )
58 50 57 10 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ↑ 𝑁 ) )
59 38 40 58 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ‘ 𝑗 ) )
60 4 9 31 5 59 climeq ⊢ ( 𝜑 → ( 𝐻 ⇝ ( 𝐴 ↑ 𝑁 ) ↔ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ⇝ ( 𝐴 ↑ 𝑁 ) ) )
61 24 60 mpbird ⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 ↑ 𝑁 ) )