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	eqtrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 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	mullidd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 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	mullidd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( 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	mullidd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( 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 ⇝ )