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

Theorem logtayl 24451
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 11760 . . . 4 0 = (ℤ‘0)
2 0zd 11427 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℤ)
3 eqeq1 2655 . . . . . . . 8 (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0))
4 oveq2 6698 . . . . . . . 8 (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛))
53, 4ifbieq2d 4144 . . . . . . 7 (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛)))
6 oveq2 6698 . . . . . . 7 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
75, 6oveq12d 6708 . . . . . 6 (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
8 eqid 2651 . . . . . 6 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
9 ovex 6718 . . . . . 6 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
107, 8, 9fvmpt 6321 . . . . 5 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
1110adantl 481 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
12 0cnd 10071 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 0 ∈ ℂ)
13 simpr 476 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
14 elnn0 11332 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↔ (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1513, 14sylib 208 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1615ord 391 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
1716con1d 139 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
1817imp 444 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
1918nnrecred 11104 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
2019recnd 10106 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
2112, 20ifclda 4153 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ)
22 expcl 12918 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2322adantlr 751 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2421, 23mulcld 10098 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ ℂ)
25 logtayllem 24450 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ dom ⇝ )
261, 2, 11, 24, 25isumclim2 14533 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
27 simpl 472 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
28 0cn 10070 . . . . . . . 8 0 ∈ ℂ
29 eqid 2651 . . . . . . . . 9 (abs ∘ − ) = (abs ∘ − )
3029cnmetdval 22621 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
3127, 28, 30sylancl 695 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
32 subid1 10339 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3332adantr 480 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 − 0) = 𝐴)
3433fveq2d 6233 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(𝐴 − 0)) = (abs‘𝐴))
3531, 34eqtrd 2685 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘𝐴))
36 simpr 476 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3735, 36eqbrtrd 4707 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) < 1)
38 cnxmet 22623 . . . . . . 7 (abs ∘ − ) ∈ (∞Met‘ℂ)
39 1rp 11874 . . . . . . . 8 1 ∈ ℝ+
40 rpxr 11878 . . . . . . . 8 (1 ∈ ℝ+ → 1 ∈ ℝ*)
4139, 40ax-mp 5 . . . . . . 7 1 ∈ ℝ*
42 elbl3 22244 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4338, 41, 42mpanl12 718 . . . . . 6 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4428, 27, 43sylancr 696 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4537, 44mpbird 247 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ (0(ball‘(abs ∘ − ))1))
46 tru 1527 . . . . . 6
47 eqid 2651 . . . . . . . 8 (0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘ − ))1)
48 0cnd 10071 . . . . . . . 8 (⊤ → 0 ∈ ℂ)
4941a1i 11 . . . . . . . 8 (⊤ → 1 ∈ ℝ*)
50 ax-1cn 10032 . . . . . . . . . . . . 13 1 ∈ ℂ
51 blssm 22270 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
5238, 28, 41, 51mp3an 1464 . . . . . . . . . . . . . 14 (0(ball‘(abs ∘ − ))1) ⊆ ℂ
5352sseli 3632 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ ℂ)
54 subcl 10318 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
5550, 53, 54sylancr 696 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ ℂ)
5653abscld 14219 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ)
5729cnmetdval 22621 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5853, 28, 57sylancl 695 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5953subid1d 10419 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 − 0) = 𝑦)
6059fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦))
6158, 60eqtrd 2685 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦))
62 elbl3 22244 . . . . . . . . . . . . . . . . . . 19 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6338, 41, 62mpanl12 718 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6428, 53, 63sylancr 696 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6564ibi 256 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) < 1)
6661, 65eqbrtrrd 4709 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < 1)
6756, 66gtned 10210 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ (abs‘𝑦))
68 abs1 14081 . . . . . . . . . . . . . . . 16 (abs‘1) = 1
69 fveq2 6229 . . . . . . . . . . . . . . . 16 (1 = 𝑦 → (abs‘1) = (abs‘𝑦))
7068, 69syl5eqr 2699 . . . . . . . . . . . . . . 15 (1 = 𝑦 → 1 = (abs‘𝑦))
7170necon3i 2855 . . . . . . . . . . . . . 14 (1 ≠ (abs‘𝑦) → 1 ≠ 𝑦)
7267, 71syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ 𝑦)
73 subeq0 10345 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦))
7473necon3bid 2867 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7550, 53, 74sylancr 696 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7672, 75mpbird 247 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ≠ 0)
7755, 76logcld 24362 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ)
7877negcld 10417 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ)
7978adantl 481 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 − 𝑦)) ∈ ℂ)
80 eqid 2651 . . . . . . . . 9 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))
8179, 80fmptd 6425 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
8253absge0d 14227 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (abs‘𝑦))
8356rexrd 10127 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ*)
84 peano2re 10247 . . . . . . . . . . . . . . . 16 ((abs‘𝑦) ∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ)
8556, 84syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ)
8685rehalfcld 11317 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ)
8786rexrd 10127 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ*)
88 iccssxr 12294 . . . . . . . . . . . . . . 15 (0[,]+∞) ⊆ ℝ*
89 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0))
90 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
9189, 90ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗)))
92 eqid 2651 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))
93 c0ex 10072 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
94 ovex 6718 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 𝑗) ∈ V
9593, 94ifex 4189 . . . . . . . . . . . . . . . . . . . . 21 if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V
9691, 92, 95fvmpt 6321 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗)))
9796eqcomd 2657 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → if(𝑗 = 0, 0, (1 / 𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗))
9897oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9998mpteq2ia 4773 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
10099mpteq2i 4774 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗))))
101 0cnd 10071 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈ ℂ)
102 nn0cn 11340 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
103102adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
104 df-ne 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ≠ 0 ↔ ¬ 𝑚 = 0)
105104biimpri 218 . . . . . . . . . . . . . . . . . . 19 𝑚 = 0 → 𝑚 ≠ 0)
106 reccl 10730 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈ ℂ)
107103, 105, 106syl2an 493 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ)
108101, 107ifclda 4153 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑚 ∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ)
109108, 92fmptd 6425 . . . . . . . . . . . . . . . 16 (⊤ → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
110 recn 10064 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ → 𝑟 ∈ ℂ)
111 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑟 → (𝑥𝑗) = (𝑟𝑗))
112111oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))
113112mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
114 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))
115 nn0ex 11336 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
116115mptex 6527 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) ∈ V
117113, 114, 116fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
118110, 117syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
119118eqcomd 2657 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟))
120119seqeq3d 12849 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)))
121120eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ → (seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ ↔ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ ))
122121rabbiia 3215 . . . . . . . . . . . . . . . . 17 {𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }
123122supeq1i 8394 . . . . . . . . . . . . . . . 16 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
124100, 109, 123radcnvcl 24216 . . . . . . . . . . . . . . 15 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
12588, 124sseldi 3634 . . . . . . . . . . . . . 14 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
12646, 125mp1i 13 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
127 1re 10077 . . . . . . . . . . . . . . 15 1 ∈ ℝ
128 avglt1 11308 . . . . . . . . . . . . . . 15 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12956, 127, 128sylancl 695 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
13066, 129mpbid 222 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))
131 0red 10079 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℝ)
132131, 56, 86, 82, 130lelttrd 10233 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2))
133131, 86, 132ltled 10223 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2))
13486, 133absidd 14205 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) = (((abs‘𝑦) + 1) / 2))
13546, 109mp1i 13 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
13686recnd 10106 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ)
137 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗))
138137oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))
139138mpteq2dv 4778 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
140115mptex 6527 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) ∈ V
141139, 114, 140fvmpt 6321 . . . . . . . . . . . . . . . . . 18 ((((abs‘𝑦) + 1) / 2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
142136, 141syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
143142seqeq3d 12849 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) = seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))))
144 avglt2 11309 . . . . . . . . . . . . . . . . . . . 20 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14556, 127, 144sylancl 695 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14666, 145mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1)
147134, 146eqbrtrd 4707 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1)
148 logtayllem 24450 . . . . . . . . . . . . . . . . 17 (((((abs‘𝑦) + 1) / 2) ∈ ℂ ∧ (abs‘(((abs‘𝑦) + 1) / 2)) < 1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
149136, 147, 148syl2anc 694 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
150143, 149eqeltrd 2730 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝ )
151100, 135, 123, 136, 150radcnvle 24219 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
152134, 151eqbrtrrd 4709 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
15383, 87, 126, 130, 152xrltletrd 12030 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
154 0re 10078 . . . . . . . . . . . . 13 0 ∈ ℝ
155 elico2 12275 . . . . . . . . . . . . 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 ⇝ }, ℝ*, < ))))
156154, 126, 155sylancr 696 . . . . . . . . . . . 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 ⇝ }, ℝ*, < ))))
15756, 82, 153, 156mpbir3and 1264 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
158 absf 14121 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
159 ffn 6083 . . . . . . . . . . . 12 (abs:ℂ⟶ℝ → abs Fn ℂ)
160 elpreima 6377 . . . . . . . . . . . 12 (abs Fn ℂ → (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))))
161158, 159, 160mp2b 10 . . . . . . . . . . 11 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
16253, 157, 161sylanbrc 699 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
163 cnvimass 5520 . . . . . . . . . . . . . . . . . 18 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
164158fdmi 6090 . . . . . . . . . . . . . . . . . 18 dom abs = ℂ
165163, 164sseqtri 3670 . . . . . . . . . . . . . . . . 17 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
166165sseli 3632 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → 𝑦 ∈ ℂ)
167 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝑥𝑗) = (𝑦𝑗))
168167oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
169168mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
170115mptex 6527 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) ∈ V
171169, 114, 170fvmpt 6321 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
172171adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
173172fveq1d 6231 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛))
174 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0))
175 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛))
176174, 175ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛)))
177 oveq2 6698 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (𝑦𝑗) = (𝑦𝑛))
178176, 177oveq12d 6708 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
179 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
180 ovex 6718 . . . . . . . . . . . . . . . . . . . 20 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ V
181178, 179, 180fvmpt 6321 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
182181adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
183173, 182eqtr2d 2686 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
184183sumeq2dv 14477 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
185166, 184syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
186185mpteq2ia 4773 . . . . . . . . . . . . . 14 (𝑦 ∈ (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 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
187 eqid 2651 . . . . . . . . . . . . . 14 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
188 eqid 2651 . . . . . . . . . . . . . 14 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))
189100, 186, 109, 123, 187, 188psercn 24225 . . . . . . . . . . . . 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 ⇝ }, ℝ*, < )))–cn→ℂ))
190 cncff 22743 . . . . . . . . . . . . 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 ⇝ }, ℝ*, < )))–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 ⇝ }, ℝ*, < )))⟶ℂ)
191189, 190syl 17 . . . . . . . . . . . 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 ⇝ }, ℝ*, < )))⟶ℂ)
192 eqid 2651 . . . . . . . . . . . . 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 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
193192fmpt 6421 . . . . . . . . . . . 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 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))⟶ℂ)
194191, 193sylibr 224 . . . . . . . . . . 11 (⊤ → ∀𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
195194r19.21bi 2961 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
196162, 195sylan2 490 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
197 eqid 2651 . . . . . . . . 9 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
198196, 197fmptd 6425 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
199 cnelprrecn 10067 . . . . . . . . . . . . 13 ℂ ∈ {ℝ, ℂ}
200199a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
20177adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 − 𝑦)) ∈ ℂ)
202 ovexd 6720 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈ V)
20329cnmetdval 22621 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 − 𝑦) ∈ ℂ) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
20450, 55, 203sylancr 696 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
205 nncan 10348 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦)
20650, 53, 205sylancr 696 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦)
207206fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦))
208204, 207eqtrd 2685 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦))
209208, 66eqbrtrd 4707 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1)
210 elbl 22240 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1)))
21138, 50, 41, 210mp3an 1464 . . . . . . . . . . . . . . 15 ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1))
21255, 209, 211sylanbrc 699 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
213212adantl 481 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
214 neg1cn 11162 . . . . . . . . . . . . . 14 -1 ∈ ℂ
215214a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈ ℂ)
216 eqid 2651 . . . . . . . . . . . . . . . . . 18 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
217216dvlog2lem 24443 . . . . . . . . . . . . . . . . 17 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
218217sseli 3632 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ (ℂ ∖ (-∞(,]0)))
219218eldifad 3619 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ ℂ)
220 eqid 2651 . . . . . . . . . . . . . . . . 17 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
221220logdmn0 24431 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ≠ 0)
222218, 221syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ≠ 0)
223219, 222logcld 24362 . . . . . . . . . . . . . 14 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑥) ∈ ℂ)
224223adantl 481 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈ ℂ)
225 ovexd 6720 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V)
226 simpr 476 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
22750, 226, 54sylancr 696 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
228214a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → -1 ∈ ℂ)
229 1cnd 10094 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
230 0cnd 10071 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
231 1cnd 10094 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℂ)
232200, 231dvmptc 23766 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 1)) = (𝑦 ∈ ℂ ↦ 0))
233200dvmptid 23765 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
234200, 229, 230, 232, 226, 229, 233dvmptsub 23775 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 − 1)))
235 df-neg 10307 . . . . . . . . . . . . . . . 16 -1 = (0 − 1)
236235mpteq2i 4774 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ -1) = (𝑦 ∈ ℂ ↦ (0 − 1))
237234, 236syl6eqr 2703 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1))
23852a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
239 eqid 2651 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
240239cnfldtop 22634 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) ∈ Top
241239cnfldtopon 22633 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
242241toponunii 20769 . . . . . . . . . . . . . . . . 17 ℂ = (TopOpen‘ℂfld)
243242restid 16141 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
244240, 243ax-mp 5 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
245244eqcomi 2660 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
246239cnfldtopn 22632 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
247246blopn 22352 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
24838, 28, 41, 247mp3an 1464 . . . . . . . . . . . . . . 15 (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld)
249248a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
250200, 227, 228, 237, 238, 245, 239, 249dvmptres 23771 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -1))
251216dvlog2 24444 . . . . . . . . . . . . . 14 (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥))
252 logf1o 24356 . . . . . . . . . . . . . . . . . . . 20 log:(ℂ ∖ {0})–1-1-onto→ran log
253 f1of 6175 . . . . . . . . . . . . . . . . . . . 20 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
254252, 253ax-mp 5 . . . . . . . . . . . . . . . . . . 19 log:(ℂ ∖ {0})⟶ran log
255220logdmss 24433 . . . . . . . . . . . . . . . . . . . 20 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
256217, 255sstri 3645 . . . . . . . . . . . . . . . . . . 19 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
257 fssres 6108 . . . . . . . . . . . . . . . . . . 19 ((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
258254, 256, 257mp2an 708 . . . . . . . . . . . . . . . . . 18 (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log
259258a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
260259feqmptd 6288 . . . . . . . . . . . . . . . 16 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)))
261 fvres 6245 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥) = (log‘𝑥))
262261mpteq2ia 4773 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))
263260, 262syl6eq 2701 . . . . . . . . . . . . . . 15 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))
264263oveq2d 6706 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))))
265251, 264syl5reqr 2700 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥)))
266 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦)))
267 oveq2 6698 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦)))
268200, 200, 213, 215, 224, 225, 250, 265, 266, 267dvmptco 23780 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ ((1 / (1 − 𝑦)) · -1)))
269200, 201, 202, 268dvmptneg 23774 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)))
27055, 76reccld 10832 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ)
271 mulcom 10060 . . . . . . . . . . . . . . . 16 (((1 / (1 − 𝑦)) ∈ ℂ ∧ -1 ∈ ℂ) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
272270, 214, 271sylancl 695 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
273270mulm1d 10520 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦)))
274272, 273eqtrd 2685 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦)))
275274negeqd 10313 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦)))
276270negnegd 10421 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦)))
277275, 276eqtrd 2685 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦)))
278277mpteq2ia 4773 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
279269, 278syl6eq 2701 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
280279dmeqd 5358 . . . . . . . . 9 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
281 dmmptg 5670 . . . . . . . . . 10 (∀𝑦 ∈ (0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1))
282 ovexd 6720 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ V)
283281, 282mprg 2955 . . . . . . . . 9 dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1)
284280, 283syl6eq 2701 . . . . . . . 8 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (0(ball‘(abs ∘ − ))1))
285 sumex 14462 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V
286285a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V)
287 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
288287cbvsumv 14470 . . . . . . . . . . . . . 14 Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘)
289185, 288syl6eq 2701 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
290289mpteq2ia 4773 . . . . . . . . . . . 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 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
291 eqid 2651 . . . . . . . . . . . 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))
292100, 290, 109, 123, 187, 188, 291pserdv2 24229 . . . . . . . . . . 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)))))
293162ssriv 3640 . . . . . . . . . . . 12 (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
294293a1i 11 . . . . . . . . . . 11 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
295200, 195, 286, 292, 294, 245, 239, 249dvmptres 23771 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
296 nnnn0 11337 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
297296adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
298 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0))
299 oveq2 6698 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
300298, 299ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛)))
301 ovex 6718 . . . . . . . . . . . . . . . . . . . . 21 (1 / 𝑛) ∈ V
30293, 301ifex 4189 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V
303300, 92, 302fvmpt 6321 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
304297, 303syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
305 nnne0 11091 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
306305adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
307306neneqd 2828 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
308307iffalsed 4130 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
309304, 308eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛))
310309oveq2d 6706 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛)))
311 nncn 11066 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
312311adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
313312, 306recidd 10834 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1)
314310, 313eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1)
315314oveq1d 6705 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1))))
316 nnm1nn0 11372 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
317 expcl 12918 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
31853, 316, 317syl2an 493 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
319318mulid2d 10096 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
320315, 319eqtrd 2685 . . . . . . . . . . . . 13 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
321320sumeq2dv 14477 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)))
322 nnuz 11761 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
323 1e0p1 11590 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
324323fveq2i 6232 . . . . . . . . . . . . . . 15 (ℤ‘1) = (ℤ‘(0 + 1))
325322, 324eqtri 2673 . . . . . . . . . . . . . 14 ℕ = (ℤ‘(0 + 1))
326 oveq1 6697 . . . . . . . . . . . . . . 15 (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1))
327326oveq2d 6706 . . . . . . . . . . . . . 14 (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1)))
328 1zzd 11446 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ∈ ℤ)
329 0zd 11427 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℤ)
3301, 325, 327, 328, 329, 318isumshft 14615 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)))
331 pncan2 10326 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚)
33250, 102, 331sylancr 696 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((1 + 𝑚) − 1) = 𝑚)
333332oveq2d 6706 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑦↑((1 + 𝑚) − 1)) = (𝑦𝑚))
334333sumeq2i 14473 . . . . . . . . . . . . 13 Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚)
335330, 334syl6eq 2701 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚))
336 geoisum 14652 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ (abs‘𝑦) < 1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
33753, 66, 336syl2anc 694 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
338321, 335, 3373eqtrd 2689 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦)))
339338mpteq2ia 4773 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
340295, 339syl6eq 2701 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
341279, 340eqtr4d 2688 . . . . . . . 8 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))))
342 blcntr 22265 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘ − ))1))
34338, 28, 39, 342mp3an 1464 . . . . . . . . 9 0 ∈ (0(ball‘(abs ∘ − ))1)
344343a1i 11 . . . . . . . 8 (⊤ → 0 ∈ (0(ball‘(abs ∘ − ))1))
345 oveq2 6698 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (1 − 𝑦) = (1 − 0))
346 1m0e1 11169 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
347345, 346syl6eq 2701 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (1 − 𝑦) = 1)
348347fveq2d 6233 . . . . . . . . . . . . . 14 (𝑦 = 0 → (log‘(1 − 𝑦)) = (log‘1))
349 log1 24377 . . . . . . . . . . . . . 14 (log‘1) = 0
350348, 349syl6eq 2701 . . . . . . . . . . . . 13 (𝑦 = 0 → (log‘(1 − 𝑦)) = 0)
351350negeqd 10313 . . . . . . . . . . . 12 (𝑦 = 0 → -(log‘(1 − 𝑦)) = -0)
352 neg0 10365 . . . . . . . . . . . 12 -0 = 0
353351, 352syl6eq 2701 . . . . . . . . . . 11 (𝑦 = 0 → -(log‘(1 − 𝑦)) = 0)
354353, 80, 93fvmpt 6321 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
355343, 354mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
356 oveq1 6697 . . . . . . . . . . . . . . 15 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
357356eqeq1d 2653 . . . . . . . . . . . . . 14 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
358 oveq1 6697 . . . . . . . . . . . . . . 15 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
359358eqeq1d 2653 . . . . . . . . . . . . . 14 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
360 simpll 805 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0)
361360, 28syl6eqel 2738 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ)
362 simplr 807 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0)
363361, 362expcld 13048 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦𝑛) ∈ ℂ)
364363mul02d 10272 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦𝑛)) = 0)
365 simpll 805 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑦 = 0)
366365oveq1d 6705 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = (0↑𝑛))
367 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
368367, 14sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
369368ord 391 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
370369con1d 139 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
371370imp 444 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
3723710expd 13064 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (0↑𝑛) = 0)
373366, 372eqtrd 2685 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = 0)
374373oveq2d 6706 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = ((1 / 𝑛) · 0))
375371nnrecred 11104 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
376375recnd 10106 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
377376mul01d 10273 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · 0) = 0)
378374, 377eqtrd 2685 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = 0)
379357, 359, 364, 378ifbothda 4156 . . . . . . . . . . . . 13 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
380379sumeq2dv 14477 . . . . . . . . . . . 12 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 0)
3811eqimssi 3692 . . . . . . . . . . . . . 14 0 ⊆ (ℤ‘0)
382381orci 404 . . . . . . . . . . . . 13 (ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin)
383 sumz 14497 . . . . . . . . . . . . 13 ((ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 = 0)
384382, 383ax-mp 5 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ0 0 = 0
385380, 384syl6eq 2701 . . . . . . . . . . 11 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
386385, 197, 93fvmpt 6321 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
387343, 386mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
388355, 387eqtr4d 2688 . . . . . . . 8 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0))
38947, 48, 49, 81, 198, 284, 341, 344, 388dv11cn 23809 . . . . . . 7 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))))
390389fveq1d 6231 . . . . . 6 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
39146, 390mp1i 13 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
392 oveq2 6698 . . . . . . . 8 (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴))
393392fveq2d 6233 . . . . . . 7 (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴)))
394393negeqd 10313 . . . . . 6 (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 − 𝐴)))
395 negex 10317 . . . . . 6 -(log‘(1 − 𝐴)) ∈ V
396394, 80, 395fvmpt 6321 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴)))
397 oveq1 6697 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑛) = (𝐴𝑛))
398397oveq2d 6706 . . . . . . 7 (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
399398sumeq2sdv 14479 . . . . . 6 (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
400 sumex 14462 . . . . . 6 Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
401399, 197, 400fvmpt 6321 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
402391, 396, 4013eqtr3d 2693 . . . 4 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
40345, 402syl 17 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
40426, 403breqtrrd 4713 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)))
405 seqex 12843 . . . 4 seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V
406405a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V)
407 seqex 12843 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V
408407a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V)
409 1zzd 11446 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℤ)
410 elnnuz 11762 . . . . . 6 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
411 fvres 6245 . . . . . 6 (𝑛 ∈ (ℤ‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
412410, 411sylbi 207 . . . . 5 (𝑛 ∈ ℕ → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
413412eqcomd 2657 . . . 4 (𝑛 ∈ ℕ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛))
414 addid2 10257 . . . . . . . 8 (𝑛 ∈ ℂ → (0 + 𝑛) = 𝑛)
415414adantl 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℂ) → (0 + 𝑛) = 𝑛)
416 0cnd 10071 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℂ)
417 1eluzge0 11770 . . . . . . . 8 1 ∈ (ℤ‘0)
418417a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ (ℤ‘0))
419 0cnd 10071 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
420 nn0cn 11340 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
421420adantl 481 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
422 df-ne 2824 . . . . . . . . . . . . 13 (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0)
423422biimpri 218 . . . . . . . . . . . 12 𝑘 = 0 → 𝑘 ≠ 0)
424 reccl 10730 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
425421, 423, 424syl2an 493 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
426419, 425ifclda 4153 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
427 expcl 12918 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
428427adantlr 751 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
429426, 428mulcld 10098 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
430429, 8fmptd 6425 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ)
431 1nn0 11346 . . . . . . . 8 1 ∈ ℕ0
432 ffvelrn 6397 . . . . . . . 8 (((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
433430, 431, 432sylancl 695 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
434 elfz1eq 12390 . . . . . . . . . 10 (𝑛 ∈ (0...0) → 𝑛 = 0)
435 1m1e0 11127 . . . . . . . . . . 11 (1 − 1) = 0
436435oveq2i 6701 . . . . . . . . . 10 (0...(1 − 1)) = (0...0)
437434, 436eleq2s 2748 . . . . . . . . 9 (𝑛 ∈ (0...(1 − 1)) → 𝑛 = 0)
438437fveq2d 6233 . . . . . . . 8 (𝑛 ∈ (0...(1 − 1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0))
439 0nn0 11345 . . . . . . . . . 10 0 ∈ ℕ0
440 iftrue 4125 . . . . . . . . . . . 12 (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0)
441 oveq2 6698 . . . . . . . . . . . 12 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
442440, 441oveq12d 6708 . . . . . . . . . . 11 (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (0 · (𝐴↑0)))
443 ovex 6718 . . . . . . . . . . 11 (0 · (𝐴↑0)) ∈ V
444442, 8, 443fvmpt 6321 . . . . . . . . . 10 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0)))
445439, 444ax-mp 5 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0))
446 expcl 12918 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝐴↑0) ∈ ℂ)
44727, 439, 446sylancl 695 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴↑0) ∈ ℂ)
448447mul02d 10272 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (0 · (𝐴↑0)) = 0)
449445, 448syl5eq 2697 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = 0)
450438, 449sylan9eqr 2707 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (0...(1 − 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = 0)
451415, 416, 418, 433, 450seqid 12886 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))))
452305adantl 481 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
453452neneqd 2828 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
454453iffalsed 4130 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
455454oveq1d 6705 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((1 / 𝑛) · (𝐴𝑛)))
456296, 23sylan2 490 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ ℂ)
457311adantl 481 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
458456, 457, 452divrec2d 10843 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴𝑛)))
459455, 458eqtr4d 2688 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((𝐴𝑛) / 𝑛))
460296, 11sylan2 490 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
461 id 22 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑘 = 𝑛)
4626, 461oveq12d 6708 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) / 𝑘) = ((𝐴𝑛) / 𝑛))
463 eqid 2651 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))
464 ovex 6718 . . . . . . . . . . 11 ((𝐴𝑛) / 𝑛) ∈ V
465462, 463, 464fvmpt 6321 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
466465adantl 481 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
467459, 460, 4663eqtr4d 2695 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
468410, 467sylan2br 492 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
469409, 468seqfeq 12866 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
470451, 469eqtrd 2685 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
471470fveq1d 6231 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
472413, 471sylan9eqr 2707 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
473322, 406, 408, 409, 472climeq 14342 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))))
474404, 473mpbid 222 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wtru 1524  wcel 2030  wne 2823  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  wss 3607  ifcif 4119  {csn 4210  {cpr 4212   class class class wbr 4685  cmpt 4762  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Fincfn 7997  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  2c2 11108  0cn0 11330  cuz 11725  +crp 11870  (,]cioc 12214  [,)cico 12215  [,]cicc 12216  ...cfz 12364  seqcseq 12841  cexp 12900  abscabs 14018  cli 14259  Σcsu 14460  t crest 16128  TopOpenctopn 16129  ∞Metcxmt 19779  ballcbl 19781  fldccnfld 19794  Topctop 20746  cnccncf 22726   D cdv 23672  logclog 24346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-tan 14846  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-ulm 24176  df-log 24348
This theorem is referenced by:  logtaylsum  24452  logtayl2  24453  atantayl  24709  stirlinglem5  40613
  Copyright terms: Public domain W3C validator