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 fvmptelcdm ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ◡ 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 mullidd ⊢ ( ( 𝑦 ∈ ( 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 addlid ⊢ ( 𝑛 ∈ ℂ → ( 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 ffvelcdm ⊢ ( ( ( 𝑘 ∈ ℕ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 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 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 − 𝐴 ) ) )