Metamath Proof Explorer

Theorem explecnv

Description: A sequence of terms converges to zero when it is less than powers of a number A whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses explecnv.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
explecnv.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
explecnv.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
explecnv.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
explecnv.4 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
explecnv.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
explecnv.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
Assertion explecnv ( 𝜑 → 𝐹 ⇝ 0 )

Proof

Step Hyp Ref Expression
1 explecnv.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 explecnv.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3 explecnv.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 explecnv.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 explecnv.4 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
6 explecnv.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7 explecnv.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
8 eqid ⊢ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) )
9 0z ⊢ 0 ∈ ℤ
10 ifcl ⊢ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ∈ ℤ )
11 9 3 10 sylancr ⊢ ( 𝜑 → if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ∈ ℤ )
12 4 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13 12 5 expcnv ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
14 1 fvexi ⊢ 𝑍 ∈ V
15 14 mptex ⊢ ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ V
16 15 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ V )
17 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18 1 17 ineq12i ⊢ ( 𝑍 ∩ ℕ0 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 0 ) )
19 uzin ⊢ ( ( 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 0 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) )
20 3 9 19 sylancl ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 0 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) )
21 18 20 syl5req ⊢ ( 𝜑 → ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) = ( 𝑍 ∩ ℕ0 ) )
22 21 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ↔ 𝑘 ∈ ( 𝑍 ∩ ℕ0 ) ) )
23 22 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 𝑘 ∈ ( 𝑍 ∩ ℕ0 ) )
24 23 elin2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
25 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
26 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
27 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
28 25 26 27 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
29 24 28 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
30 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 𝐴 ∈ ℝ )
31 30 24 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
32 29 31 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
33 23 elin1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 )
34 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
35 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) )
36 fvex ⊢ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
37 34 35 36 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
38 33 37 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
39 33 6 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
40 39 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
41 38 40 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℝ )
42 33 7 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
43 42 38 29 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) )
44 39 absge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
45 44 38 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ 0 , 0 , 𝑀 ) ) ) → 0 ≤ ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
46 8 11 13 16 32 41 43 45 climsqz2 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ 0 )
47 37 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
48 1 3 2 16 6 47 climabs0 ⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ 0 ) )
49 46 48 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 0 )