Metamath Proof Explorer


Theorem logtayl

Description: The Taylor series for -u log ( 1 - A ) . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logtayl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz 0 = ( ℤ ‘ 0 )
2 0zd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ∈ ℤ )
3 eqeq1 ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
4 oveq2 ( 𝑘 = 𝑛 → ( 1 / 𝑘 ) = ( 1 / 𝑛 ) )
5 3 4 ifbieq2d ( 𝑘 = 𝑛 → if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
6 oveq2 ( 𝑘 = 𝑛 → ( 𝐴𝑘 ) = ( 𝐴𝑛 ) )
7 5 6 oveq12d ( 𝑘 = 𝑛 → ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
8 eqid ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) )
9 ovex ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) ∈ V
10 7 8 9 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
11 10 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
12 0cnd ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → 0 ∈ ℂ )
13 simpr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
14 elnn0 ( 𝑛 ∈ ℕ0 ↔ ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) )
15 13 14 sylib ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) )
16 15 ord ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑛 ∈ ℕ → 𝑛 = 0 ) )
17 16 con1d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑛 = 0 → 𝑛 ∈ ℕ ) )
18 17 imp ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
19 18 nnrecred ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 1 / 𝑛 ) ∈ ℝ )
20 19 recnd ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 1 / 𝑛 ) ∈ ℂ )
21 12 20 ifclda ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) ∈ ℂ )
22 expcl ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴𝑛 ) ∈ ℂ )
23 22 adantlr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴𝑛 ) ∈ ℂ )
24 21 23 mulcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) ∈ ℂ )
25 logtayllem ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ∈ dom ⇝ )
26 1 2 11 24 25 isumclim2 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ⇝ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
27 simpl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
28 0cn 0 ∈ ℂ
29 eqid ( abs ∘ − ) = ( abs ∘ − )
30 29 cnmetdval ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝐴 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝐴 − 0 ) ) )
31 27 28 30 sylancl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝐴 − 0 ) ) )
32 subid1 ( 𝐴 ∈ ℂ → ( 𝐴 − 0 ) = 𝐴 )
33 32 adantr ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 − 0 ) = 𝐴 )
34 33 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( 𝐴 − 0 ) ) = ( abs ‘ 𝐴 ) )
35 31 34 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ( abs ∘ − ) 0 ) = ( abs ‘ 𝐴 ) )
36 simpr ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
37 35 36 eqbrtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ( abs ∘ − ) 0 ) < 1 )
38 cnxmet ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
39 1xr 1 ∈ ℝ*
40 elbl3 ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ) → ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝐴 ( abs ∘ − ) 0 ) < 1 ) )
41 38 39 40 mpanl12 ( ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝐴 ( abs ∘ − ) 0 ) < 1 ) )
42 28 27 41 sylancr ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝐴 ( abs ∘ − ) 0 ) < 1 ) )
43 37 42 mpbird ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
44 tru
45 eqid ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 1 )
46 0cnd ( ⊤ → 0 ∈ ℂ )
47 39 a1i ( ⊤ → 1 ∈ ℝ* )
48 ax-1cn 1 ∈ ℂ
49 blssm ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ )
50 38 28 39 49 mp3an ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ
51 50 sseli ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑦 ∈ ℂ )
52 subcl ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 1 − 𝑦 ) ∈ ℂ )
53 48 51 52 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 − 𝑦 ) ∈ ℂ )
54 51 abscld ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) ∈ ℝ )
55 29 cnmetdval ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑦 − 0 ) ) )
56 51 28 55 sylancl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑦 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑦 − 0 ) ) )
57 51 subid1d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑦 − 0 ) = 𝑦 )
58 57 fveq2d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ ( 𝑦 − 0 ) ) = ( abs ‘ 𝑦 ) )
59 56 58 eqtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑦 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑦 ) )
60 elbl3 ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 0 ) < 1 ) )
61 38 39 60 mpanl12 ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 0 ) < 1 ) )
62 28 51 61 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 0 ) < 1 ) )
63 62 ibi ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑦 ( abs ∘ − ) 0 ) < 1 )
64 59 63 eqbrtrrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) < 1 )
65 54 64 gtned ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 1 ≠ ( abs ‘ 𝑦 ) )
66 abs1 ( abs ‘ 1 ) = 1
67 fveq2 ( 1 = 𝑦 → ( abs ‘ 1 ) = ( abs ‘ 𝑦 ) )
68 66 67 eqtr3id ( 1 = 𝑦 → 1 = ( abs ‘ 𝑦 ) )
69 68 necon3i ( 1 ≠ ( abs ‘ 𝑦 ) → 1 ≠ 𝑦 )
70 65 69 syl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 1 ≠ 𝑦 )
71 subeq0 ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 1 − 𝑦 ) = 0 ↔ 1 = 𝑦 ) )
72 71 necon3bid ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 1 − 𝑦 ) ≠ 0 ↔ 1 ≠ 𝑦 ) )
73 48 51 72 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 1 − 𝑦 ) ≠ 0 ↔ 1 ≠ 𝑦 ) )
74 70 73 mpbird ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 − 𝑦 ) ≠ 0 )
75 53 74 logcld ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( log ‘ ( 1 − 𝑦 ) ) ∈ ℂ )
76 75 negcld ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → - ( log ‘ ( 1 − 𝑦 ) ) ∈ ℂ )
77 76 adantl ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → - ( log ‘ ( 1 − 𝑦 ) ) ∈ ℂ )
78 77 fmpttd ( ⊤ → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) : ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⟶ ℂ )
79 51 absge0d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 0 ≤ ( abs ‘ 𝑦 ) )
80 54 rexrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) ∈ ℝ* )
81 peano2re ( ( abs ‘ 𝑦 ) ∈ ℝ → ( ( abs ‘ 𝑦 ) + 1 ) ∈ ℝ )
82 54 81 syl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( abs ‘ 𝑦 ) + 1 ) ∈ ℝ )
83 82 rehalfcld ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ∈ ℝ )
84 83 rexrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ∈ ℝ* )
85 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
86 eqeq1 ( 𝑚 = 𝑗 → ( 𝑚 = 0 ↔ 𝑗 = 0 ) )
87 oveq2 ( 𝑚 = 𝑗 → ( 1 / 𝑚 ) = ( 1 / 𝑗 ) )
88 86 87 ifbieq2d ( 𝑚 = 𝑗 → if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) = if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) )
89 eqid ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) )
90 c0ex 0 ∈ V
91 ovex ( 1 / 𝑗 ) ∈ V
92 90 91 ifex if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) ∈ V
93 88 89 92 fvmpt ( 𝑗 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑗 ) = if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) )
94 93 eqcomd ( 𝑗 ∈ ℕ0 → if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) = ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑗 ) )
95 94 oveq1d ( 𝑗 ∈ ℕ0 → ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) = ( ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑗 ) · ( 𝑥𝑗 ) ) )
96 95 mpteq2ia ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑗 ) · ( 𝑥𝑗 ) ) )
97 96 mpteq2i ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑗 ) · ( 𝑥𝑗 ) ) ) )
98 0cnd ( ( ( ⊤ ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 0 ) → 0 ∈ ℂ )
99 nn0cn ( 𝑚 ∈ ℕ0𝑚 ∈ ℂ )
100 99 adantl ( ( ⊤ ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
101 neqne ( ¬ 𝑚 = 0 → 𝑚 ≠ 0 )
102 reccl ( ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) → ( 1 / 𝑚 ) ∈ ℂ )
103 100 101 102 syl2an ( ( ( ⊤ ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 = 0 ) → ( 1 / 𝑚 ) ∈ ℂ )
104 98 103 ifclda ( ( ⊤ ∧ 𝑚 ∈ ℕ0 ) → if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ∈ ℂ )
105 104 fmpttd ( ⊤ → ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) : ℕ0 ⟶ ℂ )
106 recn ( 𝑟 ∈ ℝ → 𝑟 ∈ ℂ )
107 oveq1 ( 𝑥 = 𝑟 → ( 𝑥𝑗 ) = ( 𝑟𝑗 ) )
108 107 oveq2d ( 𝑥 = 𝑟 → ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) )
109 108 mpteq2dv ( 𝑥 = 𝑟 → ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) )
110 eqid ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) )
111 nn0ex 0 ∈ V
112 111 mptex ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ∈ V
113 109 110 112 fvmpt ( 𝑟 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) )
114 106 113 syl ( 𝑟 ∈ ℝ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) )
115 114 eqcomd ( 𝑟 ∈ ℝ → ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) )
116 115 seqeq3d ( 𝑟 ∈ ℝ → seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) = seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) ) )
117 116 eleq1d ( 𝑟 ∈ ℝ → ( seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ ) )
118 117 rabbiia { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } = { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ }
119 118 supeq1i sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
120 97 105 119 radcnvcl ( ⊤ → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
121 85 120 sselid ( ⊤ → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
122 44 121 mp1i ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
123 1re 1 ∈ ℝ
124 avglt1 ( ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑦 ) < 1 ↔ ( abs ‘ 𝑦 ) < ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) )
125 54 123 124 sylancl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( abs ‘ 𝑦 ) < 1 ↔ ( abs ‘ 𝑦 ) < ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) )
126 64 125 mpbid ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) < ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) )
127 0red ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 0 ∈ ℝ )
128 127 54 83 79 126 lelttrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 0 < ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) )
129 127 83 128 ltled ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 0 ≤ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) )
130 83 129 absidd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) = ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) )
131 44 105 mp1i ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) : ℕ0 ⟶ ℂ )
132 83 recnd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ∈ ℂ )
133 oveq1 ( 𝑥 = ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) → ( 𝑥𝑗 ) = ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) )
134 133 oveq2d ( 𝑥 = ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) → ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) )
135 134 mpteq2dv ( 𝑥 = ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) → ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
136 111 mptex ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ∈ V
137 135 110 136 fvmpt ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
138 132 137 syl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
139 138 seqeq3d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) ) = seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) )
140 avglt2 ( ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑦 ) < 1 ↔ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) < 1 ) )
141 54 123 140 sylancl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( abs ‘ 𝑦 ) < 1 ↔ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) < 1 ) )
142 64 141 mpbid ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) < 1 )
143 130 142 eqbrtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) < 1 )
144 logtayllem ( ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ∈ ℂ ∧ ( abs ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) < 1 ) → seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) ∈ dom ⇝ )
145 132 143 144 syl2anc ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) ∈ dom ⇝ )
146 139 145 eqeltrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → seq 0 ( + , ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) ) ∈ dom ⇝ )
147 97 131 119 132 146 radcnvle ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
148 130 147 eqbrtrrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( ( abs ‘ 𝑦 ) + 1 ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
149 80 84 122 126 148 xrltletrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
150 0re 0 ∈ ℝ
151 elico2 ( ( 0 ∈ ℝ ∧ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) → ( ( abs ‘ 𝑦 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
152 150 122 151 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( abs ‘ 𝑦 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
153 54 79 149 152 mpbir3and ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ 𝑦 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
154 absf abs : ℂ ⟶ ℝ
155 ffn ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
156 elpreima ( abs Fn ℂ → ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
157 154 155 156 mp2b ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
158 51 153 157 sylanbrc ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
159 cnvimass ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⊆ dom abs
160 154 fdmi dom abs = ℂ
161 159 160 sseqtri ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⊆ ℂ
162 161 sseli ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → 𝑦 ∈ ℂ )
163 oveq1 ( 𝑥 = 𝑦 → ( 𝑥𝑗 ) = ( 𝑦𝑗 ) )
164 163 oveq2d ( 𝑥 = 𝑦 → ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) )
165 164 mpteq2dv ( 𝑥 = 𝑦 → ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) )
166 111 mptex ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) ∈ V
167 165 110 166 fvmpt ( 𝑦 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) )
168 167 adantr ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) )
169 168 fveq1d ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) ‘ 𝑛 ) )
170 eqeq1 ( 𝑗 = 𝑛 → ( 𝑗 = 0 ↔ 𝑛 = 0 ) )
171 oveq2 ( 𝑗 = 𝑛 → ( 1 / 𝑗 ) = ( 1 / 𝑛 ) )
172 170 171 ifbieq2d ( 𝑗 = 𝑛 → if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
173 oveq2 ( 𝑗 = 𝑛 → ( 𝑦𝑗 ) = ( 𝑦𝑛 ) )
174 172 173 oveq12d ( 𝑗 = 𝑛 → ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
175 eqid ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) )
176 ovex ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ∈ V
177 174 175 176 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) ‘ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
178 177 adantl ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑦𝑗 ) ) ) ‘ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
179 169 178 eqtr2d ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) )
180 179 sumeq2dv ( 𝑦 ∈ ℂ → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) )
181 162 180 syl ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) )
182 181 mpteq2ia ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) = ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) )
183 eqid ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) = ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
184 eqid if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑧 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑧 ) + 1 ) ) = if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑧 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑧 ) + 1 ) )
185 97 182 105 119 183 184 psercn ( ⊤ → ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ∈ ( ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cn→ ℂ ) )
186 cncff ( ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ∈ ( ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cn→ ℂ ) → ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) : ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⟶ ℂ )
187 185 186 syl ( ⊤ → ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) : ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⟶ ℂ )
188 187 fvmptelrn ( ( ⊤ ∧ 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ∈ ℂ )
189 158 188 sylan2 ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ∈ ℂ )
190 189 fmpttd ( ⊤ → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) : ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⟶ ℂ )
191 cnelprrecn ℂ ∈ { ℝ , ℂ }
192 191 a1i ( ⊤ → ℂ ∈ { ℝ , ℂ } )
193 75 adantl ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ( log ‘ ( 1 − 𝑦 ) ) ∈ ℂ )
194 ovexd ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) ∈ V )
195 29 cnmetdval ( ( 1 ∈ ℂ ∧ ( 1 − 𝑦 ) ∈ ℂ ) → ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) = ( abs ‘ ( 1 − ( 1 − 𝑦 ) ) ) )
196 48 53 195 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) = ( abs ‘ ( 1 − ( 1 − 𝑦 ) ) ) )
197 nncan ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 1 − ( 1 − 𝑦 ) ) = 𝑦 )
198 48 51 197 sylancr ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 − ( 1 − 𝑦 ) ) = 𝑦 )
199 198 fveq2d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( abs ‘ ( 1 − ( 1 − 𝑦 ) ) ) = ( abs ‘ 𝑦 ) )
200 196 199 eqtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) = ( abs ‘ 𝑦 ) )
201 200 64 eqbrtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) < 1 )
202 elbl ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( ( 1 − 𝑦 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( ( 1 − 𝑦 ) ∈ ℂ ∧ ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) < 1 ) ) )
203 38 48 39 202 mp3an ( ( 1 − 𝑦 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( ( 1 − 𝑦 ) ∈ ℂ ∧ ( 1 ( abs ∘ − ) ( 1 − 𝑦 ) ) < 1 ) )
204 53 201 203 sylanbrc ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 − 𝑦 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) )
205 204 adantl ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ( 1 − 𝑦 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) )
206 neg1cn - 1 ∈ ℂ
207 206 a1i ( ( ⊤ ∧ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → - 1 ∈ ℂ )
208 eqid ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
209 208 dvlog2lem ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
210 209 sseli ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
211 210 eldifad ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑥 ∈ ℂ )
212 eqid ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
213 212 logdmn0 ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑥 ≠ 0 )
214 210 213 syl ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑥 ≠ 0 )
215 211 214 logcld ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( log ‘ 𝑥 ) ∈ ℂ )
216 215 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
217 ovexd ( ( ⊤ ∧ 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → ( 1 / 𝑥 ) ∈ V )
218 simpr ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
219 48 218 52 sylancr ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → ( 1 − 𝑦 ) ∈ ℂ )
220 206 a1i ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → - 1 ∈ ℂ )
221 1cnd ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℂ )
222 0cnd ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → 0 ∈ ℂ )
223 1cnd ( ⊤ → 1 ∈ ℂ )
224 192 223 dvmptc ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 1 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
225 192 dvmptid ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
226 192 221 222 224 218 221 225 dvmptsub ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 0 − 1 ) ) )
227 df-neg - 1 = ( 0 − 1 )
228 227 mpteq2i ( 𝑦 ∈ ℂ ↦ - 1 ) = ( 𝑦 ∈ ℂ ↦ ( 0 − 1 ) )
229 226 228 eqtr4di ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ - 1 ) )
230 50 a1i ( ⊤ → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ )
231 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
232 231 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
233 232 toponrestid ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
234 231 cnfldtopn ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
235 234 blopn ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ ( TopOpen ‘ ℂfld ) )
236 38 28 39 235 mp3an ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ ( TopOpen ‘ ℂfld )
237 236 a1i ( ⊤ → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ ( TopOpen ‘ ℂfld ) )
238 192 219 220 229 230 233 231 237 dvmptres ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - 1 ) )
239 logf1o log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
240 f1of ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
241 239 240 ax-mp log : ( ℂ ∖ { 0 } ) ⟶ ran log
242 212 logdmss ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } )
243 209 242 sstri ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( ℂ ∖ { 0 } )
244 fssres ( ( log : ( ℂ ∖ { 0 } ) ⟶ ran log ∧ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) : ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⟶ ran log )
245 241 243 244 mp2an ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) : ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⟶ ran log
246 245 a1i ( ⊤ → ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) : ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⟶ ran log )
247 246 feqmptd ( ⊤ → ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) = ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ‘ 𝑥 ) ) )
248 fvres ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
249 248 mpteq2ia ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( log ‘ 𝑥 ) )
250 247 249 eqtrdi ( ⊤ → ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) = ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( log ‘ 𝑥 ) ) )
251 250 oveq2d ( ⊤ → ( ℂ D ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ) = ( ℂ D ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( log ‘ 𝑥 ) ) ) )
252 208 dvlog2 ( ℂ D ( log ↾ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ) = ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / 𝑥 ) )
253 251 252 eqtr3di ( ⊤ → ( ℂ D ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / 𝑥 ) ) )
254 fveq2 ( 𝑥 = ( 1 − 𝑦 ) → ( log ‘ 𝑥 ) = ( log ‘ ( 1 − 𝑦 ) ) )
255 oveq2 ( 𝑥 = ( 1 − 𝑦 ) → ( 1 / 𝑥 ) = ( 1 / ( 1 − 𝑦 ) ) )
256 192 192 205 207 216 217 238 253 254 255 dvmptco ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( log ‘ ( 1 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) ) )
257 192 193 194 256 dvmptneg ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) ) )
258 53 74 reccld ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 / ( 1 − 𝑦 ) ) ∈ ℂ )
259 mulcom ( ( ( 1 / ( 1 − 𝑦 ) ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) = ( - 1 · ( 1 / ( 1 − 𝑦 ) ) ) )
260 258 206 259 sylancl ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) = ( - 1 · ( 1 / ( 1 − 𝑦 ) ) ) )
261 258 mulm1d ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( - 1 · ( 1 / ( 1 − 𝑦 ) ) ) = - ( 1 / ( 1 − 𝑦 ) ) )
262 260 261 eqtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) = - ( 1 / ( 1 − 𝑦 ) ) )
263 262 negeqd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → - ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) = - - ( 1 / ( 1 − 𝑦 ) ) )
264 258 negnegd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → - - ( 1 / ( 1 − 𝑦 ) ) = ( 1 / ( 1 − 𝑦 ) ) )
265 263 264 eqtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → - ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) = ( 1 / ( 1 − 𝑦 ) ) )
266 265 mpteq2ia ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( ( 1 / ( 1 − 𝑦 ) ) · - 1 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) )
267 257 266 eqtrdi ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) ) )
268 267 dmeqd ( ⊤ → dom ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ) = dom ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) ) )
269 dmmptg ( ∀ 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ( 1 / ( 1 − 𝑦 ) ) ∈ V → dom ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
270 ovexd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( 1 / ( 1 − 𝑦 ) ) ∈ V )
271 269 270 mprg dom ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 1 )
272 268 271 eqtrdi ( ⊤ → dom ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
273 sumex Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ∈ V
274 273 a1i ( ( ⊤ ∧ 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) → Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ∈ V )
275 fveq2 ( 𝑛 = 𝑘 → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) )
276 275 cbvsumv Σ 𝑛 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑛 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 )
277 181 276 eqtrdi ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) )
278 277 mpteq2ia ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) = ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑥𝑗 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) )
279 eqid ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑧 ) + if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑧 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑧 ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑧 ) + if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑧 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑧 ) + 1 ) ) ) / 2 ) )
280 97 278 105 119 183 184 279 pserdv2 ( ⊤ → ( ℂ D ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ) = ( 𝑦 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ) )
281 158 ssriv ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
282 281 a1i ( ⊤ → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) · ( 𝑟𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
283 192 188 274 280 282 233 231 237 dvmptres ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ) )
284 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
285 284 adantl ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
286 eqeq1 ( 𝑚 = 𝑛 → ( 𝑚 = 0 ↔ 𝑛 = 0 ) )
287 oveq2 ( 𝑚 = 𝑛 → ( 1 / 𝑚 ) = ( 1 / 𝑛 ) )
288 286 287 ifbieq2d ( 𝑚 = 𝑛 → if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
289 ovex ( 1 / 𝑛 ) ∈ V
290 90 289 ifex if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) ∈ V
291 288 89 290 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
292 285 291 syl ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
293 nnne0 ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
294 293 adantl ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
295 294 neneqd ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
296 295 iffalsed ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) = ( 1 / 𝑛 ) )
297 292 296 eqtrd ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) = ( 1 / 𝑛 ) )
298 297 oveq2d ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) = ( 𝑛 · ( 1 / 𝑛 ) ) )
299 nncn ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
300 299 adantl ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
301 300 294 recidd ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · ( 1 / 𝑛 ) ) = 1 )
302 298 301 eqtrd ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) = 1 )
303 302 oveq1d ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) = ( 1 · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) )
304 nnm1nn0 ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
305 expcl ( ( 𝑦 ∈ ℂ ∧ ( 𝑛 − 1 ) ∈ ℕ0 ) → ( 𝑦 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
306 51 304 305 syl2an ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
307 306 mulid2d ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( 1 · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑦 ↑ ( 𝑛 − 1 ) ) )
308 303 307 eqtrd ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑦 ↑ ( 𝑛 − 1 ) ) )
309 308 sumeq2dv ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) = Σ 𝑛 ∈ ℕ ( 𝑦 ↑ ( 𝑛 − 1 ) ) )
310 nnuz ℕ = ( ℤ ‘ 1 )
311 1e0p1 1 = ( 0 + 1 )
312 311 fveq2i ( ℤ ‘ 1 ) = ( ℤ ‘ ( 0 + 1 ) )
313 310 312 eqtri ℕ = ( ℤ ‘ ( 0 + 1 ) )
314 oveq1 ( 𝑛 = ( 1 + 𝑚 ) → ( 𝑛 − 1 ) = ( ( 1 + 𝑚 ) − 1 ) )
315 314 oveq2d ( 𝑛 = ( 1 + 𝑚 ) → ( 𝑦 ↑ ( 𝑛 − 1 ) ) = ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) )
316 1zzd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 1 ∈ ℤ )
317 0zd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 0 ∈ ℤ )
318 1 313 315 316 317 306 isumshft ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → Σ 𝑛 ∈ ℕ ( 𝑦 ↑ ( 𝑛 − 1 ) ) = Σ 𝑚 ∈ ℕ0 ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) )
319 pncan2 ( ( 1 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 1 + 𝑚 ) − 1 ) = 𝑚 )
320 48 99 319 sylancr ( 𝑚 ∈ ℕ0 → ( ( 1 + 𝑚 ) − 1 ) = 𝑚 )
321 320 oveq2d ( 𝑚 ∈ ℕ0 → ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) = ( 𝑦𝑚 ) )
322 321 sumeq2i Σ 𝑚 ∈ ℕ0 ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) = Σ 𝑚 ∈ ℕ0 ( 𝑦𝑚 )
323 318 322 eqtrdi ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → Σ 𝑛 ∈ ℕ ( 𝑦 ↑ ( 𝑛 − 1 ) ) = Σ 𝑚 ∈ ℕ0 ( 𝑦𝑚 ) )
324 geoisum ( ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) < 1 ) → Σ 𝑚 ∈ ℕ0 ( 𝑦𝑚 ) = ( 1 / ( 1 − 𝑦 ) ) )
325 51 64 324 syl2anc ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → Σ 𝑚 ∈ ℕ0 ( 𝑦𝑚 ) = ( 1 / ( 1 − 𝑦 ) ) )
326 309 323 325 3eqtrd ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) = ( 1 / ( 1 − 𝑦 ) ) )
327 326 mpteq2ia ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 0 , ( 1 / 𝑚 ) ) ) ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) )
328 283 327 eqtrdi ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ ( 1 / ( 1 − 𝑦 ) ) ) )
329 267 328 eqtr4d ( ⊤ → ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ) = ( ℂ D ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ) )
330 1rp 1 ∈ ℝ+
331 blcntr ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+ ) → 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
332 38 28 330 331 mp3an 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 )
333 332 a1i ( ⊤ → 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
334 oveq2 ( 𝑦 = 0 → ( 1 − 𝑦 ) = ( 1 − 0 ) )
335 1m0e1 ( 1 − 0 ) = 1
336 334 335 eqtrdi ( 𝑦 = 0 → ( 1 − 𝑦 ) = 1 )
337 336 fveq2d ( 𝑦 = 0 → ( log ‘ ( 1 − 𝑦 ) ) = ( log ‘ 1 ) )
338 log1 ( log ‘ 1 ) = 0
339 337 338 eqtrdi ( 𝑦 = 0 → ( log ‘ ( 1 − 𝑦 ) ) = 0 )
340 339 negeqd ( 𝑦 = 0 → - ( log ‘ ( 1 − 𝑦 ) ) = - 0 )
341 neg0 - 0 = 0
342 340 341 eqtrdi ( 𝑦 = 0 → - ( log ‘ ( 1 − 𝑦 ) ) = 0 )
343 eqid ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) )
344 342 343 90 fvmpt ( 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 0 ) = 0 )
345 332 344 mp1i ( ⊤ → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 0 ) = 0 )
346 oveq1 ( 0 = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) → ( 0 · ( 𝑦𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
347 346 eqeq1d ( 0 = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) → ( ( 0 · ( 𝑦𝑛 ) ) = 0 ↔ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = 0 ) )
348 oveq1 ( ( 1 / 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) → ( ( 1 / 𝑛 ) · ( 𝑦𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
349 348 eqeq1d ( ( 1 / 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) → ( ( ( 1 / 𝑛 ) · ( 𝑦𝑛 ) ) = 0 ↔ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = 0 ) )
350 simpll ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → 𝑦 = 0 )
351 350 28 eqeltrdi ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → 𝑦 ∈ ℂ )
352 simplr ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → 𝑛 ∈ ℕ0 )
353 351 352 expcld ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → ( 𝑦𝑛 ) ∈ ℂ )
354 353 mul02d ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → ( 0 · ( 𝑦𝑛 ) ) = 0 )
355 simpll ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑦 = 0 )
356 355 oveq1d ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑦𝑛 ) = ( 0 ↑ 𝑛 ) )
357 simpr ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
358 357 14 sylib ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) )
359 358 ord ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑛 ∈ ℕ → 𝑛 = 0 ) )
360 359 con1d ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑛 = 0 → 𝑛 ∈ ℕ ) )
361 360 imp ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
362 361 0expd ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 0 ↑ 𝑛 ) = 0 )
363 356 362 eqtrd ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑦𝑛 ) = 0 )
364 363 oveq2d ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( 1 / 𝑛 ) · ( 𝑦𝑛 ) ) = ( ( 1 / 𝑛 ) · 0 ) )
365 361 nnrecred ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 1 / 𝑛 ) ∈ ℝ )
366 365 recnd ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 1 / 𝑛 ) ∈ ℂ )
367 366 mul01d ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( 1 / 𝑛 ) · 0 ) = 0 )
368 364 367 eqtrd ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( 1 / 𝑛 ) · ( 𝑦𝑛 ) ) = 0 )
369 347 349 354 368 ifbothda ( ( 𝑦 = 0 ∧ 𝑛 ∈ ℕ0 ) → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = 0 )
370 369 sumeq2dv ( 𝑦 = 0 → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = Σ 𝑛 ∈ ℕ0 0 )
371 1 eqimssi 0 ⊆ ( ℤ ‘ 0 )
372 371 orci ( ℕ0 ⊆ ( ℤ ‘ 0 ) ∨ ℕ0 ∈ Fin )
373 sumz ( ( ℕ0 ⊆ ( ℤ ‘ 0 ) ∨ ℕ0 ∈ Fin ) → Σ 𝑛 ∈ ℕ0 0 = 0 )
374 372 373 ax-mp Σ 𝑛 ∈ ℕ0 0 = 0
375 370 374 eqtrdi ( 𝑦 = 0 → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = 0 )
376 eqid ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) )
377 375 376 90 fvmpt ( 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 0 ) = 0 )
378 332 377 mp1i ( ⊤ → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 0 ) = 0 )
379 345 378 eqtr4d ( ⊤ → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 0 ) = ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 0 ) )
380 45 46 47 78 190 272 329 333 379 dv11cn ( ⊤ → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) )
381 380 fveq1d ( ⊤ → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 𝐴 ) = ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 𝐴 ) )
382 44 381 mp1i ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 𝐴 ) = ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 𝐴 ) )
383 oveq2 ( 𝑦 = 𝐴 → ( 1 − 𝑦 ) = ( 1 − 𝐴 ) )
384 383 fveq2d ( 𝑦 = 𝐴 → ( log ‘ ( 1 − 𝑦 ) ) = ( log ‘ ( 1 − 𝐴 ) ) )
385 384 negeqd ( 𝑦 = 𝐴 → - ( log ‘ ( 1 − 𝑦 ) ) = - ( log ‘ ( 1 − 𝐴 ) ) )
386 negex - ( log ‘ ( 1 − 𝐴 ) ) ∈ V
387 385 343 386 fvmpt ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ - ( log ‘ ( 1 − 𝑦 ) ) ) ‘ 𝐴 ) = - ( log ‘ ( 1 − 𝐴 ) ) )
388 oveq1 ( 𝑦 = 𝐴 → ( 𝑦𝑛 ) = ( 𝐴𝑛 ) )
389 388 oveq2d ( 𝑦 = 𝐴 → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
390 389 sumeq2sdv ( 𝑦 = 𝐴 → Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
391 sumex Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) ∈ V
392 390 376 391 fvmpt ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → ( ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↦ Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝑦𝑛 ) ) ) ‘ 𝐴 ) = Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
393 382 387 392 3eqtr3d ( 𝐴 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → - ( log ‘ ( 1 − 𝐴 ) ) = Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
394 43 393 syl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → - ( log ‘ ( 1 − 𝐴 ) ) = Σ 𝑛 ∈ ℕ0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
395 26 394 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) )
396 seqex seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ∈ V
397 396 a1i ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ∈ V )
398 seqex seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ∈ V
399 398 a1i ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ∈ V )
400 1zzd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℤ )
401 elnnuz ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ ‘ 1 ) )
402 fvres ( 𝑛 ∈ ( ℤ ‘ 1 ) → ( ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) ‘ 𝑛 ) = ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ‘ 𝑛 ) )
403 401 402 sylbi ( 𝑛 ∈ ℕ → ( ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) ‘ 𝑛 ) = ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ‘ 𝑛 ) )
404 403 eqcomd ( 𝑛 ∈ ℕ → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) ‘ 𝑛 ) )
405 addid2 ( 𝑛 ∈ ℂ → ( 0 + 𝑛 ) = 𝑛 )
406 405 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℂ ) → ( 0 + 𝑛 ) = 𝑛 )
407 0cnd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ∈ ℂ )
408 1eluzge0 1 ∈ ( ℤ ‘ 0 )
409 408 a1i ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ( ℤ ‘ 0 ) )
410 0cnd ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → 0 ∈ ℂ )
411 nn0cn ( 𝑘 ∈ ℕ0𝑘 ∈ ℂ )
412 411 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
413 neqne ( ¬ 𝑘 = 0 → 𝑘 ≠ 0 )
414 reccl ( ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) → ( 1 / 𝑘 ) ∈ ℂ )
415 412 413 414 syl2an ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 = 0 ) → ( 1 / 𝑘 ) ∈ ℂ )
416 410 415 ifclda ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) ∈ ℂ )
417 expcl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
418 417 adantlr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
419 416 418 mulcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ∈ ℂ )
420 419 fmpttd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) : ℕ0 ⟶ ℂ )
421 1nn0 1 ∈ ℕ0
422 ffvelrn ( ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) : ℕ0 ⟶ ℂ ∧ 1 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 1 ) ∈ ℂ )
423 420 421 422 sylancl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 1 ) ∈ ℂ )
424 elfz1eq ( 𝑛 ∈ ( 0 ... 0 ) → 𝑛 = 0 )
425 1m1e0 ( 1 − 1 ) = 0
426 425 oveq2i ( 0 ... ( 1 − 1 ) ) = ( 0 ... 0 )
427 424 426 eleq2s ( 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) → 𝑛 = 0 )
428 427 fveq2d ( 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 0 ) )
429 0nn0 0 ∈ ℕ0
430 iftrue ( 𝑘 = 0 → if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) = 0 )
431 oveq2 ( 𝑘 = 0 → ( 𝐴𝑘 ) = ( 𝐴 ↑ 0 ) )
432 430 431 oveq12d ( 𝑘 = 0 → ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) = ( 0 · ( 𝐴 ↑ 0 ) ) )
433 ovex ( 0 · ( 𝐴 ↑ 0 ) ) ∈ V
434 432 8 433 fvmpt ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 0 ) = ( 0 · ( 𝐴 ↑ 0 ) ) )
435 429 434 ax-mp ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 0 ) = ( 0 · ( 𝐴 ↑ 0 ) )
436 expcl ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ↑ 0 ) ∈ ℂ )
437 27 429 436 sylancl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ↑ 0 ) ∈ ℂ )
438 437 mul02d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 0 · ( 𝐴 ↑ 0 ) ) = 0 )
439 435 438 syl5eq ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 0 ) = 0 )
440 428 439 sylan9eqr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = 0 )
441 406 407 409 423 440 seqid ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) )
442 293 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
443 442 neneqd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
444 443 iffalsed ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) = ( 1 / 𝑛 ) )
445 444 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) = ( ( 1 / 𝑛 ) · ( 𝐴𝑛 ) ) )
446 284 23 sylan2 ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴𝑛 ) ∈ ℂ )
447 299 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
448 446 447 442 divrec2d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴𝑛 ) / 𝑛 ) = ( ( 1 / 𝑛 ) · ( 𝐴𝑛 ) ) )
449 445 448 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) = ( ( 𝐴𝑛 ) / 𝑛 ) )
450 284 11 sylan2 ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) · ( 𝐴𝑛 ) ) )
451 id ( 𝑘 = 𝑛𝑘 = 𝑛 )
452 6 451 oveq12d ( 𝑘 = 𝑛 → ( ( 𝐴𝑘 ) / 𝑘 ) = ( ( 𝐴𝑛 ) / 𝑛 ) )
453 eqid ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) )
454 ovex ( ( 𝐴𝑛 ) / 𝑛 ) ∈ V
455 452 453 454 fvmpt ( 𝑛 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ‘ 𝑛 ) = ( ( 𝐴𝑛 ) / 𝑛 ) )
456 455 adantl ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ‘ 𝑛 ) = ( ( 𝐴𝑛 ) / 𝑛 ) )
457 449 450 456 3eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ‘ 𝑛 ) )
458 401 457 sylan2br ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ( ℤ ‘ 1 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ‘ 𝑛 ) )
459 400 458 seqfeq ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) )
460 441 459 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) )
461 460 fveq1d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ↾ ( ℤ ‘ 1 ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ‘ 𝑛 ) )
462 404 461 sylan9eqr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ‘ 𝑛 ) )
463 310 397 399 400 462 climeq ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , 0 , ( 1 / 𝑘 ) ) · ( 𝐴𝑘 ) ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) ) )
464 395 463 mpbid ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝐴𝑘 ) / 𝑘 ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) )