Metamath Proof Explorer

Theorem geomulcvg

Description: The geometric series converges even if it is multiplied by k to result in the larger series k x. A ^ k . (Contributed by Mario Carneiro, 27-Mar-2015)

Ref Expression
Hypothesis geomulcvg.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) )
Assertion geomulcvg ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 geomulcvg.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) )
2 elnn0 ⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
3 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → 𝐴 = 0 )
4 3 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → ( 𝐴 ↑ 𝑘 ) = ( 0 ↑ 𝑘 ) )
5 0exp ⊢ ( 𝑘 ∈ ℕ → ( 0 ↑ 𝑘 ) = 0 )
6 4 5 sylan9eq ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) = 0 )
7 6 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = ( 𝑘 · 0 ) )
8 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
9 8 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
10 9 mul01d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 0 ) = 0 )
11 7 10 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
12 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
13 12 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = ( 0 · ( 𝐴 ↑ 𝑘 ) ) )
14 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → 𝐴 ∈ ℂ )
15 0nn0 ⊢ 0 ∈ ℕ0
16 12 15 eqeltrdi ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → 𝑘 ∈ ℕ0 )
17 14 16 expcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
18 17 mul02d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → ( 0 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
19 13 18 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 = 0 ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
20 11 19 jaodan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
21 2 20 sylan2b ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
22 21 mpteq2dva ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ 0 ) )
23 1 22 syl5eq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → 𝐹 = ( 𝑘 ∈ ℕ0 ↦ 0 ) )
24 fconstmpt ⊢ ( ℕ0 × { 0 } ) = ( 𝑘 ∈ ℕ0 ↦ 0 )
25 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
26 25 xpeq1i ⊢ ( ℕ0 × { 0 } ) = ( ( ℤ≥ ‘ 0 ) × { 0 } )
27 24 26 eqtr3i ⊢ ( 𝑘 ∈ ℕ0 ↦ 0 ) = ( ( ℤ≥ ‘ 0 ) × { 0 } )
28 23 27 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → 𝐹 = ( ( ℤ≥ ‘ 0 ) × { 0 } ) )
29 28 seqeq3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → seq 0 ( + , 𝐹 ) = seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) )
30 0z ⊢ 0 ∈ ℤ
31 serclim0 ⊢ ( 0 ∈ ℤ → seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) ⇝ 0 )
32 30 31 ax-mp ⊢ seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) ⇝ 0
33 29 32 eqbrtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → seq 0 ( + , 𝐹 ) ⇝ 0 )
34 seqex ⊢ seq 0 ( + , 𝐹 ) ∈ V
35 c0ex ⊢ 0 ∈ V
36 34 35 breldm ⊢ ( seq 0 ( + , 𝐹 ) ⇝ 0 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
37 33 36 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 = 0 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
38 1red ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → 1 ∈ ℝ )
39 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
40 39 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
41 peano2re ⊢ ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
42 40 41 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
43 42 rehalfcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℝ )
44 43 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℝ )
45 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
46 45 adantlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
47 44 46 rerpdivcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ∈ ℝ )
48 40 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
49 48 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
50 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
51 1re ⊢ 1 ∈ ℝ
52 avglt1 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) < 1 ↔ ( abs ‘ 𝐴 ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) )
53 40 51 52 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) < 1 ↔ ( abs ‘ 𝐴 ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) )
54 50 53 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
55 49 54 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 · ( abs ‘ 𝐴 ) ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
56 55 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( 1 · ( abs ‘ 𝐴 ) ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
57 38 44 46 ltmuldivd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( ( 1 · ( abs ‘ 𝐴 ) ) < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↔ 1 < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ) )
58 56 57 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → 1 < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) )
59 expmulnbnd ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ∈ ℝ ∧ 1 < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ) → ∃ 𝑛 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) )
60 38 47 58 59 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ∃ 𝑛 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) )
61 eluznn0 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ0 )
62 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
63 62 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
64 63 mulid2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 · 𝑘 ) = 𝑘 )
65 43 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℂ )
66 65 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℂ )
67 48 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
68 46 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
69 68 rpne0d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
70 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
71 66 67 69 70 expdivd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) = ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
72 64 71 breq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ↔ 𝑘 < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) ) )
73 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
74 73 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
75 reexpcl ⊢ ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ∈ ℝ )
76 44 75 sylan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ∈ ℝ )
77 40 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
78 reexpcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
79 77 78 sylan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ )
80 77 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
81 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
82 81 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
83 68 rpgt0d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 0 < ( abs ‘ 𝐴 ) )
84 expgt0 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < ( abs ‘ 𝐴 ) ) → 0 < ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
85 80 82 83 84 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → 0 < ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
86 ltmuldiv ⊢ ( ( 𝑘 ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ∈ ℝ ∧ ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) ) → ( ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ↔ 𝑘 < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) ) )
87 74 76 79 85 86 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ↔ 𝑘 < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) ) )
88 72 87 bitr4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ↔ ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) )
89 61 88 sylan2 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ↔ ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) )
90 89 anassrs ⊢ ( ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ↔ ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) )
91 90 ralbidva ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) )
92 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) → 𝑛 ∈ ℕ0 )
93 oveq2 ⊢ ( 𝑘 = 𝑚 → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
94 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) )
95 ovex ⊢ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ∈ V
96 93 94 95 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
97 96 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
98 43 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ∈ ℝ )
99 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
100 98 99 reexpcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ∈ ℝ )
101 97 100 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) ∈ ℝ )
102 id ⊢ ( 𝑘 = 𝑚 → 𝑘 = 𝑚 )
103 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ 𝑚 ) )
104 102 103 oveq12d ⊢ ( 𝑘 = 𝑚 → ( 𝑘 · ( 𝐴 ↑ 𝑘 ) ) = ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) )
105 ovex ⊢ ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ∈ V
106 104 1 105 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( 𝐹 ‘ 𝑚 ) = ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) )
107 106 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) )
108 nn0cn ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
109 108 adantl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
110 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑚 ) ∈ ℂ )
111 110 ad4ant14 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑚 ) ∈ ℂ )
112 109 111 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ∈ ℂ )
113 107 112 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
114 0red ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ∈ ℝ )
115 absge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
116 115 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ≤ ( abs ‘ 𝐴 ) )
117 114 40 43 116 54 lelttrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 < ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
118 114 43 117 ltled ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ≤ ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
119 43 118 absidd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) = ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) )
120 avglt2 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) < 1 ↔ ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) < 1 ) )
121 40 51 120 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) < 1 ↔ ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) < 1 ) )
122 50 121 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) < 1 )
123 119 122 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) < 1 )
124 oveq2 ⊢ ( 𝑘 = 𝑛 → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑛 ) )
125 ovex ⊢ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑛 ) ∈ V
126 124 94 125 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑛 ) )
127 126 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑛 ) )
128 65 123 127 geolim ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ⇝ ( 1 / ( 1 − ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) ) )
129 seqex ⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∈ V
130 ovex ⊢ ( 1 / ( 1 − ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) ) ∈ V
131 129 130 breldm ⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ⇝ ( 1 / ( 1 − ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ )
132 128 131 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ )
133 132 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ )
134 1red ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) → 1 ∈ ℝ )
135 eluznn0 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ℕ0 )
136 92 135 sylan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ℕ0 )
137 136 nn0red ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ℝ )
138 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐴 ∈ ℂ )
139 138 abscld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
140 139 136 reexpcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ∈ ℝ )
141 137 140 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) ∈ ℝ )
142 136 100 syldan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ∈ ℝ )
143 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) )
144 oveq2 ⊢ ( 𝑘 = 𝑚 → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) )
145 102 144 oveq12d ⊢ ( 𝑘 = 𝑚 → ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) = ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) )
146 145 93 breq12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ↔ ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ) )
147 146 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
148 143 147 sylan ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
149 141 142 148 ltled ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
150 136 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ℂ )
151 138 136 expcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐴 ↑ 𝑚 ) ∈ ℂ )
152 150 151 absmuld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ) = ( ( abs ‘ 𝑚 ) · ( abs ‘ ( 𝐴 ↑ 𝑚 ) ) ) )
153 136 nn0ge0d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 0 ≤ 𝑚 )
154 137 153 absidd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ 𝑚 ) = 𝑚 )
155 138 136 absexpd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝐴 ↑ 𝑚 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) )
156 154 155 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( abs ‘ 𝑚 ) · ( abs ‘ ( 𝐴 ↑ 𝑚 ) ) ) = ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) )
157 152 156 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ) = ( 𝑚 · ( ( abs ‘ 𝐴 ) ↑ 𝑚 ) ) )
158 142 recnd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ∈ ℂ )
159 158 mulid2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 1 · ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
160 149 157 159 3brtr4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ) ≤ ( 1 · ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ) )
161 136 106 syl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) )
162 161 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑚 ) ) = ( abs ‘ ( 𝑚 · ( 𝐴 ↑ 𝑚 ) ) ) )
163 136 96 syl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) = ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) )
164 163 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 1 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) ) = ( 1 · ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑚 ) ) )
165 160 162 164 3brtr4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( 1 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ‘ 𝑚 ) ) )
166 25 92 101 113 133 134 165 cvgcmpce ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) ) ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
167 166 expr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ ) )
168 167 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑘 · ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) < ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) ↑ 𝑘 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ ) )
169 91 168 sylbid ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ ) )
170 169 rexlimdva ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → ( ∃ 𝑛 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 1 · 𝑘 ) < ( ( ( ( ( abs ‘ 𝐴 ) + 1 ) / 2 ) / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ ) )
171 60 170 mpd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝐴 ≠ 0 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
172 37 171 pm2.61dane ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )