MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  logtayl Structured version   Visualization version   GIF version

Theorem logtayl 26015
Description: The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
Assertion
Ref Expression
logtayl ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Distinct variable group:   𝐴,𝑘

Proof of Theorem logtayl
Dummy variables 𝑗 𝑚 𝑛 𝑟 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 12805 . . . 4 0 = (ℤ‘0)
2 0zd 12511 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℤ)
3 eqeq1 2740 . . . . . . . 8 (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0))
4 oveq2 7365 . . . . . . . 8 (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛))
53, 4ifbieq2d 4512 . . . . . . 7 (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛)))
6 oveq2 7365 . . . . . . 7 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
75, 6oveq12d 7375 . . . . . 6 (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
8 eqid 2736 . . . . . 6 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
9 ovex 7390 . . . . . 6 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
107, 8, 9fvmpt 6948 . . . . 5 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
1110adantl 482 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
12 0cnd 11148 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 0 ∈ ℂ)
13 simpr 485 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
14 elnn0 12415 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↔ (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1513, 14sylib 217 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1615ord 862 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
1716con1d 145 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
1817imp 407 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
1918nnrecred 12204 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
2019recnd 11183 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
2112, 20ifclda 4521 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ)
22 expcl 13985 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2322adantlr 713 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2421, 23mulcld 11175 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ ℂ)
25 logtayllem 26014 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ dom ⇝ )
261, 2, 11, 24, 25isumclim2 15643 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
27 simpl 483 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
28 0cn 11147 . . . . . . . 8 0 ∈ ℂ
29 eqid 2736 . . . . . . . . 9 (abs ∘ − ) = (abs ∘ − )
3029cnmetdval 24134 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
3127, 28, 30sylancl 586 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
32 subid1 11421 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3332adantr 481 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 − 0) = 𝐴)
3433fveq2d 6846 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(𝐴 − 0)) = (abs‘𝐴))
3531, 34eqtrd 2776 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘𝐴))
36 simpr 485 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3735, 36eqbrtrd 5127 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) < 1)
38 cnxmet 24136 . . . . . . 7 (abs ∘ − ) ∈ (∞Met‘ℂ)
39 1xr 11214 . . . . . . 7 1 ∈ ℝ*
40 elbl3 23745 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4138, 39, 40mpanl12 700 . . . . . 6 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4228, 27, 41sylancr 587 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4337, 42mpbird 256 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ (0(ball‘(abs ∘ − ))1))
44 tru 1545 . . . . . 6
45 eqid 2736 . . . . . . . 8 (0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘ − ))1)
46 0cnd 11148 . . . . . . . 8 (⊤ → 0 ∈ ℂ)
4739a1i 11 . . . . . . . 8 (⊤ → 1 ∈ ℝ*)
48 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
49 blssm 23771 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
5038, 28, 39, 49mp3an 1461 . . . . . . . . . . . . . 14 (0(ball‘(abs ∘ − ))1) ⊆ ℂ
5150sseli 3940 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ ℂ)
52 subcl 11400 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
5348, 51, 52sylancr 587 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ ℂ)
5451abscld 15321 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ)
5529cnmetdval 24134 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5651, 28, 55sylancl 586 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5751subid1d 11501 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 − 0) = 𝑦)
5857fveq2d 6846 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦))
5956, 58eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦))
60 elbl3 23745 . . . . . . . . . . . . . . . . . . 19 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6138, 39, 60mpanl12 700 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6228, 51, 61sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6362ibi 266 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) < 1)
6459, 63eqbrtrrd 5129 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < 1)
6554, 64gtned 11290 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ (abs‘𝑦))
66 abs1 15182 . . . . . . . . . . . . . . . 16 (abs‘1) = 1
67 fveq2 6842 . . . . . . . . . . . . . . . 16 (1 = 𝑦 → (abs‘1) = (abs‘𝑦))
6866, 67eqtr3id 2790 . . . . . . . . . . . . . . 15 (1 = 𝑦 → 1 = (abs‘𝑦))
6968necon3i 2976 . . . . . . . . . . . . . 14 (1 ≠ (abs‘𝑦) → 1 ≠ 𝑦)
7065, 69syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ 𝑦)
71 subeq0 11427 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦))
7271necon3bid 2988 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7348, 51, 72sylancr 587 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7470, 73mpbird 256 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ≠ 0)
7553, 74logcld 25926 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ)
7675negcld 11499 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ)
7776adantl 482 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 − 𝑦)) ∈ ℂ)
7877fmpttd 7063 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
7951absge0d 15329 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (abs‘𝑦))
8054rexrd 11205 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ*)
81 peano2re 11328 . . . . . . . . . . . . . . . 16 ((abs‘𝑦) ∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ)
8254, 81syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ)
8382rehalfcld 12400 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ)
8483rexrd 11205 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ*)
85 iccssxr 13347 . . . . . . . . . . . . . . 15 (0[,]+∞) ⊆ ℝ*
86 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0))
87 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
8886, 87ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗)))
89 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))
90 c0ex 11149 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
91 ovex 7390 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 𝑗) ∈ V
9290, 91ifex 4536 . . . . . . . . . . . . . . . . . . . . 21 if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V
9388, 89, 92fvmpt 6948 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗)))
9493eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → if(𝑗 = 0, 0, (1 / 𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗))
9594oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9695mpteq2ia 5208 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9796mpteq2i 5210 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗))))
98 0cnd 11148 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈ ℂ)
99 nn0cn 12423 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
10099adantl 482 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
101 neqne 2951 . . . . . . . . . . . . . . . . . . 19 𝑚 = 0 → 𝑚 ≠ 0)
102 reccl 11820 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈ ℂ)
103100, 101, 102syl2an 596 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ)
10498, 103ifclda 4521 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑚 ∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ)
105104fmpttd 7063 . . . . . . . . . . . . . . . 16 (⊤ → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
106 recn 11141 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ → 𝑟 ∈ ℂ)
107 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑟 → (𝑥𝑗) = (𝑟𝑗))
108107oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))
109108mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
110 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))
111 nn0ex 12419 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
112111mptex 7173 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) ∈ V
113109, 110, 112fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
114106, 113syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
115114eqcomd 2742 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟))
116115seqeq3d 13914 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)))
117116eleq1d 2822 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ → (seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ ↔ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ ))
118117rabbiia 3411 . . . . . . . . . . . . . . . . 17 {𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }
119118supeq1i 9383 . . . . . . . . . . . . . . . 16 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
12097, 105, 119radcnvcl 25776 . . . . . . . . . . . . . . 15 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
12185, 120sselid 3942 . . . . . . . . . . . . . 14 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
12244, 121mp1i 13 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
123 1re 11155 . . . . . . . . . . . . . . 15 1 ∈ ℝ
124 avglt1 12391 . . . . . . . . . . . . . . 15 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12554, 123, 124sylancl 586 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12664, 125mpbid 231 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))
127 0red 11158 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℝ)
128127, 54, 83, 79, 126lelttrd 11313 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2))
129127, 83, 128ltled 11303 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2))
13083, 129absidd 15307 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) = (((abs‘𝑦) + 1) / 2))
13144, 105mp1i 13 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
13283recnd 11183 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ)
133 oveq1 7364 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗))
134133oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))
135134mpteq2dv 5207 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
136111mptex 7173 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) ∈ V
137135, 110, 136fvmpt 6948 . . . . . . . . . . . . . . . . . 18 ((((abs‘𝑦) + 1) / 2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
138132, 137syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
139138seqeq3d 13914 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) = seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))))
140 avglt2 12392 . . . . . . . . . . . . . . . . . . . 20 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14154, 123, 140sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14264, 141mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1)
143130, 142eqbrtrd 5127 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1)
144 logtayllem 26014 . . . . . . . . . . . . . . . . 17 (((((abs‘𝑦) + 1) / 2) ∈ ℂ ∧ (abs‘(((abs‘𝑦) + 1) / 2)) < 1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
145132, 143, 144syl2anc 584 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
146139, 145eqeltrd 2838 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝ )
14797, 131, 119, 132, 146radcnvle 25779 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
148130, 147eqbrtrrd 5129 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
14980, 84, 122, 126, 148xrltletrd 13080 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
150 0re 11157 . . . . . . . . . . . . 13 0 ∈ ℝ
151 elico2 13328 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*) → ((abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
152150, 122, 151sylancr 587 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
15354, 79, 149, 152mpbir3and 1342 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
154 absf 15222 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
155 ffn 6668 . . . . . . . . . . . 12 (abs:ℂ⟶ℝ → abs Fn ℂ)
156 elpreima 7008 . . . . . . . . . . . 12 (abs Fn ℂ → (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))))
157154, 155, 156mp2b 10 . . . . . . . . . . 11 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
15851, 153, 157sylanbrc 583 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
159 cnvimass 6033 . . . . . . . . . . . . . . . . 17 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
160154fdmi 6680 . . . . . . . . . . . . . . . . 17 dom abs = ℂ
161159, 160sseqtri 3980 . . . . . . . . . . . . . . . 16 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
162161sseli 3940 . . . . . . . . . . . . . . 15 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → 𝑦 ∈ ℂ)
163 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑥𝑗) = (𝑦𝑗))
164163oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
165164mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
166111mptex 7173 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) ∈ V
167165, 110, 166fvmpt 6948 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
168167adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
169168fveq1d 6844 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛))
170 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0))
171 oveq2 7365 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛))
172170, 171ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛)))
173 oveq2 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (𝑦𝑗) = (𝑦𝑛))
174172, 173oveq12d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
175 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
176 ovex 7390 . . . . . . . . . . . . . . . . . . 19 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ V
177174, 175, 176fvmpt 6948 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
178177adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
179169, 178eqtr2d 2777 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
180179sumeq2dv 15588 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
181162, 180syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
182181mpteq2ia 5208 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
183 eqid 2736 . . . . . . . . . . . . 13 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
184 eqid 2736 . . . . . . . . . . . . 13 if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑧) + 1)) = if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑧) + 1))
18597, 182, 105, 119, 183, 184psercn 25785 . . . . . . . . . . . 12 (⊤ → (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) ∈ ((abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))–cn→ℂ))
186 cncff 24256 . . . . . . . . . . . 12 ((𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) ∈ ((abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))–cn→ℂ) → (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))⟶ℂ)
187185, 186syl 17 . . . . . . . . . . 11 (⊤ → (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))⟶ℂ)
188187fvmptelcdm 7061 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
189158, 188sylan2 593 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
190189fmpttd 7063 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
191 cnelprrecn 11144 . . . . . . . . . . . . 13 ℂ ∈ {ℝ, ℂ}
192191a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
19375adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 − 𝑦)) ∈ ℂ)
194 ovexd 7392 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈ V)
19529cnmetdval 24134 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 − 𝑦) ∈ ℂ) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
19648, 53, 195sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
197 nncan 11430 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦)
19848, 51, 197sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦)
199198fveq2d 6846 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦))
200196, 199eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦))
201200, 64eqbrtrd 5127 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1)
202 elbl 23741 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1)))
20338, 48, 39, 202mp3an 1461 . . . . . . . . . . . . . . 15 ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1))
20453, 201, 203sylanbrc 583 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
205204adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
206 neg1cn 12267 . . . . . . . . . . . . . 14 -1 ∈ ℂ
207206a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈ ℂ)
208 eqid 2736 . . . . . . . . . . . . . . . . . 18 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
209208dvlog2lem 26007 . . . . . . . . . . . . . . . . 17 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
210209sseli 3940 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ (ℂ ∖ (-∞(,]0)))
211210eldifad 3922 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ ℂ)
212 eqid 2736 . . . . . . . . . . . . . . . . 17 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
213212logdmn0 25995 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ≠ 0)
214210, 213syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ≠ 0)
215211, 214logcld 25926 . . . . . . . . . . . . . 14 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑥) ∈ ℂ)
216215adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈ ℂ)
217 ovexd 7392 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V)
218 simpr 485 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
21948, 218, 52sylancr 587 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
220206a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → -1 ∈ ℂ)
221 1cnd 11150 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
222 0cnd 11148 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
223 1cnd 11150 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℂ)
224192, 223dvmptc 25322 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 1)) = (𝑦 ∈ ℂ ↦ 0))
225192dvmptid 25321 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
226192, 221, 222, 224, 218, 221, 225dvmptsub 25331 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 − 1)))
227 df-neg 11388 . . . . . . . . . . . . . . . 16 -1 = (0 − 1)
228227mpteq2i 5210 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ -1) = (𝑦 ∈ ℂ ↦ (0 − 1))
229226, 228eqtr4di 2794 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1))
23050a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
231 eqid 2736 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
232231cnfldtopon 24146 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
233232toponrestid 22270 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
234231cnfldtopn 24145 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
235234blopn 23856 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
23638, 28, 39, 235mp3an 1461 . . . . . . . . . . . . . . 15 (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld)
237236a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
238192, 219, 220, 229, 230, 233, 231, 237dvmptres 25327 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -1))
239 logf1o 25920 . . . . . . . . . . . . . . . . . . . 20 log:(ℂ ∖ {0})–1-1-onto→ran log
240 f1of 6784 . . . . . . . . . . . . . . . . . . . 20 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
241239, 240ax-mp 5 . . . . . . . . . . . . . . . . . . 19 log:(ℂ ∖ {0})⟶ran log
242212logdmss 25997 . . . . . . . . . . . . . . . . . . . 20 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
243209, 242sstri 3953 . . . . . . . . . . . . . . . . . . 19 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
244 fssres 6708 . . . . . . . . . . . . . . . . . . 19 ((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
245241, 243, 244mp2an 690 . . . . . . . . . . . . . . . . . 18 (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log
246245a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
247246feqmptd 6910 . . . . . . . . . . . . . . . 16 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)))
248 fvres 6861 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥) = (log‘𝑥))
249248mpteq2ia 5208 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))
250247, 249eqtrdi 2792 . . . . . . . . . . . . . . 15 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))
251250oveq2d 7373 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))))
252208dvlog2 26008 . . . . . . . . . . . . . 14 (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥))
253251, 252eqtr3di 2791 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥)))
254 fveq2 6842 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦)))
255 oveq2 7365 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦)))
256192, 192, 205, 207, 216, 217, 238, 253, 254, 255dvmptco 25336 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ ((1 / (1 − 𝑦)) · -1)))
257192, 193, 194, 256dvmptneg 25330 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)))
25853, 74reccld 11924 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ)
259 mulcom 11137 . . . . . . . . . . . . . . . 16 (((1 / (1 − 𝑦)) ∈ ℂ ∧ -1 ∈ ℂ) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
260258, 206, 259sylancl 586 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
261258mulm1d 11607 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦)))
262260, 261eqtrd 2776 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦)))
263262negeqd 11395 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦)))
264258negnegd 11503 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦)))
265263, 264eqtrd 2776 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦)))
266265mpteq2ia 5208 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
267257, 266eqtrdi 2792 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
268267dmeqd 5861 . . . . . . . . 9 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
269 dmmptg 6194 . . . . . . . . . 10 (∀𝑦 ∈ (0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1))
270 ovexd 7392 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ V)
271269, 270mprg 3070 . . . . . . . . 9 dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1)
272268, 271eqtrdi 2792 . . . . . . . 8 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (0(ball‘(abs ∘ − ))1))
273 sumex 15572 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V
274273a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V)
275 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
276275cbvsumv 15581 . . . . . . . . . . . . . 14 Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘)
277181, 276eqtrdi 2792 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
278277mpteq2ia 5208 . . . . . . . . . . . 12 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
279 eqid 2736 . . . . . . . . . . . 12 (0(ball‘(abs ∘ − ))(((abs‘𝑧) + if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑧) + 1))) / 2)) = (0(ball‘(abs ∘ − ))(((abs‘𝑧) + if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑧) + 1))) / 2))
28097, 278, 105, 119, 183, 184, 279pserdv2 25789 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
281158ssriv 3948 . . . . . . . . . . . 12 (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
282281a1i 11 . . . . . . . . . . 11 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
283192, 188, 274, 280, 282, 233, 231, 237dvmptres 25327 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
284 nnnn0 12420 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
285284adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
286 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0))
287 oveq2 7365 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
288286, 287ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛)))
289 ovex 7390 . . . . . . . . . . . . . . . . . . . . 21 (1 / 𝑛) ∈ V
29090, 289ifex 4536 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V
291288, 89, 290fvmpt 6948 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
292285, 291syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
293 nnne0 12187 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
294293adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
295294neneqd 2948 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
296295iffalsed 4497 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
297292, 296eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛))
298297oveq2d 7373 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛)))
299 nncn 12161 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
300299adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
301300, 294recidd 11926 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1)
302298, 301eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1)
303302oveq1d 7372 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1))))
304 nnm1nn0 12454 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
305 expcl 13985 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
30651, 304, 305syl2an 596 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
307306mulid2d 11173 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
308303, 307eqtrd 2776 . . . . . . . . . . . . 13 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
309308sumeq2dv 15588 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)))
310 nnuz 12806 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
311 1e0p1 12660 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
312311fveq2i 6845 . . . . . . . . . . . . . . 15 (ℤ‘1) = (ℤ‘(0 + 1))
313310, 312eqtri 2764 . . . . . . . . . . . . . 14 ℕ = (ℤ‘(0 + 1))
314 oveq1 7364 . . . . . . . . . . . . . . 15 (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1))
315314oveq2d 7373 . . . . . . . . . . . . . 14 (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1)))
316 1zzd 12534 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ∈ ℤ)
317 0zd 12511 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℤ)
3181, 313, 315, 316, 317, 306isumshft 15724 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)))
319 pncan2 11408 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚)
32048, 99, 319sylancr 587 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((1 + 𝑚) − 1) = 𝑚)
321320oveq2d 7373 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑦↑((1 + 𝑚) − 1)) = (𝑦𝑚))
322321sumeq2i 15584 . . . . . . . . . . . . 13 Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚)
323318, 322eqtrdi 2792 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚))
324 geoisum 15762 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ (abs‘𝑦) < 1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
32551, 64, 324syl2anc 584 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
326309, 323, 3253eqtrd 2780 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦)))
327326mpteq2ia 5208 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
328283, 327eqtrdi 2792 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
329267, 328eqtr4d 2779 . . . . . . . 8 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))))
330 1rp 12919 . . . . . . . . . 10 1 ∈ ℝ+
331 blcntr 23766 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘ − ))1))
33238, 28, 330, 331mp3an 1461 . . . . . . . . 9 0 ∈ (0(ball‘(abs ∘ − ))1)
333332a1i 11 . . . . . . . 8 (⊤ → 0 ∈ (0(ball‘(abs ∘ − ))1))
334 oveq2 7365 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (1 − 𝑦) = (1 − 0))
335 1m0e1 12274 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
336334, 335eqtrdi 2792 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (1 − 𝑦) = 1)
337336fveq2d 6846 . . . . . . . . . . . . . 14 (𝑦 = 0 → (log‘(1 − 𝑦)) = (log‘1))
338 log1 25941 . . . . . . . . . . . . . 14 (log‘1) = 0
339337, 338eqtrdi 2792 . . . . . . . . . . . . 13 (𝑦 = 0 → (log‘(1 − 𝑦)) = 0)
340339negeqd 11395 . . . . . . . . . . . 12 (𝑦 = 0 → -(log‘(1 − 𝑦)) = -0)
341 neg0 11447 . . . . . . . . . . . 12 -0 = 0
342340, 341eqtrdi 2792 . . . . . . . . . . 11 (𝑦 = 0 → -(log‘(1 − 𝑦)) = 0)
343 eqid 2736 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))
344342, 343, 90fvmpt 6948 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
345332, 344mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
346 oveq1 7364 . . . . . . . . . . . . . . 15 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
347346eqeq1d 2738 . . . . . . . . . . . . . 14 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
348 oveq1 7364 . . . . . . . . . . . . . . 15 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
349348eqeq1d 2738 . . . . . . . . . . . . . 14 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
350 simpll 765 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0)
351350, 28eqeltrdi 2846 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ)
352 simplr 767 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0)
353351, 352expcld 14051 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦𝑛) ∈ ℂ)
354353mul02d 11353 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦𝑛)) = 0)
355 simpll 765 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑦 = 0)
356355oveq1d 7372 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = (0↑𝑛))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
358357, 14sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
359358ord 862 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
360359con1d 145 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
361360imp 407 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
3623610expd 14044 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (0↑𝑛) = 0)
363356, 362eqtrd 2776 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = 0)
364363oveq2d 7373 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = ((1 / 𝑛) · 0))
365361nnrecred 12204 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
366365recnd 11183 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
367366mul01d 11354 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · 0) = 0)
368364, 367eqtrd 2776 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = 0)
369347, 349, 354, 368ifbothda 4524 . . . . . . . . . . . . 13 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
370369sumeq2dv 15588 . . . . . . . . . . . 12 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 0)
3711eqimssi 4002 . . . . . . . . . . . . . 14 0 ⊆ (ℤ‘0)
372371orci 863 . . . . . . . . . . . . 13 (ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin)
373 sumz 15607 . . . . . . . . . . . . 13 ((ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 = 0)
374372, 373ax-mp 5 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ0 0 = 0
375370, 374eqtrdi 2792 . . . . . . . . . . 11 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
376 eqid 2736 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
377375, 376, 90fvmpt 6948 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
378332, 377mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
379345, 378eqtr4d 2779 . . . . . . . 8 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0))
38045, 46, 47, 78, 190, 272, 329, 333, 379dv11cn 25365 . . . . . . 7 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))))
381380fveq1d 6844 . . . . . 6 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
38244, 381mp1i 13 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
383 oveq2 7365 . . . . . . . 8 (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴))
384383fveq2d 6846 . . . . . . 7 (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴)))
385384negeqd 11395 . . . . . 6 (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 − 𝐴)))
386 negex 11399 . . . . . 6 -(log‘(1 − 𝐴)) ∈ V
387385, 343, 386fvmpt 6948 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴)))
388 oveq1 7364 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑛) = (𝐴𝑛))
389388oveq2d 7373 . . . . . . 7 (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
390389sumeq2sdv 15589 . . . . . 6 (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
391 sumex 15572 . . . . . 6 Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
392390, 376, 391fvmpt 6948 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
393382, 387, 3923eqtr3d 2784 . . . 4 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
39443, 393syl 17 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
39526, 394breqtrrd 5133 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)))
396 seqex 13908 . . . 4 seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V
397396a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V)
398 seqex 13908 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V
399398a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V)
400 1zzd 12534 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℤ)
401 elnnuz 12807 . . . . . 6 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
402 fvres 6861 . . . . . 6 (𝑛 ∈ (ℤ‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
403401, 402sylbi 216 . . . . 5 (𝑛 ∈ ℕ → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
404403eqcomd 2742 . . . 4 (𝑛 ∈ ℕ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛))
405 addid2 11338 . . . . . . . 8 (𝑛 ∈ ℂ → (0 + 𝑛) = 𝑛)
406405adantl 482 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℂ) → (0 + 𝑛) = 𝑛)
407 0cnd 11148 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℂ)
408 1eluzge0 12817 . . . . . . . 8 1 ∈ (ℤ‘0)
409408a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ (ℤ‘0))
410 0cnd 11148 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
411 nn0cn 12423 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
412411adantl 482 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
413 neqne 2951 . . . . . . . . . . . 12 𝑘 = 0 → 𝑘 ≠ 0)
414 reccl 11820 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
415412, 413, 414syl2an 596 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
416410, 415ifclda 4521 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
417 expcl 13985 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
418417adantlr 713 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
419416, 418mulcld 11175 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
420419fmpttd 7063 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ)
421 1nn0 12429 . . . . . . . 8 1 ∈ ℕ0
422 ffvelcdm 7032 . . . . . . . 8 (((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
423420, 421, 422sylancl 586 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
424 elfz1eq 13452 . . . . . . . . . 10 (𝑛 ∈ (0...0) → 𝑛 = 0)
425 1m1e0 12225 . . . . . . . . . . 11 (1 − 1) = 0
426425oveq2i 7368 . . . . . . . . . 10 (0...(1 − 1)) = (0...0)
427424, 426eleq2s 2856 . . . . . . . . 9 (𝑛 ∈ (0...(1 − 1)) → 𝑛 = 0)
428427fveq2d 6846 . . . . . . . 8 (𝑛 ∈ (0...(1 − 1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0))
429 0nn0 12428 . . . . . . . . . 10 0 ∈ ℕ0
430 iftrue 4492 . . . . . . . . . . . 12 (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0)
431 oveq2 7365 . . . . . . . . . . . 12 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
432430, 431oveq12d 7375 . . . . . . . . . . 11 (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (0 · (𝐴↑0)))
433 ovex 7390 . . . . . . . . . . 11 (0 · (𝐴↑0)) ∈ V
434432, 8, 433fvmpt 6948 . . . . . . . . . 10 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0)))
435429, 434ax-mp 5 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0))
436 expcl 13985 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝐴↑0) ∈ ℂ)
43727, 429, 436sylancl 586 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴↑0) ∈ ℂ)
438437mul02d 11353 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (0 · (𝐴↑0)) = 0)
439435, 438eqtrid 2788 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = 0)
440428, 439sylan9eqr 2798 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (0...(1 − 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = 0)
441406, 407, 409, 423, 440seqid 13953 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))))
442293adantl 482 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
443442neneqd 2948 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
444443iffalsed 4497 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
445444oveq1d 7372 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((1 / 𝑛) · (𝐴𝑛)))
446284, 23sylan2 593 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ ℂ)
447299adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
448446, 447, 442divrec2d 11935 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴𝑛)))
449445, 448eqtr4d 2779 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((𝐴𝑛) / 𝑛))
450284, 11sylan2 593 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
451 id 22 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑘 = 𝑛)
4526, 451oveq12d 7375 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) / 𝑘) = ((𝐴𝑛) / 𝑛))
453 eqid 2736 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))
454 ovex 7390 . . . . . . . . . . 11 ((𝐴𝑛) / 𝑛) ∈ V
455452, 453, 454fvmpt 6948 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
456455adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
457449, 450, 4563eqtr4d 2786 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
458401, 457sylan2br 595 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
459400, 458seqfeq 13933 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
460441, 459eqtrd 2776 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
461460fveq1d 6844 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
462404, 461sylan9eqr 2798 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
463310, 397, 399, 400, 462climeq 15449 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))))
464395, 463mpbid 231 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wtru 1542  wcel 2106  wne 2943  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  ifcif 4486  {csn 4586  {cpr 4588   class class class wbr 5105  cmpt 5188  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637   Fn wfn 6491  wf 6492  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  Fincfn 8883  supcsup 9376  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  -∞cmnf 11187  *cxr 11188   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cuz 12763  +crp 12915  (,]cioc 13265  [,)cico 13266  [,]cicc 13267  ...cfz 13424  seqcseq 13906  cexp 13967  abscabs 15119  cli 15366  Σcsu 15570  TopOpenctopn 17303  ∞Metcxmet 20781  ballcbl 20783  fldccnfld 20796  cnccncf 24239   D cdv 25227  logclog 25910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-tan 15954  df-pi 15955  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-ulm 25736  df-log 25912
This theorem is referenced by:  logtaylsum  26016  logtayl2  26017  atantayl  26287  stirlinglem5  44309
  Copyright terms: Public domain W3C validator