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

Theorem logtayl 25170
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 12268 . . . 4 0 = (ℤ‘0)
2 0zd 11981 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℤ)
3 eqeq1 2822 . . . . . . . 8 (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0))
4 oveq2 7153 . . . . . . . 8 (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛))
53, 4ifbieq2d 4488 . . . . . . 7 (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛)))
6 oveq2 7153 . . . . . . 7 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
75, 6oveq12d 7163 . . . . . 6 (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
8 eqid 2818 . . . . . 6 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
9 ovex 7178 . . . . . 6 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
107, 8, 9fvmpt 6761 . . . . 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 10622 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 0 ∈ ℂ)
13 simpr 485 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
14 elnn0 11887 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↔ (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1513, 14sylib 219 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1615ord 858 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
1716con1d 147 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
1817imp 407 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
1918nnrecred 11676 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
2019recnd 10657 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
2112, 20ifclda 4497 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ)
22 expcl 13435 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2322adantlr 711 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2421, 23mulcld 10649 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ ℂ)
25 logtayllem 25169 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ dom ⇝ )
261, 2, 11, 24, 25isumclim2 15101 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
27 simpl 483 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
28 0cn 10621 . . . . . . . 8 0 ∈ ℂ
29 eqid 2818 . . . . . . . . 9 (abs ∘ − ) = (abs ∘ − )
3029cnmetdval 23306 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
3127, 28, 30sylancl 586 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
32 subid1 10894 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3332adantr 481 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 − 0) = 𝐴)
3433fveq2d 6667 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(𝐴 − 0)) = (abs‘𝐴))
3531, 34eqtrd 2853 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘𝐴))
36 simpr 485 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3735, 36eqbrtrd 5079 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) < 1)
38 cnxmet 23308 . . . . . . 7 (abs ∘ − ) ∈ (∞Met‘ℂ)
39 1xr 10688 . . . . . . 7 1 ∈ ℝ*
40 elbl3 22929 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4138, 39, 40mpanl12 698 . . . . . 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 258 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ (0(ball‘(abs ∘ − ))1))
44 tru 1532 . . . . . 6
45 eqid 2818 . . . . . . . 8 (0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘ − ))1)
46 0cnd 10622 . . . . . . . 8 (⊤ → 0 ∈ ℂ)
4739a1i 11 . . . . . . . 8 (⊤ → 1 ∈ ℝ*)
48 ax-1cn 10583 . . . . . . . . . . . . 13 1 ∈ ℂ
49 blssm 22955 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
5038, 28, 39, 49mp3an 1452 . . . . . . . . . . . . . 14 (0(ball‘(abs ∘ − ))1) ⊆ ℂ
5150sseli 3960 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ ℂ)
52 subcl 10873 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
5348, 51, 52sylancr 587 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ ℂ)
5451abscld 14784 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ)
5529cnmetdval 23306 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5651, 28, 55sylancl 586 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5751subid1d 10974 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 − 0) = 𝑦)
5857fveq2d 6667 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦))
5956, 58eqtrd 2853 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦))
60 elbl3 22929 . . . . . . . . . . . . . . . . . . 19 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6138, 39, 60mpanl12 698 . . . . . . . . . . . . . . . . . 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 268 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) < 1)
6459, 63eqbrtrrd 5081 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < 1)
6554, 64gtned 10763 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ (abs‘𝑦))
66 abs1 14645 . . . . . . . . . . . . . . . 16 (abs‘1) = 1
67 fveq2 6663 . . . . . . . . . . . . . . . 16 (1 = 𝑦 → (abs‘1) = (abs‘𝑦))
6866, 67syl5eqr 2867 . . . . . . . . . . . . . . 15 (1 = 𝑦 → 1 = (abs‘𝑦))
6968necon3i 3045 . . . . . . . . . . . . . 14 (1 ≠ (abs‘𝑦) → 1 ≠ 𝑦)
7065, 69syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ 𝑦)
71 subeq0 10900 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦))
7271necon3bid 3057 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7348, 51, 72sylancr 587 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7470, 73mpbird 258 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ≠ 0)
7553, 74logcld 25081 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ)
7675negcld 10972 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ)
7776adantl 482 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 − 𝑦)) ∈ ℂ)
7877fmpttd 6871 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
7951absge0d 14792 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (abs‘𝑦))
8054rexrd 10679 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ*)
81 peano2re 10801 . . . . . . . . . . . . . . . 16 ((abs‘𝑦) ∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ)
8254, 81syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ)
8382rehalfcld 11872 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ)
8483rexrd 10679 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ*)
85 iccssxr 12807 . . . . . . . . . . . . . . 15 (0[,]+∞) ⊆ ℝ*
86 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0))
87 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
8886, 87ifbieq2d 4488 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗)))
89 eqid 2818 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))
90 c0ex 10623 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
91 ovex 7178 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 𝑗) ∈ V
9290, 91ifex 4511 . . . . . . . . . . . . . . . . . . . . 21 if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V
9388, 89, 92fvmpt 6761 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗)))
9493eqcomd 2824 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → if(𝑗 = 0, 0, (1 / 𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗))
9594oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9695mpteq2ia 5148 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9796mpteq2i 5149 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗))))
98 0cnd 10622 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈ ℂ)
99 nn0cn 11895 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
10099adantl 482 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
101 neqne 3021 . . . . . . . . . . . . . . . . . . 19 𝑚 = 0 → 𝑚 ≠ 0)
102 reccl 11293 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈ ℂ)
103100, 101, 102syl2an 595 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ)
10498, 103ifclda 4497 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑚 ∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ)
105104fmpttd 6871 . . . . . . . . . . . . . . . 16 (⊤ → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
106 recn 10615 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ → 𝑟 ∈ ℂ)
107 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑟 → (𝑥𝑗) = (𝑟𝑗))
108107oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))
109108mpteq2dv 5153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
110 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))
111 nn0ex 11891 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
112111mptex 6977 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) ∈ V
113109, 110, 112fvmpt 6761 . . . . . . . . . . . . . . . . . . . . . 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 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟))
116115seqeq3d 13365 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)))
117116eleq1d 2894 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ → (seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ ↔ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ ))
118117rabbiia 3470 . . . . . . . . . . . . . . . . 17 {𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }
119118supeq1i 8899 . . . . . . . . . . . . . . . 16 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
12097, 105, 119radcnvcl 24932 . . . . . . . . . . . . . . 15 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
12185, 120sseldi 3962 . . . . . . . . . . . . . 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 10629 . . . . . . . . . . . . . . 15 1 ∈ ℝ
124 avglt1 11863 . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))
127 0red 10632 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℝ)
128127, 54, 83, 79, 126lelttrd 10786 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2))
129127, 83, 128ltled 10776 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2))
13083, 129absidd 14770 . . . . . . . . . . . . . 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 10657 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ)
133 oveq1 7152 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗))
134133oveq2d 7161 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))
135134mpteq2dv 5153 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
136111mptex 6977 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) ∈ V
137135, 110, 136fvmpt 6761 . . . . . . . . . . . . . . . . . 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 13365 . . . . . . . . . . . . . . . 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 11864 . . . . . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1)
143130, 142eqbrtrd 5079 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1)
144 logtayllem 25169 . . . . . . . . . . . . . . . . 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 2910 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝ )
14797, 131, 119, 132, 146radcnvle 24935 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
148130, 147eqbrtrrd 5081 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
14980, 84, 122, 126, 148xrltletrd 12542 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
150 0re 10631 . . . . . . . . . . . . 13 0 ∈ ℝ
151 elico2 12788 . . . . . . . . . . . . 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 1334 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
154 absf 14685 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
155 ffn 6507 . . . . . . . . . . . 12 (abs:ℂ⟶ℝ → abs Fn ℂ)
156 elpreima 6820 . . . . . . . . . . . 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 5942 . . . . . . . . . . . . . . . . 17 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
160154fdmi 6517 . . . . . . . . . . . . . . . . 17 dom abs = ℂ
161159, 160sseqtri 4000 . . . . . . . . . . . . . . . 16 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
162161sseli 3960 . . . . . . . . . . . . . . 15 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → 𝑦 ∈ ℂ)
163 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑥𝑗) = (𝑦𝑗))
164163oveq2d 7161 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
165164mpteq2dv 5153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
166111mptex 6977 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) ∈ V
167165, 110, 166fvmpt 6761 . . . . . . . . . . . . . . . . . . 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 6665 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛))
170 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0))
171 oveq2 7153 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛))
172170, 171ifbieq2d 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛)))
173 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (𝑦𝑗) = (𝑦𝑛))
174172, 173oveq12d 7163 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
175 eqid 2818 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
176 ovex 7178 . . . . . . . . . . . . . . . . . . 19 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ V
177174, 175, 176fvmpt 6761 . . . . . . . . . . . . . . . . . 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 2854 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
180179sumeq2dv 15048 . . . . . . . . . . . . . . 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 5148 . . . . . . . . . . . . 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 2818 . . . . . . . . . . . . 13 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
184 eqid 2818 . . . . . . . . . . . . 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 24941 . . . . . . . . . . . 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 23428 . . . . . . . . . . . 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 ⇝ }, ℝ*, < )))⟶ℂ)
188187fvmptelrn 6869 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
189158, 188sylan2 592 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
190189fmpttd 6871 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
191 cnelprrecn 10618 . . . . . . . . . . . . 13 ℂ ∈ {ℝ, ℂ}
192191a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
19375adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 − 𝑦)) ∈ ℂ)
194 ovexd 7180 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈ V)
19529cnmetdval 23306 . . . . . . . . . . . . . . . . . 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 10903 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦)
19848, 51, 197sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦)
199198fveq2d 6667 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦))
200196, 199eqtrd 2853 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦))
201200, 64eqbrtrd 5079 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1)
202 elbl 22925 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1)))
20338, 48, 39, 202mp3an 1452 . . . . . . . . . . . . . . 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 11739 . . . . . . . . . . . . . 14 -1 ∈ ℂ
207206a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈ ℂ)
208 eqid 2818 . . . . . . . . . . . . . . . . . 18 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
209208dvlog2lem 25162 . . . . . . . . . . . . . . . . 17 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
210209sseli 3960 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ (ℂ ∖ (-∞(,]0)))
211210eldifad 3945 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ ℂ)
212 eqid 2818 . . . . . . . . . . . . . . . . 17 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
213212logdmn0 25150 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ≠ 0)
214210, 213syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ≠ 0)
215211, 214logcld 25081 . . . . . . . . . . . . . 14 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑥) ∈ ℂ)
216215adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈ ℂ)
217 ovexd 7180 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V)
218 simpr 485 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
21948, 218, 52sylancr 587 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
220206a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → -1 ∈ ℂ)
221 1cnd 10624 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
222 0cnd 10622 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
223 1cnd 10624 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℂ)
224192, 223dvmptc 24482 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 1)) = (𝑦 ∈ ℂ ↦ 0))
225192dvmptid 24481 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
226192, 221, 222, 224, 218, 221, 225dvmptsub 24491 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 − 1)))
227 df-neg 10861 . . . . . . . . . . . . . . . 16 -1 = (0 − 1)
228227mpteq2i 5149 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ -1) = (𝑦 ∈ ℂ ↦ (0 − 1))
229226, 228syl6eqr 2871 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1))
23050a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
231 eqid 2818 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
232231cnfldtopon 23318 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
233232toponrestid 21457 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
234231cnfldtopn 23317 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
235234blopn 23037 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
23638, 28, 39, 235mp3an 1452 . . . . . . . . . . . . . . 15 (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld)
237236a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
238192, 219, 220, 229, 230, 233, 231, 237dvmptres 24487 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -1))
239208dvlog2 25163 . . . . . . . . . . . . . 14 (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥))
240 logf1o 25075 . . . . . . . . . . . . . . . . . . . 20 log:(ℂ ∖ {0})–1-1-onto→ran log
241 f1of 6608 . . . . . . . . . . . . . . . . . . . 20 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
242240, 241ax-mp 5 . . . . . . . . . . . . . . . . . . 19 log:(ℂ ∖ {0})⟶ran log
243212logdmss 25152 . . . . . . . . . . . . . . . . . . . 20 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
244209, 243sstri 3973 . . . . . . . . . . . . . . . . . . 19 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
245 fssres 6537 . . . . . . . . . . . . . . . . . . 19 ((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
246242, 244, 245mp2an 688 . . . . . . . . . . . . . . . . . 18 (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log
247246a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
248247feqmptd 6726 . . . . . . . . . . . . . . . 16 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)))
249 fvres 6682 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥) = (log‘𝑥))
250249mpteq2ia 5148 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))
251248, 250syl6eq 2869 . . . . . . . . . . . . . . 15 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))
252251oveq2d 7161 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))))
253239, 252syl5reqr 2868 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥)))
254 fveq2 6663 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦)))
255 oveq2 7153 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦)))
256192, 192, 205, 207, 216, 217, 238, 253, 254, 255dvmptco 24496 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ ((1 / (1 − 𝑦)) · -1)))
257192, 193, 194, 256dvmptneg 24490 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)))
25853, 74reccld 11397 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ)
259 mulcom 10611 . . . . . . . . . . . . . . . 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 11080 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦)))
262260, 261eqtrd 2853 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦)))
263262negeqd 10868 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦)))
264258negnegd 10976 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦)))
265263, 264eqtrd 2853 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦)))
266265mpteq2ia 5148 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
267257, 266syl6eq 2869 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
268267dmeqd 5767 . . . . . . . . 9 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
269 dmmptg 6089 . . . . . . . . . 10 (∀𝑦 ∈ (0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1))
270 ovexd 7180 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ V)
271269, 270mprg 3149 . . . . . . . . 9 dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1)
272268, 271syl6eq 2869 . . . . . . . 8 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (0(ball‘(abs ∘ − ))1))
273 sumex 15032 . . . . . . . . . . . 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 6663 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
276275cbvsumv 15041 . . . . . . . . . . . . . 14 Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘)
277181, 276syl6eq 2869 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
278277mpteq2ia 5148 . . . . . . . . . . . 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 2818 . . . . . . . . . . . 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 24945 . . . . . . . . . . 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 3968 . . . . . . . . . . . 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 24487 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
284 nnnn0 11892 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
285284adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
286 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0))
287 oveq2 7153 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
288286, 287ifbieq2d 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛)))
289 ovex 7178 . . . . . . . . . . . . . . . . . . . . 21 (1 / 𝑛) ∈ V
29090, 289ifex 4511 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V
291288, 89, 290fvmpt 6761 . . . . . . . . . . . . . . . . . . 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 11659 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
294293adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
295294neneqd 3018 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
296295iffalsed 4474 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
297292, 296eqtrd 2853 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛))
298297oveq2d 7161 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛)))
299 nncn 11634 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
300299adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
301300, 294recidd 11399 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1)
302298, 301eqtrd 2853 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1)
303302oveq1d 7160 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1))))
304 nnm1nn0 11926 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
305 expcl 13435 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
30651, 304, 305syl2an 595 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
307306mulid2d 10647 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
308303, 307eqtrd 2853 . . . . . . . . . . . . 13 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
309308sumeq2dv 15048 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)))
310 nnuz 12269 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
311 1e0p1 12128 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
312311fveq2i 6666 . . . . . . . . . . . . . . 15 (ℤ‘1) = (ℤ‘(0 + 1))
313310, 312eqtri 2841 . . . . . . . . . . . . . 14 ℕ = (ℤ‘(0 + 1))
314 oveq1 7152 . . . . . . . . . . . . . . 15 (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1))
315314oveq2d 7161 . . . . . . . . . . . . . 14 (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1)))
316 1zzd 12001 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ∈ ℤ)
317 0zd 11981 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℤ)
3181, 313, 315, 316, 317, 306isumshft 15182 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)))
319 pncan2 10881 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚)
32048, 99, 319sylancr 587 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((1 + 𝑚) − 1) = 𝑚)
321320oveq2d 7161 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑦↑((1 + 𝑚) − 1)) = (𝑦𝑚))
322321sumeq2i 15044 . . . . . . . . . . . . 13 Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚)
323318, 322syl6eq 2869 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚))
324 geoisum 15221 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ (abs‘𝑦) < 1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
32551, 64, 324syl2anc 584 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
326309, 323, 3253eqtrd 2857 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦)))
327326mpteq2ia 5148 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
328283, 327syl6eq 2869 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
329267, 328eqtr4d 2856 . . . . . . . 8 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))))
330 1rp 12381 . . . . . . . . . 10 1 ∈ ℝ+
331 blcntr 22950 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘ − ))1))
33238, 28, 330, 331mp3an 1452 . . . . . . . . 9 0 ∈ (0(ball‘(abs ∘ − ))1)
333332a1i 11 . . . . . . . 8 (⊤ → 0 ∈ (0(ball‘(abs ∘ − ))1))
334 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (1 − 𝑦) = (1 − 0))
335 1m0e1 11746 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
336334, 335syl6eq 2869 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (1 − 𝑦) = 1)
337336fveq2d 6667 . . . . . . . . . . . . . 14 (𝑦 = 0 → (log‘(1 − 𝑦)) = (log‘1))
338 log1 25096 . . . . . . . . . . . . . 14 (log‘1) = 0
339337, 338syl6eq 2869 . . . . . . . . . . . . 13 (𝑦 = 0 → (log‘(1 − 𝑦)) = 0)
340339negeqd 10868 . . . . . . . . . . . 12 (𝑦 = 0 → -(log‘(1 − 𝑦)) = -0)
341 neg0 10920 . . . . . . . . . . . 12 -0 = 0
342340, 341syl6eq 2869 . . . . . . . . . . 11 (𝑦 = 0 → -(log‘(1 − 𝑦)) = 0)
343 eqid 2818 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))
344342, 343, 90fvmpt 6761 . . . . . . . . . 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 7152 . . . . . . . . . . . . . . 15 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
347346eqeq1d 2820 . . . . . . . . . . . . . 14 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
348 oveq1 7152 . . . . . . . . . . . . . . 15 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
349348eqeq1d 2820 . . . . . . . . . . . . . 14 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
350 simpll 763 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0)
351350, 28syl6eqel 2918 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ)
352 simplr 765 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0)
353351, 352expcld 13498 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦𝑛) ∈ ℂ)
354353mul02d 10826 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦𝑛)) = 0)
355 simpll 763 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑦 = 0)
356355oveq1d 7160 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = (0↑𝑛))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
358357, 14sylib 219 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
359358ord 858 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
360359con1d 147 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
361360imp 407 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
3623610expd 13491 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (0↑𝑛) = 0)
363356, 362eqtrd 2853 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = 0)
364363oveq2d 7161 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = ((1 / 𝑛) · 0))
365361nnrecred 11676 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
366365recnd 10657 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
367366mul01d 10827 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · 0) = 0)
368364, 367eqtrd 2853 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = 0)
369347, 349, 354, 368ifbothda 4500 . . . . . . . . . . . . 13 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
370369sumeq2dv 15048 . . . . . . . . . . . 12 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 0)
3711eqimssi 4022 . . . . . . . . . . . . . 14 0 ⊆ (ℤ‘0)
372371orci 859 . . . . . . . . . . . . 13 (ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin)
373 sumz 15067 . . . . . . . . . . . . 13 ((ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 = 0)
374372, 373ax-mp 5 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ0 0 = 0
375370, 374syl6eq 2869 . . . . . . . . . . 11 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
376 eqid 2818 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
377375, 376, 90fvmpt 6761 . . . . . . . . . 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 2856 . . . . . . . 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 24525 . . . . . . 7 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))))
381380fveq1d 6665 . . . . . 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 7153 . . . . . . . 8 (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴))
384383fveq2d 6667 . . . . . . 7 (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴)))
385384negeqd 10868 . . . . . 6 (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 − 𝐴)))
386 negex 10872 . . . . . 6 -(log‘(1 − 𝐴)) ∈ V
387385, 343, 386fvmpt 6761 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴)))
388 oveq1 7152 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑛) = (𝐴𝑛))
389388oveq2d 7161 . . . . . . 7 (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
390389sumeq2sdv 15049 . . . . . 6 (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
391 sumex 15032 . . . . . 6 Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
392390, 376, 391fvmpt 6761 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
393382, 387, 3923eqtr3d 2861 . . . 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 5085 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)))
396 seqex 13359 . . . 4 seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V
397396a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V)
398 seqex 13359 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V
399398a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V)
400 1zzd 12001 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℤ)
401 elnnuz 12270 . . . . . 6 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
402 fvres 6682 . . . . . 6 (𝑛 ∈ (ℤ‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
403401, 402sylbi 218 . . . . 5 (𝑛 ∈ ℕ → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
404403eqcomd 2824 . . . 4 (𝑛 ∈ ℕ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛))
405 addid2 10811 . . . . . . . 8 (𝑛 ∈ ℂ → (0 + 𝑛) = 𝑛)
406405adantl 482 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℂ) → (0 + 𝑛) = 𝑛)
407 0cnd 10622 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℂ)
408 1eluzge0 12280 . . . . . . . 8 1 ∈ (ℤ‘0)
409408a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ (ℤ‘0))
410 0cnd 10622 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
411 nn0cn 11895 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
412411adantl 482 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
413 neqne 3021 . . . . . . . . . . . 12 𝑘 = 0 → 𝑘 ≠ 0)
414 reccl 11293 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
415412, 413, 414syl2an 595 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
416410, 415ifclda 4497 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
417 expcl 13435 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
418417adantlr 711 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
419416, 418mulcld 10649 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
420419fmpttd 6871 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ)
421 1nn0 11901 . . . . . . . 8 1 ∈ ℕ0
422 ffvelrn 6841 . . . . . . . 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 12906 . . . . . . . . . 10 (𝑛 ∈ (0...0) → 𝑛 = 0)
425 1m1e0 11697 . . . . . . . . . . 11 (1 − 1) = 0
426425oveq2i 7156 . . . . . . . . . 10 (0...(1 − 1)) = (0...0)
427424, 426eleq2s 2928 . . . . . . . . 9 (𝑛 ∈ (0...(1 − 1)) → 𝑛 = 0)
428427fveq2d 6667 . . . . . . . 8 (𝑛 ∈ (0...(1 − 1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0))
429 0nn0 11900 . . . . . . . . . 10 0 ∈ ℕ0
430 iftrue 4469 . . . . . . . . . . . 12 (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0)
431 oveq2 7153 . . . . . . . . . . . 12 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
432430, 431oveq12d 7163 . . . . . . . . . . 11 (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (0 · (𝐴↑0)))
433 ovex 7178 . . . . . . . . . . 11 (0 · (𝐴↑0)) ∈ V
434432, 8, 433fvmpt 6761 . . . . . . . . . 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 13435 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝐴↑0) ∈ ℂ)
43727, 429, 436sylancl 586 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴↑0) ∈ ℂ)
438437mul02d 10826 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (0 · (𝐴↑0)) = 0)
439435, 438syl5eq 2865 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = 0)
440428, 439sylan9eqr 2875 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (0...(1 − 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = 0)
441406, 407, 409, 423, 440seqid 13403 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))))
442293adantl 482 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
443442neneqd 3018 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
444443iffalsed 4474 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
445444oveq1d 7160 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((1 / 𝑛) · (𝐴𝑛)))
446284, 23sylan2 592 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ ℂ)
447299adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
448446, 447, 442divrec2d 11408 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴𝑛)))
449445, 448eqtr4d 2856 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((𝐴𝑛) / 𝑛))
450284, 11sylan2 592 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
451 id 22 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑘 = 𝑛)
4526, 451oveq12d 7163 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) / 𝑘) = ((𝐴𝑛) / 𝑛))
453 eqid 2818 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))
454 ovex 7178 . . . . . . . . . . 11 ((𝐴𝑛) / 𝑛) ∈ V
455452, 453, 454fvmpt 6761 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
456455adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
457449, 450, 4563eqtr4d 2863 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
458401, 457sylan2br 594 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
459400, 458seqfeq 13383 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
460441, 459eqtrd 2853 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
461460fveq1d 6665 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
462404, 461sylan9eqr 2875 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
463310, 397, 399, 400, 462climeq 14912 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))))
464395, 463mpbid 233 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wtru 1529  wcel 2105  wne 3013  {crab 3139  Vcvv 3492  cdif 3930  wss 3933  ifcif 4463  {csn 4557  {cpr 4559   class class class wbr 5057  cmpt 5137  ccnv 5547  dom cdm 5548  ran crn 5549  cres 5550  cima 5551  ccom 5552   Fn wfn 6343  wf 6344  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  Fincfn 8497  supcsup 8892  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  +∞cpnf 10660  -∞cmnf 10661  *cxr 10662   < clt 10663  cle 10664  cmin 10858  -cneg 10859   / cdiv 11285  cn 11626  2c2 11680  0cn0 11885  cuz 12231  +crp 12377  (,]cioc 12727  [,)cico 12728  [,]cicc 12729  ...cfz 12880  seqcseq 13357  cexp 13417  abscabs 14581  cli 14829  Σcsu 15030  TopOpenctopn 16683  ∞Metcxmet 20458  ballcbl 20460  fldccnfld 20473  cnccncf 23411   D cdv 24388  logclog 25065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-tan 15413  df-pi 15414  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-limc 24391  df-dv 24392  df-ulm 24892  df-log 25067
This theorem is referenced by:  logtaylsum  25171  logtayl2  25172  atantayl  25442  stirlinglem5  42240
  Copyright terms: Public domain W3C validator