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 ⇝ )