# Metamath Proof Explorer

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 ${⊢}{G}=\left({x}\in ℂ⟼\left({n}\in {ℕ}_{0}⟼{A}\left({n}\right){{x}}^{{n}}\right)\right)$
radcnv.a ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶ℂ$
psergf.x ${⊢}{\phi }\to {X}\in ℂ$
radcnvlem2.y ${⊢}{\phi }\to {Y}\in ℂ$
radcnvlem2.a ${⊢}{\phi }\to \left|{X}\right|<\left|{Y}\right|$
radcnvlem2.c ${⊢}{\phi }\to seq0\left(+,{G}\left({Y}\right)\right)\in \mathrm{dom}⇝$
radcnvlem1.h ${⊢}{H}=\left({m}\in {ℕ}_{0}⟼{m}\left|{G}\left({X}\right)\left({m}\right)\right|\right)$
Assertion radcnvlem1 ${⊢}{\phi }\to seq0\left(+,{H}\right)\in \mathrm{dom}⇝$

### Proof

Step Hyp Ref Expression
1 pser.g ${⊢}{G}=\left({x}\in ℂ⟼\left({n}\in {ℕ}_{0}⟼{A}\left({n}\right){{x}}^{{n}}\right)\right)$
2 radcnv.a ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶ℂ$
3 psergf.x ${⊢}{\phi }\to {X}\in ℂ$
4 radcnvlem2.y ${⊢}{\phi }\to {Y}\in ℂ$
5 radcnvlem2.a ${⊢}{\phi }\to \left|{X}\right|<\left|{Y}\right|$
6 radcnvlem2.c ${⊢}{\phi }\to seq0\left(+,{G}\left({Y}\right)\right)\in \mathrm{dom}⇝$
7 radcnvlem1.h ${⊢}{H}=\left({m}\in {ℕ}_{0}⟼{m}\left|{G}\left({X}\right)\left({m}\right)\right|\right)$
8 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
9 0zd ${⊢}{\phi }\to 0\in ℤ$
10 1rp ${⊢}1\in {ℝ}^{+}$
11 10 a1i ${⊢}{\phi }\to 1\in {ℝ}^{+}$
12 1 pserval2 ${⊢}\left({Y}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({Y}\right)\left({k}\right)={A}\left({k}\right){{Y}}^{{k}}$
13 4 12 sylan ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({Y}\right)\left({k}\right)={A}\left({k}\right){{Y}}^{{k}}$
14 fvexd ${⊢}{\phi }\to {G}\left({Y}\right)\in \mathrm{V}$
15 1 2 4 psergf ${⊢}{\phi }\to {G}\left({Y}\right):{ℕ}_{0}⟶ℂ$
16 15 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({Y}\right)\left({k}\right)\in ℂ$
17 8 9 14 6 16 serf0 ${⊢}{\phi }\to {G}\left({Y}\right)⇝0$
18 8 9 11 13 17 climi0 ${⊢}{\phi }\to \exists {j}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1$
19 simprl ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to {j}\in {ℕ}_{0}$
20 nn0re ${⊢}{i}\in {ℕ}_{0}\to {i}\in ℝ$
21 20 adantl ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {i}\in {ℕ}_{0}\right)\to {i}\in ℝ$
22 3 adantr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to {X}\in ℂ$
23 22 abscld ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left|{X}\right|\in ℝ$
24 4 adantr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to {Y}\in ℂ$
25 24 abscld ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left|{Y}\right|\in ℝ$
26 0red ${⊢}{\phi }\to 0\in ℝ$
27 3 abscld ${⊢}{\phi }\to \left|{X}\right|\in ℝ$
28 4 abscld ${⊢}{\phi }\to \left|{Y}\right|\in ℝ$
29 3 absge0d ${⊢}{\phi }\to 0\le \left|{X}\right|$
30 26 27 28 29 5 lelttrd ${⊢}{\phi }\to 0<\left|{Y}\right|$
31 30 gt0ne0d ${⊢}{\phi }\to \left|{Y}\right|\ne 0$
32 31 adantr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left|{Y}\right|\ne 0$
33 23 25 32 redivcld ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \frac{\left|{X}\right|}{\left|{Y}\right|}\in ℝ$
34 reexpcl ${⊢}\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\in ℝ\wedge {i}\in {ℕ}_{0}\right)\to {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\in ℝ$
35 33 34 sylan ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {i}\in {ℕ}_{0}\right)\to {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\in ℝ$
36 21 35 remulcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {i}\in {ℕ}_{0}\right)\to {i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\in ℝ$
37 eqid ${⊢}\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)=\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)$
38 36 37 fmptd ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right):{ℕ}_{0}⟶ℝ$
39 38 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℕ}_{0}\right)\to \left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\left({m}\right)\in ℝ$
40 nn0re ${⊢}{m}\in {ℕ}_{0}\to {m}\in ℝ$
41 40 adantl ${⊢}\left({\phi }\wedge {m}\in {ℕ}_{0}\right)\to {m}\in ℝ$
42 1 2 3 psergf ${⊢}{\phi }\to {G}\left({X}\right):{ℕ}_{0}⟶ℂ$
43 42 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in {ℕ}_{0}\right)\to {G}\left({X}\right)\left({m}\right)\in ℂ$
44 43 abscld ${⊢}\left({\phi }\wedge {m}\in {ℕ}_{0}\right)\to \left|{G}\left({X}\right)\left({m}\right)\right|\in ℝ$
45 41 44 remulcld ${⊢}\left({\phi }\wedge {m}\in {ℕ}_{0}\right)\to {m}\left|{G}\left({X}\right)\left({m}\right)\right|\in ℝ$
46 45 7 fmptd ${⊢}{\phi }\to {H}:{ℕ}_{0}⟶ℝ$
47 46 adantr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to {H}:{ℕ}_{0}⟶ℝ$
48 47 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℕ}_{0}\right)\to {H}\left({m}\right)\in ℝ$
49 48 recnd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℕ}_{0}\right)\to {H}\left({m}\right)\in ℂ$
50 27 28 31 redivcld ${⊢}{\phi }\to \frac{\left|{X}\right|}{\left|{Y}\right|}\in ℝ$
51 50 recnd ${⊢}{\phi }\to \frac{\left|{X}\right|}{\left|{Y}\right|}\in ℂ$
52 divge0 ${⊢}\left(\left(\left|{X}\right|\in ℝ\wedge 0\le \left|{X}\right|\right)\wedge \left(\left|{Y}\right|\in ℝ\wedge 0<\left|{Y}\right|\right)\right)\to 0\le \frac{\left|{X}\right|}{\left|{Y}\right|}$
53 27 29 28 30 52 syl22anc ${⊢}{\phi }\to 0\le \frac{\left|{X}\right|}{\left|{Y}\right|}$
54 50 53 absidd ${⊢}{\phi }\to \left|\frac{\left|{X}\right|}{\left|{Y}\right|}\right|=\frac{\left|{X}\right|}{\left|{Y}\right|}$
55 28 recnd ${⊢}{\phi }\to \left|{Y}\right|\in ℂ$
56 55 mulid1d ${⊢}{\phi }\to \left|{Y}\right|\cdot 1=\left|{Y}\right|$
57 5 56 breqtrrd ${⊢}{\phi }\to \left|{X}\right|<\left|{Y}\right|\cdot 1$
58 1red ${⊢}{\phi }\to 1\in ℝ$
59 ltdivmul ${⊢}\left(\left|{X}\right|\in ℝ\wedge 1\in ℝ\wedge \left(\left|{Y}\right|\in ℝ\wedge 0<\left|{Y}\right|\right)\right)\to \left(\frac{\left|{X}\right|}{\left|{Y}\right|}<1↔\left|{X}\right|<\left|{Y}\right|\cdot 1\right)$
60 27 58 28 30 59 syl112anc ${⊢}{\phi }\to \left(\frac{\left|{X}\right|}{\left|{Y}\right|}<1↔\left|{X}\right|<\left|{Y}\right|\cdot 1\right)$
61 57 60 mpbird ${⊢}{\phi }\to \frac{\left|{X}\right|}{\left|{Y}\right|}<1$
62 54 61 eqbrtrd ${⊢}{\phi }\to \left|\frac{\left|{X}\right|}{\left|{Y}\right|}\right|<1$
63 37 geomulcvg ${⊢}\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\in ℂ\wedge \left|\frac{\left|{X}\right|}{\left|{Y}\right|}\right|<1\right)\to seq0\left(+,\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\right)\in \mathrm{dom}⇝$
64 51 62 63 syl2anc ${⊢}{\phi }\to seq0\left(+,\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\right)\in \mathrm{dom}⇝$
65 64 adantr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to seq0\left(+,\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\right)\in \mathrm{dom}⇝$
66 1red ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to 1\in ℝ$
67 42 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {G}\left({X}\right):{ℕ}_{0}⟶ℂ$
68 eluznn0 ${⊢}\left({j}\in {ℕ}_{0}\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in {ℕ}_{0}$
69 19 68 sylan ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in {ℕ}_{0}$
70 67 69 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {G}\left({X}\right)\left({m}\right)\in ℂ$
71 70 abscld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{G}\left({X}\right)\left({m}\right)\right|\in ℝ$
72 33 adantr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \frac{\left|{X}\right|}{\left|{Y}\right|}\in ℝ$
73 72 69 reexpcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}\in ℝ$
74 69 nn0red ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in ℝ$
75 69 nn0ge0d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0\le {m}$
76 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {A}:{ℕ}_{0}⟶ℂ$
77 76 69 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {A}\left({m}\right)\in ℂ$
78 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {Y}\in ℂ$
79 78 69 expcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {{Y}}^{{m}}\in ℂ$
80 77 79 mulcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {A}\left({m}\right){{Y}}^{{m}}\in ℂ$
81 80 abscld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|\in ℝ$
82 1red ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 1\in ℝ$
83 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {X}\in ℂ$
84 83 abscld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{X}\right|\in ℝ$
85 84 69 reexpcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {\left|{X}\right|}^{{m}}\in ℝ$
86 83 absge0d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0\le \left|{X}\right|$
87 84 69 86 expge0d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0\le {\left|{X}\right|}^{{m}}$
88 simprr ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1$
89 fveq2 ${⊢}{k}={m}\to {A}\left({k}\right)={A}\left({m}\right)$
90 oveq2 ${⊢}{k}={m}\to {{Y}}^{{k}}={{Y}}^{{m}}$
91 89 90 oveq12d ${⊢}{k}={m}\to {A}\left({k}\right){{Y}}^{{k}}={A}\left({m}\right){{Y}}^{{m}}$
92 91 fveq2d ${⊢}{k}={m}\to \left|{A}\left({k}\right){{Y}}^{{k}}\right|=\left|{A}\left({m}\right){{Y}}^{{m}}\right|$
93 92 breq1d ${⊢}{k}={m}\to \left(\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1↔\left|{A}\left({m}\right){{Y}}^{{m}}\right|<1\right)$
94 93 rspccva ${⊢}\left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|<1$
95 88 94 sylan ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|<1$
96 1re ${⊢}1\in ℝ$
97 ltle ${⊢}\left(\left|{A}\left({m}\right){{Y}}^{{m}}\right|\in ℝ\wedge 1\in ℝ\right)\to \left(\left|{A}\left({m}\right){{Y}}^{{m}}\right|<1\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|\le 1\right)$
98 81 96 97 sylancl ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left(\left|{A}\left({m}\right){{Y}}^{{m}}\right|<1\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|\le 1\right)$
99 95 98 mpd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|\le 1$
100 81 82 85 87 99 lemul1ad ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|{\left|{X}\right|}^{{m}}\le 1{\left|{X}\right|}^{{m}}$
101 83 69 expcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {{X}}^{{m}}\in ℂ$
102 77 101 mulcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {A}\left({m}\right){{X}}^{{m}}\in ℂ$
103 102 79 absmuld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}{{Y}}^{{m}}\right|=\left|{A}\left({m}\right){{X}}^{{m}}\right|\left|{{Y}}^{{m}}\right|$
104 80 101 absmuld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}{{X}}^{{m}}\right|=\left|{A}\left({m}\right){{Y}}^{{m}}\right|\left|{{X}}^{{m}}\right|$
105 77 79 101 mul32d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {A}\left({m}\right){{Y}}^{{m}}{{X}}^{{m}}={A}\left({m}\right){{X}}^{{m}}{{Y}}^{{m}}$
106 105 fveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}{{X}}^{{m}}\right|=\left|{A}\left({m}\right){{X}}^{{m}}{{Y}}^{{m}}\right|$
107 83 69 absexpd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{{X}}^{{m}}\right|={\left|{X}\right|}^{{m}}$
108 107 oveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|\left|{{X}}^{{m}}\right|=\left|{A}\left({m}\right){{Y}}^{{m}}\right|{\left|{X}\right|}^{{m}}$
109 104 106 108 3eqtr3d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}{{Y}}^{{m}}\right|=\left|{A}\left({m}\right){{Y}}^{{m}}\right|{\left|{X}\right|}^{{m}}$
110 78 69 absexpd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{{Y}}^{{m}}\right|={\left|{Y}\right|}^{{m}}$
111 110 oveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}\right|\left|{{Y}}^{{m}}\right|=\left|{A}\left({m}\right){{X}}^{{m}}\right|{\left|{Y}\right|}^{{m}}$
112 103 109 111 3eqtr3d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{Y}}^{{m}}\right|{\left|{X}\right|}^{{m}}=\left|{A}\left({m}\right){{X}}^{{m}}\right|{\left|{Y}\right|}^{{m}}$
113 85 recnd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {\left|{X}\right|}^{{m}}\in ℂ$
114 113 mulid2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 1{\left|{X}\right|}^{{m}}={\left|{X}\right|}^{{m}}$
115 100 112 114 3brtr3d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}\right|{\left|{Y}\right|}^{{m}}\le {\left|{X}\right|}^{{m}}$
116 102 abscld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}\right|\in ℝ$
117 25 adantr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{Y}\right|\in ℝ$
118 117 69 reexpcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {\left|{Y}\right|}^{{m}}\in ℝ$
119 eluzelz ${⊢}{m}\in {ℤ}_{\ge {j}}\to {m}\in ℤ$
120 119 adantl ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in ℤ$
121 30 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0<\left|{Y}\right|$
122 expgt0 ${⊢}\left(\left|{Y}\right|\in ℝ\wedge {m}\in ℤ\wedge 0<\left|{Y}\right|\right)\to 0<{\left|{Y}\right|}^{{m}}$
123 117 120 121 122 syl3anc ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0<{\left|{Y}\right|}^{{m}}$
124 lemuldiv ${⊢}\left(\left|{A}\left({m}\right){{X}}^{{m}}\right|\in ℝ\wedge {\left|{X}\right|}^{{m}}\in ℝ\wedge \left({\left|{Y}\right|}^{{m}}\in ℝ\wedge 0<{\left|{Y}\right|}^{{m}}\right)\right)\to \left(\left|{A}\left({m}\right){{X}}^{{m}}\right|{\left|{Y}\right|}^{{m}}\le {\left|{X}\right|}^{{m}}↔\left|{A}\left({m}\right){{X}}^{{m}}\right|\le \frac{{\left|{X}\right|}^{{m}}}{{\left|{Y}\right|}^{{m}}}\right)$
125 116 85 118 123 124 syl112anc ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left(\left|{A}\left({m}\right){{X}}^{{m}}\right|{\left|{Y}\right|}^{{m}}\le {\left|{X}\right|}^{{m}}↔\left|{A}\left({m}\right){{X}}^{{m}}\right|\le \frac{{\left|{X}\right|}^{{m}}}{{\left|{Y}\right|}^{{m}}}\right)$
126 115 125 mpbid ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{A}\left({m}\right){{X}}^{{m}}\right|\le \frac{{\left|{X}\right|}^{{m}}}{{\left|{Y}\right|}^{{m}}}$
127 1 pserval2 ${⊢}\left({X}\in ℂ\wedge {m}\in {ℕ}_{0}\right)\to {G}\left({X}\right)\left({m}\right)={A}\left({m}\right){{X}}^{{m}}$
128 83 69 127 syl2anc ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {G}\left({X}\right)\left({m}\right)={A}\left({m}\right){{X}}^{{m}}$
129 128 fveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{G}\left({X}\right)\left({m}\right)\right|=\left|{A}\left({m}\right){{X}}^{{m}}\right|$
130 23 recnd ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left|{X}\right|\in ℂ$
131 130 adantr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{X}\right|\in ℂ$
132 25 recnd ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to \left|{Y}\right|\in ℂ$
133 132 adantr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{Y}\right|\in ℂ$
134 31 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{Y}\right|\ne 0$
135 131 133 134 69 expdivd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}=\frac{{\left|{X}\right|}^{{m}}}{{\left|{Y}\right|}^{{m}}}$
136 126 129 135 3brtr4d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{G}\left({X}\right)\left({m}\right)\right|\le {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
137 71 73 74 75 136 lemul2ad ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\left|{G}\left({X}\right)\left({m}\right)\right|\le {m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
138 74 71 remulcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\left|{G}\left({X}\right)\left({m}\right)\right|\in ℝ$
139 70 absge0d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0\le \left|{G}\left({X}\right)\left({m}\right)\right|$
140 74 71 75 139 mulge0d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 0\le {m}\left|{G}\left({X}\right)\left({m}\right)\right|$
141 138 140 absidd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{m}\left|{G}\left({X}\right)\left({m}\right)\right|\right|={m}\left|{G}\left({X}\right)\left({m}\right)\right|$
142 74 73 remulcld ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}\in ℝ$
143 142 recnd ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}\in ℂ$
144 143 mulid2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 1{m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}={m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
145 137 141 144 3brtr4d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{m}\left|{G}\left({X}\right)\left({m}\right)\right|\right|\le 1{m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
146 ovex ${⊢}{m}\left|{G}\left({X}\right)\left({m}\right)\right|\in \mathrm{V}$
147 7 fvmpt2 ${⊢}\left({m}\in {ℕ}_{0}\wedge {m}\left|{G}\left({X}\right)\left({m}\right)\right|\in \mathrm{V}\right)\to {H}\left({m}\right)={m}\left|{G}\left({X}\right)\left({m}\right)\right|$
148 69 146 147 sylancl ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {H}\left({m}\right)={m}\left|{G}\left({X}\right)\left({m}\right)\right|$
149 148 fveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{H}\left({m}\right)\right|=\left|{m}\left|{G}\left({X}\right)\left({m}\right)\right|\right|$
150 id ${⊢}{i}={m}\to {i}={m}$
151 oveq2 ${⊢}{i}={m}\to {\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}={\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
152 150 151 oveq12d ${⊢}{i}={m}\to {i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}={m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
153 ovex ${⊢}{m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}\in \mathrm{V}$
154 152 37 153 fvmpt ${⊢}{m}\in {ℕ}_{0}\to \left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\left({m}\right)={m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
155 69 154 syl ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\left({m}\right)={m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
156 155 oveq2d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to 1\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\left({m}\right)=1{m}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{m}}$
157 145 149 156 3brtr4d ${⊢}\left(\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left|{H}\left({m}\right)\right|\le 1\left({i}\in {ℕ}_{0}⟼{i}{\left(\frac{\left|{X}\right|}{\left|{Y}\right|}\right)}^{{i}}\right)\left({m}\right)$
158 8 19 39 49 65 66 157 cvgcmpce ${⊢}\left({\phi }\wedge \left({j}\in {ℕ}_{0}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{A}\left({k}\right){{Y}}^{{k}}\right|<1\right)\right)\to seq0\left(+,{H}\right)\in \mathrm{dom}⇝$
159 18 158 rexlimddv ${⊢}{\phi }\to seq0\left(+,{H}\right)\in \mathrm{dom}⇝$