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

Metamath Proof Explorer

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