Theorem logtayllem

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

	Ref	Expression
Assertion	logtayllem	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ) ∈ dom ⇝ )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2		1nn0	⊢ 1 ∈ ℕ0
3	2	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℕ0 )
4		oveq2	⊢ ( 𝑛 = 𝑘 → ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
5		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) )
6		ovex	⊢ ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
9		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
10	9	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
11		reexpcl	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
12	10 11	sylan	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
13	8 12	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
14		eqeq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 = 0 ↔ 𝑘 = 0 ) )
15		oveq2	⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
16	14 15	ifbieq2d	⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) = if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) )
17		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
18	16 17	oveq12d	⊢ ( 𝑛 = 𝑘 → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) = ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
19		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) )
20		ovex	⊢ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ V
21	18 19 20	fvmpt	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) = ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
22	21	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) = ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
23		0cnd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → 0 ∈ ℂ )
24		nn0cn	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
25	24	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
26		neqne	⊢ ( ¬ 𝑘 = 0 → 𝑘 ≠ 0 )
27		reccl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) → ( 1 / 𝑘 ) ∈ ℂ )
28	25 26 27	syl2an	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 = 0 ) → ( 1 / 𝑘 ) ∈ ℂ )
29	23 28	ifclda	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) ∈ ℂ )
30		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
31	30	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
32	29 31	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
33	22 32	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
34	10	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
35		absidm	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
36	35	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
37		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
38	36 37	eqbrtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( abs ‘ 𝐴 ) ) < 1 )
39	34 38 8	geolim	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝐴 ) ) ) )
40		seqex	⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ) ∈ V
41		ovex	⊢ ( 1 / ( 1 − ( abs ‘ 𝐴 ) ) ) ∈ V
42	40 41	breldm	⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝐴 ) ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ) ∈ dom ⇝ )
43	39 42	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ) ∈ dom ⇝ )
44		1red	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℝ )
45		elnnuz	⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
46		nnrecre	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
47	46	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
48	47	recnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℂ )
49		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
50	49 31	sylan2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
51	48 50	absmuld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 1 / 𝑘 ) ) · ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) ) )
52		nnrp	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
53	52	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ+ )
54	53	rpreccld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ+ )
55	54	rpge0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 1 / 𝑘 ) )
56	47 55	absidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( 1 / 𝑘 ) ) = ( 1 / 𝑘 ) )
57		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
58		absexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
59	57 49 58	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
60	56 59	oveq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ ( 1 / 𝑘 ) ) · ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 1 / 𝑘 ) · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
61	51 60	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 1 / 𝑘 ) · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
62		1red	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
63	49 12	sylan2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
64	50	absge0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) )
65	64 59	breqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
66		nnge1	⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
67	66	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑘 )
68		0lt1	⊢ 0 < 1
69	68	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 0 < 1 )
70		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
71	70	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
72		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
73	72	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 0 < 𝑘 )
74		lerec	⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( 1 ≤ 𝑘 ↔ ( 1 / 𝑘 ) ≤ ( 1 / 1 ) ) )
75	62 69 71 73 74	syl22anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 ≤ 𝑘 ↔ ( 1 / 𝑘 ) ≤ ( 1 / 1 ) ) )
76	67 75	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ≤ ( 1 / 1 ) )
77		1div1e1	⊢ ( 1 / 1 ) = 1
78	76 77	breqtrdi	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ≤ 1 )
79	47 62 63 65 78	lemul1ad	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) ≤ ( 1 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
80	61 79	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ≤ ( 1 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
81	49 22	sylan2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) = ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
82		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
83	82	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
84	83	neneqd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ¬ 𝑘 = 0 )
85	84	iffalsed	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) = ( 1 / 𝑘 ) )
86	85	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
87	81 86	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
88	87	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( abs ‘ ( ( 1 / 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
89	49 8	sylan2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
90	89	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 1 · ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ) = ( 1 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
91	80 88 90	3brtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) ) ≤ ( 1 · ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ) )
92	45 91	sylan2br	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ‘ 𝑘 ) ) ≤ ( 1 · ( ( 𝑛 ∈ ℕ0 ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ) )
93	1 3 13 33 43 44 92	cvgcmpce	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴 ↑ 𝑛 ) ) ) ) ∈ dom ⇝ )