This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abelthlem5

Description: Lemma for abelth . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
Assertion abelthlem5 ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
7 abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
10 1rp ⊢ 1 ∈ ℝ+
11 10 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
12 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) )
13 8 9 11 12 7 climi0 ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 )
15 simprl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → 𝑗 ∈ ℕ0 )
16 oveq2 ⊢ ( 𝑛 = 𝑖 → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
17 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
18 ovex ⊢ ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ∈ V
19 16 17 18 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
20 19 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
21 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
22 0cn ⊢ 0 ∈ ℂ
23 1xr ⊢ 1 ∈ ℝ*
24 blssm ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ )
25 21 22 23 24 mp3an ⊢ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ
26 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
27 25 26 sselid ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → 𝑋 ∈ ℂ )
28 27 abscld ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
29 reexpcl ⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 𝑖 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ∈ ℝ )
30 28 29 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ∈ ℝ )
31 20 30 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) ∈ ℝ )
32 fveq2 ⊢ ( 𝑘 = 𝑖 → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) )
33 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑖 ) )
34 32 33 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
35 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
36 ovex ⊢ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ V
37 34 35 36 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
38 37 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
39 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑥 ) ∈ ℂ )
40 8 9 39 serf ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
42 41 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
43 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑖 ) ∈ ℂ )
44 27 43 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑖 ) ∈ ℂ )
45 42 44 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ ℂ )
46 38 45 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
47 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ 𝑋 ) ∈ ℂ )
48 absidm ⊢ ( 𝑋 ∈ ℂ → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
49 27 48 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
50 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
51 50 cnmetdval ⊢ ( ( 𝑋 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) )
52 27 22 51 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) )
53 27 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( 𝑋 − 0 ) = 𝑋 )
54 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) )
55 52 54 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑋 ) )
56 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
57 21 23 56 mpanl12 ⊢ ( ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
58 22 27 57 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
59 26 58 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( 𝑋 ( abs ∘ − ) 0 ) < 1 )
60 55 59 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ 𝑋 ) < 1 )
61 49 60 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ( abs ‘ ( abs ‘ 𝑋 ) ) < 1 )
62 47 61 20 geolim ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝑋 ) ) ) )
63 climrel ⊢ Rel ⇝
64 63 releldmi ⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝑋 ) ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) ∈ dom ⇝ )
65 62 64 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) ∈ dom ⇝ )
66 1red ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → 1 ∈ ℝ )
67 41 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
68 eluznn0 ⊢ ( ( 𝑗 ∈ ℕ0 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑖 ∈ ℕ0 )
69 15 68 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑖 ∈ ℕ0 )
70 67 69 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
71 69 44 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑋 ↑ 𝑖 ) ∈ ℂ )
72 70 71 absmuld ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) · ( abs ‘ ( 𝑋 ↑ 𝑖 ) ) ) )
73 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑋 ∈ ℂ )
74 73 69 absexpd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝑋 ↑ 𝑖 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
75 74 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) · ( abs ‘ ( 𝑋 ↑ 𝑖 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) )
76 72 75 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) )
77 70 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ )
78 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 1 ∈ ℝ )
79 69 30 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ∈ ℝ )
80 71 absge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( abs ‘ ( 𝑋 ↑ 𝑖 ) ) )
81 80 74 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
82 simprr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 )
83 2fveq3 ⊢ ( 𝑚 = 𝑖 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) )
84 83 breq1d ⊢ ( 𝑚 = 𝑖 → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ↔ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) < 1 ) )
85 84 rspccva ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) < 1 )
86 82 85 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) < 1 )
87 1re ⊢ 1 ∈ ℝ
88 ltle ⊢ ( ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) < 1 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ≤ 1 ) )
89 77 87 88 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) < 1 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ≤ 1 ) )
90 86 89 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ≤ 1 )
91 77 78 79 81 90 lemul1ad ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) ≤ ( 1 · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) )
92 76 91 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) ≤ ( 1 · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) )
93 69 37 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
94 93 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) )
95 69 19 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) )
96 95 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 · ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) ) = ( 1 · ( ( abs ‘ 𝑋 ) ↑ 𝑖 ) ) )
97 92 94 96 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ) ≤ ( 1 · ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ‘ 𝑖 ) ) )
98 8 15 31 46 65 66 97 cvgcmpce ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
99 14 98 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )