Metamath Proof Explorer

Theorem radcnvlem1

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges absolutely at X , even if the terms in the sequence are multiplied by n . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
psergf.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
radcnvlem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
radcnvlem2.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) )
radcnvlem2.c ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑌 ) ) ∈ dom ⇝ )
radcnvlem1.h ⊢ 𝐻 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
Assertion radcnvlem1 ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3 psergf.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4 radcnvlem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5 radcnvlem2.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) )
6 radcnvlem2.c ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑌 ) ) ∈ dom ⇝ )
7 radcnvlem1.h ⊢ 𝐻 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
10 1rp ⊢ 1 ∈ ℝ+
11 10 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
12 1 pserval2 ⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) )
13 4 12 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) )
14 fvexd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ V )
15 1 2 4 psergf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) : ℕ0 ⟶ ℂ )
16 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑌 ) ‘ 𝑘 ) ∈ ℂ )
17 8 9 14 6 16 serf0 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ⇝ 0 )
18 8 9 11 13 17 climi0 ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 )
19 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → 𝑗 ∈ ℕ0 )
20 nn0re ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℝ )
22 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → 𝑋 ∈ ℂ )
23 22 abscld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
24 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → 𝑌 ∈ ℂ )
25 24 abscld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( abs ‘ 𝑌 ) ∈ ℝ )
26 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
27 3 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
28 4 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ∈ ℝ )
29 3 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑋 ) )
30 26 27 28 29 5 lelttrd ⊢ ( 𝜑 → 0 < ( abs ‘ 𝑌 ) )
31 30 gt0ne0d ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ≠ 0 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( abs ‘ 𝑌 ) ≠ 0 )
33 23 25 32 redivcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℝ )
34 reexpcl ⊢ ( ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℝ ∧ 𝑖 ∈ ℕ0 ) → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ∈ ℝ )
35 33 34 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ∈ ℝ )
36 21 35 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ∈ ℝ )
37 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) )
38 36 37 fmptd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) : ℕ0 ⟶ ℝ )
39 38 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ‘ 𝑚 ) ∈ ℝ )
40 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℝ )
42 1 2 3 psergf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )
43 42 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ∈ ℂ )
44 43 abscld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ∈ ℝ )
45 41 44 remulcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ∈ ℝ )
46 45 7 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ0 ⟶ ℝ )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → 𝐻 : ℕ0 ⟶ ℝ )
48 47 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑚 ) ∈ ℝ )
49 48 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑚 ) ∈ ℂ )
50 27 28 31 redivcld ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℝ )
51 50 recnd ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℂ )
52 divge0 ⊢ ( ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑋 ) ) ∧ ( ( abs ‘ 𝑌 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝑌 ) ) ) → 0 ≤ ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) )
53 27 29 28 30 52 syl22anc ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) )
54 50 53 absidd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ) = ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) )
55 28 recnd ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ∈ ℂ )
56 55 mulridd ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) · 1 ) = ( abs ‘ 𝑌 ) )
57 5 56 breqtrrd ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( ( abs ‘ 𝑌 ) · 1 ) )
58 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
59 ltdivmul ⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( abs ‘ 𝑌 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝑌 ) ) ) → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) < 1 ↔ ( abs ‘ 𝑋 ) < ( ( abs ‘ 𝑌 ) · 1 ) ) )
60 27 58 28 30 59 syl112anc ⊢ ( 𝜑 → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) < 1 ↔ ( abs ‘ 𝑋 ) < ( ( abs ‘ 𝑌 ) · 1 ) ) )
61 57 60 mpbird ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) < 1 )
62 54 61 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ) < 1 )
63 37 geomulcvg ⊢ ( ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℂ ∧ ( abs ‘ ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ) < 1 ) → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ) ∈ dom ⇝ )
64 51 62 63 syl2anc ⊢ ( 𝜑 → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ) ∈ dom ⇝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ) ∈ dom ⇝ )
66 1red ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → 1 ∈ ℝ )
67 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )
68 eluznn0 ⊢ ( ( 𝑗 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ0 )
69 19 68 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ0 )
70 67 69 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ∈ ℂ )
71 70 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ∈ ℝ )
72 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ∈ ℝ )
73 72 69 reexpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ∈ ℝ )
74 69 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℝ )
75 69 nn0ge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ 𝑚 )
76 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
77 76 69 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
78 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑌 ∈ ℂ )
79 78 69 expcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑌 ↑ 𝑚 ) ∈ ℂ )
80 77 79 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ∈ ℂ )
81 80 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) ∈ ℝ )
82 1red ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 1 ∈ ℝ )
83 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑋 ∈ ℂ )
84 83 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
85 84 69 reexpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ∈ ℝ )
86 83 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( abs ‘ 𝑋 ) )
87 84 69 86 expge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) )
88 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 )
89 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑚 ) )
90 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑌 ↑ 𝑘 ) = ( 𝑌 ↑ 𝑚 ) )
91 89 90 oveq12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) )
92 91 fveq2d ⊢ ( 𝑘 = 𝑚 → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) )
93 92 breq1d ⊢ ( 𝑘 = 𝑚 → ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ↔ ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) < 1 ) )
94 93 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) < 1 )
95 88 94 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) < 1 )
96 1re ⊢ 1 ∈ ℝ
97 ltle ⊢ ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) < 1 → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) ≤ 1 ) )
98 81 96 97 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) < 1 → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) ≤ 1 ) )
99 95 98 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) ≤ 1 )
100 81 82 85 87 99 lemul1ad ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) ≤ ( 1 · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) )
101 83 69 expcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑋 ↑ 𝑚 ) ∈ ℂ )
102 77 101 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ )
103 102 79 absmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) · ( 𝑌 ↑ 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( abs ‘ ( 𝑌 ↑ 𝑚 ) ) ) )
104 80 101 absmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) · ( 𝑋 ↑ 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( abs ‘ ( 𝑋 ↑ 𝑚 ) ) ) )
105 77 79 101 mul32d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) · ( 𝑋 ↑ 𝑚 ) ) = ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) · ( 𝑌 ↑ 𝑚 ) ) )
106 105 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) · ( 𝑋 ↑ 𝑚 ) ) ) = ( abs ‘ ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) · ( 𝑌 ↑ 𝑚 ) ) ) )
107 83 69 absexpd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝑋 ↑ 𝑚 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) )
108 107 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( abs ‘ ( 𝑋 ↑ 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) )
109 104 106 108 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) · ( 𝑌 ↑ 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) )
110 78 69 absexpd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝑌 ↑ 𝑚 ) ) = ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) )
111 110 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( abs ‘ ( 𝑌 ↑ 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) )
112 103 109 111 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑌 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) )
113 85 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ∈ ℂ )
114 113 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 · ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) )
115 100 112 114 3brtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) )
116 102 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ∈ ℝ )
117 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ 𝑌 ) ∈ ℝ )
118 117 69 reexpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ∈ ℝ )
119 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑚 ∈ ℤ )
120 119 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℤ )
121 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 < ( abs ‘ 𝑌 ) )
122 expgt0 ⊢ ( ( ( abs ‘ 𝑌 ) ∈ ℝ ∧ 𝑚 ∈ ℤ ∧ 0 < ( abs ‘ 𝑌 ) ) → 0 < ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) )
123 117 120 121 122 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 < ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) )
124 lemuldiv ⊢ ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ∈ ℝ ∧ ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ∈ ℝ ∧ ( ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ∈ ℝ ∧ 0 < ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ) → ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ↔ ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ≤ ( ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) / ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ) )
125 116 85 118 123 124 syl112anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) · ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) ↔ ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ≤ ( ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) / ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) ) )
126 115 125 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ≤ ( ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) / ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) )
127 1 pserval2 ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) )
128 83 69 127 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) )
129 128 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )
130 23 recnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( abs ‘ 𝑋 ) ∈ ℂ )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ 𝑋 ) ∈ ℂ )
132 25 recnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → ( abs ‘ 𝑌 ) ∈ ℂ )
133 132 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ 𝑌 ) ∈ ℂ )
134 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ 𝑌 ) ≠ 0 )
135 131 133 134 69 expdivd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) = ( ( ( abs ‘ 𝑋 ) ↑ 𝑚 ) / ( ( abs ‘ 𝑌 ) ↑ 𝑚 ) ) )
136 126 129 135 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ≤ ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) )
137 71 73 74 75 136 lemul2ad ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ≤ ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) )
138 74 71 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ∈ ℝ )
139 70 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) )
140 74 71 75 139 mulge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 0 ≤ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
141 138 140 absidd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) = ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
142 74 73 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ∈ ℝ )
143 142 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ∈ ℂ )
144 143 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 · ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ) = ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) )
145 137 141 144 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ≤ ( 1 · ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ) )
146 ovex ⊢ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ∈ V
147 7 fvmpt2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ∈ V ) → ( 𝐻 ‘ 𝑚 ) = ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
148 69 146 147 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐻 ‘ 𝑚 ) = ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
149 148 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝐻 ‘ 𝑚 ) ) = ( abs ‘ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) )
150 id ⊢ ( 𝑖 = 𝑚 → 𝑖 = 𝑚 )
151 oveq2 ⊢ ( 𝑖 = 𝑚 → ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) = ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) )
152 150 151 oveq12d ⊢ ( 𝑖 = 𝑚 → ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) = ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) )
153 ovex ⊢ ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ∈ V
154 152 37 153 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ‘ 𝑚 ) = ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) )
155 69 154 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ‘ 𝑚 ) = ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) )
156 155 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 · ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ‘ 𝑚 ) ) = ( 1 · ( 𝑚 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑚 ) ) ) )
157 145 149 156 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝐻 ‘ 𝑚 ) ) ≤ ( 1 · ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑌 ) ) ↑ 𝑖 ) ) ) ‘ 𝑚 ) ) )
158 8 19 39 49 65 66 157 cvgcmpce ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑌 ↑ 𝑘 ) ) ) < 1 ) ) → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )
159 18 158 rexlimddv ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )