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

Theorem logtayl 24938
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 12091 . . . 4 0 = (ℤ‘0)
2 0zd 11802 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℤ)
3 eqeq1 2779 . . . . . . . 8 (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0))
4 oveq2 6982 . . . . . . . 8 (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛))
53, 4ifbieq2d 4373 . . . . . . 7 (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛)))
6 oveq2 6982 . . . . . . 7 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
75, 6oveq12d 6992 . . . . . 6 (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
8 eqid 2775 . . . . . 6 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
9 ovex 7006 . . . . . 6 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
107, 8, 9fvmpt 6593 . . . . 5 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
1110adantl 474 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
12 0cnd 10428 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 0 ∈ ℂ)
13 simpr 477 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
14 elnn0 11706 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↔ (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1513, 14sylib 210 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1615ord 850 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
1716con1d 142 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
1817imp 398 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
1918nnrecred 11488 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
2019recnd 10464 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
2112, 20ifclda 4382 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ)
22 expcl 13259 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2322adantlr 702 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2421, 23mulcld 10456 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ ℂ)
25 logtayllem 24937 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ dom ⇝ )
261, 2, 11, 24, 25isumclim2 14967 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
27 simpl 475 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
28 0cn 10427 . . . . . . . 8 0 ∈ ℂ
29 eqid 2775 . . . . . . . . 9 (abs ∘ − ) = (abs ∘ − )
3029cnmetdval 23076 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
3127, 28, 30sylancl 577 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
32 subid1 10703 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3332adantr 473 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 − 0) = 𝐴)
3433fveq2d 6501 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(𝐴 − 0)) = (abs‘𝐴))
3531, 34eqtrd 2811 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘𝐴))
36 simpr 477 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3735, 36eqbrtrd 4949 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) < 1)
38 cnxmet 23078 . . . . . . 7 (abs ∘ − ) ∈ (∞Met‘ℂ)
39 1xr 10496 . . . . . . 7 1 ∈ ℝ*
40 elbl3 22699 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4138, 39, 40mpanl12 689 . . . . . 6 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4228, 27, 41sylancr 578 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4337, 42mpbird 249 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ (0(ball‘(abs ∘ − ))1))
44 tru 1511 . . . . . 6
45 eqid 2775 . . . . . . . 8 (0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘ − ))1)
46 0cnd 10428 . . . . . . . 8 (⊤ → 0 ∈ ℂ)
4739a1i 11 . . . . . . . 8 (⊤ → 1 ∈ ℝ*)
48 ax-1cn 10389 . . . . . . . . . . . . 13 1 ∈ ℂ
49 blssm 22725 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
5038, 28, 39, 49mp3an 1440 . . . . . . . . . . . . . 14 (0(ball‘(abs ∘ − ))1) ⊆ ℂ
5150sseli 3853 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ ℂ)
52 subcl 10681 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
5348, 51, 52sylancr 578 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ ℂ)
5451abscld 14651 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ)
5529cnmetdval 23076 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5651, 28, 55sylancl 577 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5751subid1d 10783 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 − 0) = 𝑦)
5857fveq2d 6501 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦))
5956, 58eqtrd 2811 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦))
60 elbl3 22699 . . . . . . . . . . . . . . . . . . 19 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6138, 39, 60mpanl12 689 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6228, 51, 61sylancr 578 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6362ibi 259 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) < 1)
6459, 63eqbrtrrd 4951 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < 1)
6554, 64gtned 10571 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ (abs‘𝑦))
66 abs1 14512 . . . . . . . . . . . . . . . 16 (abs‘1) = 1
67 fveq2 6497 . . . . . . . . . . . . . . . 16 (1 = 𝑦 → (abs‘1) = (abs‘𝑦))
6866, 67syl5eqr 2825 . . . . . . . . . . . . . . 15 (1 = 𝑦 → 1 = (abs‘𝑦))
6968necon3i 2996 . . . . . . . . . . . . . 14 (1 ≠ (abs‘𝑦) → 1 ≠ 𝑦)
7065, 69syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ 𝑦)
71 subeq0 10709 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦))
7271necon3bid 3008 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7348, 51, 72sylancr 578 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7470, 73mpbird 249 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ≠ 0)
7553, 74logcld 24849 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ)
7675negcld 10781 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ)
7776adantl 474 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 − 𝑦)) ∈ ℂ)
7877fmpttd 6700 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
7951absge0d 14659 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (abs‘𝑦))
8054rexrd 10486 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ*)
81 peano2re 10609 . . . . . . . . . . . . . . . 16 ((abs‘𝑦) ∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ)
8254, 81syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ)
8382rehalfcld 11691 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ)
8483rexrd 10486 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ*)
85 iccssxr 12632 . . . . . . . . . . . . . . 15 (0[,]+∞) ⊆ ℝ*
86 eqeq1 2779 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0))
87 oveq2 6982 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
8886, 87ifbieq2d 4373 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗)))
89 eqid 2775 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))
90 c0ex 10429 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
91 ovex 7006 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 𝑗) ∈ V
9290, 91ifex 4396 . . . . . . . . . . . . . . . . . . . . 21 if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V
9388, 89, 92fvmpt 6593 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗)))
9493eqcomd 2781 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → if(𝑗 = 0, 0, (1 / 𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗))
9594oveq1d 6989 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9695mpteq2ia 5016 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9796mpteq2i 5017 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗))))
98 0cnd 10428 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈ ℂ)
99 nn0cn 11715 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
10099adantl 474 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
101 neqne 2972 . . . . . . . . . . . . . . . . . . 19 𝑚 = 0 → 𝑚 ≠ 0)
102 reccl 11102 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈ ℂ)
103100, 101, 102syl2an 586 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ)
10498, 103ifclda 4382 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑚 ∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ)
105104fmpttd 6700 . . . . . . . . . . . . . . . 16 (⊤ → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
106 recn 10421 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ → 𝑟 ∈ ℂ)
107 oveq1 6981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑟 → (𝑥𝑗) = (𝑟𝑗))
108107oveq2d 6990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))
109108mpteq2dv 5021 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
110 eqid 2775 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))
111 nn0ex 11711 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
112111mptex 6810 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) ∈ V
113109, 110, 112fvmpt 6593 . . . . . . . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟))
116115seqeq3d 13189 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)))
117116eleq1d 2847 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ → (seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ ↔ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ ))
118117rabbiia 3395 . . . . . . . . . . . . . . . . 17 {𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }
119118supeq1i 8702 . . . . . . . . . . . . . . . 16 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
12097, 105, 119radcnvcl 24702 . . . . . . . . . . . . . . 15 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
12185, 120sseldi 3855 . . . . . . . . . . . . . 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 10435 . . . . . . . . . . . . . . 15 1 ∈ ℝ
124 avglt1 11682 . . . . . . . . . . . . . . 15 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12554, 123, 124sylancl 577 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12664, 125mpbid 224 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))
127 0red 10439 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℝ)
128127, 54, 83, 79, 126lelttrd 10594 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2))
129127, 83, 128ltled 10584 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2))
13083, 129absidd 14637 . . . . . . . . . . . . . 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 10464 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ)
133 oveq1 6981 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗))
134133oveq2d 6990 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))
135134mpteq2dv 5021 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
136111mptex 6810 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) ∈ V
137135, 110, 136fvmpt 6593 . . . . . . . . . . . . . . . . . 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 13189 . . . . . . . . . . . . . . . 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 11683 . . . . . . . . . . . . . . . . . . . 20 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14154, 123, 140sylancl 577 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14264, 141mpbid 224 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1)
143130, 142eqbrtrd 4949 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1)
144 logtayllem 24937 . . . . . . . . . . . . . . . . 17 (((((abs‘𝑦) + 1) / 2) ∈ ℂ ∧ (abs‘(((abs‘𝑦) + 1) / 2)) < 1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
145132, 143, 144syl2anc 576 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
146139, 145eqeltrd 2863 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝ )
14797, 131, 119, 132, 146radcnvle 24705 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
148130, 147eqbrtrrd 4951 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
14980, 84, 122, 126, 148xrltletrd 12368 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
150 0re 10437 . . . . . . . . . . . . 13 0 ∈ ℝ
151 elico2 12613 . . . . . . . . . . . . 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 578 . . . . . . . . . . . 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 1322 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
154 absf 14552 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
155 ffn 6342 . . . . . . . . . . . 12 (abs:ℂ⟶ℝ → abs Fn ℂ)
156 elpreima 6651 . . . . . . . . . . . 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 575 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
159 cnvimass 5787 . . . . . . . . . . . . . . . . 17 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
160154fdmi 6352 . . . . . . . . . . . . . . . . 17 dom abs = ℂ
161159, 160sseqtri 3892 . . . . . . . . . . . . . . . 16 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
162161sseli 3853 . . . . . . . . . . . . . . 15 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → 𝑦 ∈ ℂ)
163 oveq1 6981 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑥𝑗) = (𝑦𝑗))
164163oveq2d 6990 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
165164mpteq2dv 5021 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
166111mptex 6810 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) ∈ V
167165, 110, 166fvmpt 6593 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
168167adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
169168fveq1d 6499 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛))
170 eqeq1 2779 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0))
171 oveq2 6982 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛))
172170, 171ifbieq2d 4373 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛)))
173 oveq2 6982 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (𝑦𝑗) = (𝑦𝑛))
174172, 173oveq12d 6992 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
175 eqid 2775 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
176 ovex 7006 . . . . . . . . . . . . . . . . . . 19 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ V
177174, 175, 176fvmpt 6593 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
178177adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
179169, 178eqtr2d 2812 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
180179sumeq2dv 14914 . . . . . . . . . . . . . . 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 5016 . . . . . . . . . . . . 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 2775 . . . . . . . . . . . . 13 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
184 eqid 2775 . . . . . . . . . . . . 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 24711 . . . . . . . . . . . 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 23198 . . . . . . . . . . . 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 6698 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
189158, 188sylan2 583 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
190189fmpttd 6700 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
191 cnelprrecn 10424 . . . . . . . . . . . . 13 ℂ ∈ {ℝ, ℂ}
192191a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
19375adantl 474 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 − 𝑦)) ∈ ℂ)
194 ovexd 7008 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈ V)
19529cnmetdval 23076 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 − 𝑦) ∈ ℂ) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
19648, 53, 195sylancr 578 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
197 nncan 10712 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦)
19848, 51, 197sylancr 578 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦)
199198fveq2d 6501 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦))
200196, 199eqtrd 2811 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦))
201200, 64eqbrtrd 4949 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1)
202 elbl 22695 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1)))
20338, 48, 39, 202mp3an 1440 . . . . . . . . . . . . . . 15 ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1))
20453, 201, 203sylanbrc 575 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
205204adantl 474 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
206 neg1cn 11558 . . . . . . . . . . . . . 14 -1 ∈ ℂ
207206a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈ ℂ)
208 eqid 2775 . . . . . . . . . . . . . . . . . 18 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
209208dvlog2lem 24930 . . . . . . . . . . . . . . . . 17 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
210209sseli 3853 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ (ℂ ∖ (-∞(,]0)))
211210eldifad 3840 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ ℂ)
212 eqid 2775 . . . . . . . . . . . . . . . . 17 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
213212logdmn0 24918 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ≠ 0)
214210, 213syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ≠ 0)
215211, 214logcld 24849 . . . . . . . . . . . . . 14 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑥) ∈ ℂ)
216215adantl 474 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈ ℂ)
217 ovexd 7008 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V)
218 simpr 477 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
21948, 218, 52sylancr 578 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
220206a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → -1 ∈ ℂ)
221 1cnd 10430 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
222 0cnd 10428 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
223 1cnd 10430 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℂ)
224192, 223dvmptc 24252 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 1)) = (𝑦 ∈ ℂ ↦ 0))
225192dvmptid 24251 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
226192, 221, 222, 224, 218, 221, 225dvmptsub 24261 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 − 1)))
227 df-neg 10669 . . . . . . . . . . . . . . . 16 -1 = (0 − 1)
228227mpteq2i 5017 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ -1) = (𝑦 ∈ ℂ ↦ (0 − 1))
229226, 228syl6eqr 2829 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1))
23050a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
231 eqid 2775 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
232231cnfldtopon 23088 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
233232toponrestid 21227 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
234231cnfldtopn 23087 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
235234blopn 22807 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
23638, 28, 39, 235mp3an 1440 . . . . . . . . . . . . . . 15 (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld)
237236a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
238192, 219, 220, 229, 230, 233, 231, 237dvmptres 24257 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -1))
239208dvlog2 24931 . . . . . . . . . . . . . 14 (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥))
240 logf1o 24843 . . . . . . . . . . . . . . . . . . . 20 log:(ℂ ∖ {0})–1-1-onto→ran log
241 f1of 6442 . . . . . . . . . . . . . . . . . . . 20 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
242240, 241ax-mp 5 . . . . . . . . . . . . . . . . . . 19 log:(ℂ ∖ {0})⟶ran log
243212logdmss 24920 . . . . . . . . . . . . . . . . . . . 20 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
244209, 243sstri 3866 . . . . . . . . . . . . . . . . . . 19 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
245 fssres 6371 . . . . . . . . . . . . . . . . . . 19 ((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
246242, 244, 245mp2an 679 . . . . . . . . . . . . . . . . . 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 6560 . . . . . . . . . . . . . . . 16 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)))
249 fvres 6516 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥) = (log‘𝑥))
250249mpteq2ia 5016 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))
251248, 250syl6eq 2827 . . . . . . . . . . . . . . 15 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))
252251oveq2d 6990 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))))
253239, 252syl5reqr 2826 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥)))
254 fveq2 6497 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦)))
255 oveq2 6982 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦)))
256192, 192, 205, 207, 216, 217, 238, 253, 254, 255dvmptco 24266 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ ((1 / (1 − 𝑦)) · -1)))
257192, 193, 194, 256dvmptneg 24260 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)))
25853, 74reccld 11206 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ)
259 mulcom 10417 . . . . . . . . . . . . . . . 16 (((1 / (1 − 𝑦)) ∈ ℂ ∧ -1 ∈ ℂ) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
260258, 206, 259sylancl 577 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
261258mulm1d 10889 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦)))
262260, 261eqtrd 2811 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦)))
263262negeqd 10676 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦)))
264258negnegd 10785 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦)))
265263, 264eqtrd 2811 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦)))
266265mpteq2ia 5016 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
267257, 266syl6eq 2827 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
268267dmeqd 5621 . . . . . . . . 9 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
269 dmmptg 5933 . . . . . . . . . 10 (∀𝑦 ∈ (0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1))
270 ovexd 7008 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ V)
271269, 270mprg 3099 . . . . . . . . 9 dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1)
272268, 271syl6eq 2827 . . . . . . . 8 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (0(ball‘(abs ∘ − ))1))
273 sumex 14899 . . . . . . . . . . . 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 6497 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
276275cbvsumv 14907 . . . . . . . . . . . . . 14 Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘)
277181, 276syl6eq 2827 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
278277mpteq2ia 5016 . . . . . . . . . . . 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 2775 . . . . . . . . . . . 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 24715 . . . . . . . . . . 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 3861 . . . . . . . . . . . 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 24257 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
284 nnnn0 11712 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
285284adantl 474 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
286 eqeq1 2779 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0))
287 oveq2 6982 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
288286, 287ifbieq2d 4373 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛)))
289 ovex 7006 . . . . . . . . . . . . . . . . . . . . 21 (1 / 𝑛) ∈ V
29090, 289ifex 4396 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V
291288, 89, 290fvmpt 6593 . . . . . . . . . . . . . . . . . . 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 11471 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
294293adantl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
295294neneqd 2969 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
296295iffalsed 4359 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
297292, 296eqtrd 2811 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛))
298297oveq2d 6990 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛)))
299 nncn 11444 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
300299adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
301300, 294recidd 11208 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1)
302298, 301eqtrd 2811 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1)
303302oveq1d 6989 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1))))
304 nnm1nn0 11747 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
305 expcl 13259 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
30651, 304, 305syl2an 586 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
307306mulid2d 10454 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
308303, 307eqtrd 2811 . . . . . . . . . . . . 13 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
309308sumeq2dv 14914 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)))
310 nnuz 12092 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
311 1e0p1 11951 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
312311fveq2i 6500 . . . . . . . . . . . . . . 15 (ℤ‘1) = (ℤ‘(0 + 1))
313310, 312eqtri 2799 . . . . . . . . . . . . . 14 ℕ = (ℤ‘(0 + 1))
314 oveq1 6981 . . . . . . . . . . . . . . 15 (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1))
315314oveq2d 6990 . . . . . . . . . . . . . 14 (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1)))
316 1zzd 11823 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ∈ ℤ)
317 0zd 11802 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℤ)
3181, 313, 315, 316, 317, 306isumshft 15048 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)))
319 pncan2 10689 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚)
32048, 99, 319sylancr 578 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((1 + 𝑚) − 1) = 𝑚)
321320oveq2d 6990 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑦↑((1 + 𝑚) − 1)) = (𝑦𝑚))
322321sumeq2i 14910 . . . . . . . . . . . . 13 Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚)
323318, 322syl6eq 2827 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚))
324 geoisum 15087 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ (abs‘𝑦) < 1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
32551, 64, 324syl2anc 576 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
326309, 323, 3253eqtrd 2815 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦)))
327326mpteq2ia 5016 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
328283, 327syl6eq 2827 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
329267, 328eqtr4d 2814 . . . . . . . 8 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))))
330 1rp 12205 . . . . . . . . . 10 1 ∈ ℝ+
331 blcntr 22720 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘ − ))1))
33238, 28, 330, 331mp3an 1440 . . . . . . . . 9 0 ∈ (0(ball‘(abs ∘ − ))1)
333332a1i 11 . . . . . . . 8 (⊤ → 0 ∈ (0(ball‘(abs ∘ − ))1))
334 oveq2 6982 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (1 − 𝑦) = (1 − 0))
335 1m0e1 11565 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
336334, 335syl6eq 2827 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (1 − 𝑦) = 1)
337336fveq2d 6501 . . . . . . . . . . . . . 14 (𝑦 = 0 → (log‘(1 − 𝑦)) = (log‘1))
338 log1 24864 . . . . . . . . . . . . . 14 (log‘1) = 0
339337, 338syl6eq 2827 . . . . . . . . . . . . 13 (𝑦 = 0 → (log‘(1 − 𝑦)) = 0)
340339negeqd 10676 . . . . . . . . . . . 12 (𝑦 = 0 → -(log‘(1 − 𝑦)) = -0)
341 neg0 10729 . . . . . . . . . . . 12 -0 = 0
342340, 341syl6eq 2827 . . . . . . . . . . 11 (𝑦 = 0 → -(log‘(1 − 𝑦)) = 0)
343 eqid 2775 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))
344342, 343, 90fvmpt 6593 . . . . . . . . . 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 6981 . . . . . . . . . . . . . . 15 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
347346eqeq1d 2777 . . . . . . . . . . . . . 14 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
348 oveq1 6981 . . . . . . . . . . . . . . 15 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
349348eqeq1d 2777 . . . . . . . . . . . . . 14 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
350 simpll 754 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0)
351350, 28syl6eqel 2871 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ)
352 simplr 756 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0)
353351, 352expcld 13322 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦𝑛) ∈ ℂ)
354353mul02d 10634 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦𝑛)) = 0)
355 simpll 754 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑦 = 0)
356355oveq1d 6989 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = (0↑𝑛))
357 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
358357, 14sylib 210 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
359358ord 850 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
360359con1d 142 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
361360imp 398 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
3623610expd 13315 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (0↑𝑛) = 0)
363356, 362eqtrd 2811 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = 0)
364363oveq2d 6990 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = ((1 / 𝑛) · 0))
365361nnrecred 11488 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
366365recnd 10464 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
367366mul01d 10635 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · 0) = 0)
368364, 367eqtrd 2811 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = 0)
369347, 349, 354, 368ifbothda 4385 . . . . . . . . . . . . 13 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
370369sumeq2dv 14914 . . . . . . . . . . . 12 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 0)
3711eqimssi 3914 . . . . . . . . . . . . . 14 0 ⊆ (ℤ‘0)
372371orci 851 . . . . . . . . . . . . 13 (ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin)
373 sumz 14933 . . . . . . . . . . . . 13 ((ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 = 0)
374372, 373ax-mp 5 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ0 0 = 0
375370, 374syl6eq 2827 . . . . . . . . . . 11 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
376 eqid 2775 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
377375, 376, 90fvmpt 6593 . . . . . . . . . 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 2814 . . . . . . . 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 24295 . . . . . . 7 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))))
381380fveq1d 6499 . . . . . 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 6982 . . . . . . . 8 (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴))
384383fveq2d 6501 . . . . . . 7 (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴)))
385384negeqd 10676 . . . . . 6 (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 − 𝐴)))
386 negex 10680 . . . . . 6 -(log‘(1 − 𝐴)) ∈ V
387385, 343, 386fvmpt 6593 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴)))
388 oveq1 6981 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑛) = (𝐴𝑛))
389388oveq2d 6990 . . . . . . 7 (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
390389sumeq2sdv 14915 . . . . . 6 (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
391 sumex 14899 . . . . . 6 Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
392390, 376, 391fvmpt 6593 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
393382, 387, 3923eqtr3d 2819 . . . 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 4955 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)))
396 seqex 13183 . . . 4 seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V
397396a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V)
398 seqex 13183 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V
399398a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V)
400 1zzd 11823 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℤ)
401 elnnuz 12093 . . . . . 6 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
402 fvres 6516 . . . . . 6 (𝑛 ∈ (ℤ‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
403401, 402sylbi 209 . . . . 5 (𝑛 ∈ ℕ → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
404403eqcomd 2781 . . . 4 (𝑛 ∈ ℕ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛))
405 addid2 10619 . . . . . . . 8 (𝑛 ∈ ℂ → (0 + 𝑛) = 𝑛)
406405adantl 474 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℂ) → (0 + 𝑛) = 𝑛)
407 0cnd 10428 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℂ)
408 1eluzge0 12103 . . . . . . . 8 1 ∈ (ℤ‘0)
409408a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ (ℤ‘0))
410 0cnd 10428 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
411 nn0cn 11715 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
412411adantl 474 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
413 neqne 2972 . . . . . . . . . . . 12 𝑘 = 0 → 𝑘 ≠ 0)
414 reccl 11102 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
415412, 413, 414syl2an 586 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
416410, 415ifclda 4382 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
417 expcl 13259 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
418417adantlr 702 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
419416, 418mulcld 10456 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
420419fmpttd 6700 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ)
421 1nn0 11722 . . . . . . . 8 1 ∈ ℕ0
422 ffvelrn 6672 . . . . . . . 8 (((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
423420, 421, 422sylancl 577 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
424 elfz1eq 12731 . . . . . . . . . 10 (𝑛 ∈ (0...0) → 𝑛 = 0)
425 1m1e0 11509 . . . . . . . . . . 11 (1 − 1) = 0
426425oveq2i 6985 . . . . . . . . . 10 (0...(1 − 1)) = (0...0)
427424, 426eleq2s 2881 . . . . . . . . 9 (𝑛 ∈ (0...(1 − 1)) → 𝑛 = 0)
428427fveq2d 6501 . . . . . . . 8 (𝑛 ∈ (0...(1 − 1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0))
429 0nn0 11721 . . . . . . . . . 10 0 ∈ ℕ0
430 iftrue 4354 . . . . . . . . . . . 12 (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0)
431 oveq2 6982 . . . . . . . . . . . 12 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
432430, 431oveq12d 6992 . . . . . . . . . . 11 (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (0 · (𝐴↑0)))
433 ovex 7006 . . . . . . . . . . 11 (0 · (𝐴↑0)) ∈ V
434432, 8, 433fvmpt 6593 . . . . . . . . . 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 13259 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝐴↑0) ∈ ℂ)
43727, 429, 436sylancl 577 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴↑0) ∈ ℂ)
438437mul02d 10634 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (0 · (𝐴↑0)) = 0)
439435, 438syl5eq 2823 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = 0)
440428, 439sylan9eqr 2833 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (0...(1 − 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = 0)
441406, 407, 409, 423, 440seqid 13227 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))))
442293adantl 474 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
443442neneqd 2969 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
444443iffalsed 4359 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
445444oveq1d 6989 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((1 / 𝑛) · (𝐴𝑛)))
446284, 23sylan2 583 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ ℂ)
447299adantl 474 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
448446, 447, 442divrec2d 11217 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴𝑛)))
449445, 448eqtr4d 2814 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((𝐴𝑛) / 𝑛))
450284, 11sylan2 583 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
451 id 22 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑘 = 𝑛)
4526, 451oveq12d 6992 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) / 𝑘) = ((𝐴𝑛) / 𝑛))
453 eqid 2775 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))
454 ovex 7006 . . . . . . . . . . 11 ((𝐴𝑛) / 𝑛) ∈ V
455452, 453, 454fvmpt 6593 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
456455adantl 474 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
457449, 450, 4563eqtr4d 2821 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
458401, 457sylan2br 585 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
459400, 458seqfeq 13207 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
460441, 459eqtrd 2811 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
461460fveq1d 6499 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
462404, 461sylan9eqr 2833 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
463310, 397, 399, 400, 462climeq 14779 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))))
464395, 463mpbid 224 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 833  w3a 1068   = wceq 1507  wtru 1508  wcel 2048  wne 2964  {crab 3089  Vcvv 3412  cdif 3825  wss 3828  ifcif 4348  {csn 4439  {cpr 4441   class class class wbr 4927  cmpt 5006  ccnv 5403  dom cdm 5404  ran crn 5405  cres 5406  cima 5407  ccom 5408   Fn wfn 6181  wf 6182  1-1-ontowf1o 6185  cfv 6186  (class class class)co 6974  Fincfn 8302  supcsup 8695  cc 10329  cr 10330  0cc0 10331  1c1 10332   + caddc 10334   · cmul 10336  +∞cpnf 10467  -∞cmnf 10468  *cxr 10469   < clt 10470  cle 10471  cmin 10666  -cneg 10667   / cdiv 11094  cn 11435  2c2 11492  0cn0 11704  cuz 12055  +crp 12201  (,]cioc 12552  [,)cico 12553  [,]cicc 12554  ...cfz 12705  seqcseq 13181  cexp 13241  abscabs 14448  cli 14696  Σcsu 14897  TopOpenctopn 16545  ∞Metcxmet 20226  ballcbl 20228  fldccnfld 20241  cnccncf 23181   D cdv 24158  logclog 24833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-inf2 8894  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409  ax-addf 10410  ax-mulf 10411
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-int 4748  df-iun 4792  df-iin 4793  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-om 7395  df-1st 7498  df-2nd 7499  df-supp 7631  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-1o 7901  df-2o 7902  df-oadd 7905  df-er 8085  df-map 8204  df-pm 8205  df-ixp 8256  df-en 8303  df-dom 8304  df-sdom 8305  df-fin 8306  df-fsupp 8625  df-fi 8666  df-sup 8697  df-inf 8698  df-oi 8765  df-card 9158  df-cda 9384  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-div 11095  df-nn 11436  df-2 11500  df-3 11501  df-4 11502  df-5 11503  df-6 11504  df-7 11505  df-8 11506  df-9 11507  df-n0 11705  df-z 11791  df-dec 11909  df-uz 12056  df-q 12160  df-rp 12202  df-xneg 12321  df-xadd 12322  df-xmul 12323  df-ioo 12555  df-ioc 12556  df-ico 12557  df-icc 12558  df-fz 12706  df-fzo 12847  df-fl 12974  df-mod 13050  df-seq 13182  df-exp 13242  df-fac 13446  df-bc 13475  df-hash 13503  df-shft 14281  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-limsup 14683  df-clim 14700  df-rlim 14701  df-sum 14898  df-ef 15275  df-sin 15277  df-cos 15278  df-tan 15279  df-pi 15280  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-starv 16430  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-unif 16438  df-hom 16439  df-cco 16440  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-pt 16568  df-prds 16571  df-xrs 16625  df-qtop 16630  df-imas 16631  df-xps 16633  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-mulg 18006  df-cntz 18212  df-cmn 18662  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-fbas 20238  df-fg 20239  df-cnfld 20242  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-perf 21443  df-cn 21533  df-cnp 21534  df-haus 21621  df-cmp 21693  df-tx 21868  df-hmeo 22061  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-xms 22627  df-ms 22628  df-tms 22629  df-cncf 23183  df-limc 24161  df-dv 24162  df-ulm 24662  df-log 24835
This theorem is referenced by:  logtaylsum  24939  logtayl2  24940  atantayl  25210  stirlinglem5  41773
  Copyright terms: Public domain W3C validator