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

Theorem logtayl 24151
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 11557 . . . 4 0 = (ℤ‘0)
2 0zd 11225 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℤ)
3 eqeq1 2613 . . . . . . . 8 (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0))
4 oveq2 6535 . . . . . . . 8 (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛))
53, 4ifbieq2d 4060 . . . . . . 7 (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛)))
6 oveq2 6535 . . . . . . 7 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
75, 6oveq12d 6545 . . . . . 6 (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
8 eqid 2609 . . . . . 6 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
9 ovex 6555 . . . . . 6 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
107, 8, 9fvmpt 6176 . . . . 5 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
1110adantl 480 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
12 0cnd 9890 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 0 ∈ ℂ)
13 simpr 475 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
14 elnn0 11144 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↔ (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1513, 14sylib 206 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
1615ord 390 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
1716con1d 137 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
1817imp 443 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
1918nnrecred 10916 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
2019recnd 9925 . . . . . 6 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
2112, 20ifclda 4069 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ)
22 expcl 12698 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2322adantlr 746 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2421, 23mulcld 9917 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ ℂ)
25 logtayllem 24150 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ dom ⇝ )
261, 2, 11, 24, 25isumclim2 14280 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
27 simpl 471 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
28 0cn 9889 . . . . . . . 8 0 ∈ ℂ
29 eqid 2609 . . . . . . . . 9 (abs ∘ − ) = (abs ∘ − )
3029cnmetdval 22332 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
3127, 28, 30sylancl 692 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘(𝐴 − 0)))
32 subid1 10153 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3332adantr 479 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 − 0) = 𝐴)
3433fveq2d 6092 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(𝐴 − 0)) = (abs‘𝐴))
3531, 34eqtrd 2643 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) = (abs‘𝐴))
36 simpr 475 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3735, 36eqbrtrd 4599 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴(abs ∘ − )0) < 1)
38 cnxmet 22334 . . . . . . 7 (abs ∘ − ) ∈ (∞Met‘ℂ)
39 1rp 11671 . . . . . . . 8 1 ∈ ℝ+
40 rpxr 11675 . . . . . . . 8 (1 ∈ ℝ+ → 1 ∈ ℝ*)
4139, 40ax-mp 5 . . . . . . 7 1 ∈ ℝ*
42 elbl3 21955 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4338, 41, 42mpanl12 713 . . . . . 6 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4428, 27, 43sylancr 693 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) < 1))
4537, 44mpbird 245 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ (0(ball‘(abs ∘ − ))1))
46 tru 1478 . . . . . 6
47 eqid 2609 . . . . . . . 8 (0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘ − ))1)
48 0cnd 9890 . . . . . . . 8 (⊤ → 0 ∈ ℂ)
4941a1i 11 . . . . . . . 8 (⊤ → 1 ∈ ℝ*)
50 ax-1cn 9851 . . . . . . . . . . . . 13 1 ∈ ℂ
51 blssm 21981 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
5238, 28, 41, 51mp3an 1415 . . . . . . . . . . . . . 14 (0(ball‘(abs ∘ − ))1) ⊆ ℂ
5352sseli 3563 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ ℂ)
54 subcl 10132 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
5550, 53, 54sylancr 693 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ ℂ)
5653abscld 13972 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ)
5729cnmetdval 22332 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5853, 28, 57sylancl 692 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0)))
5953subid1d 10233 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 − 0) = 𝑦)
6059fveq2d 6092 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦))
6158, 60eqtrd 2643 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦))
62 elbl3 21955 . . . . . . . . . . . . . . . . . . 19 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6338, 41, 62mpanl12 713 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6428, 53, 63sylancr 693 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) < 1))
6564ibi 254 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (𝑦(abs ∘ − )0) < 1)
6661, 65eqbrtrrd 4601 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < 1)
6756, 66gtned 10024 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ (abs‘𝑦))
68 abs1 13834 . . . . . . . . . . . . . . . 16 (abs‘1) = 1
69 fveq2 6088 . . . . . . . . . . . . . . . 16 (1 = 𝑦 → (abs‘1) = (abs‘𝑦))
7068, 69syl5eqr 2657 . . . . . . . . . . . . . . 15 (1 = 𝑦 → 1 = (abs‘𝑦))
7170necon3i 2813 . . . . . . . . . . . . . 14 (1 ≠ (abs‘𝑦) → 1 ≠ 𝑦)
7267, 71syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ≠ 𝑦)
73 subeq0 10159 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦))
7473necon3bid 2825 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7550, 53, 74sylancr 693 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦))
7672, 75mpbird 245 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ≠ 0)
7755, 76logcld 24066 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ)
7877negcld 10231 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ)
7978adantl 480 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 − 𝑦)) ∈ ℂ)
80 eqid 2609 . . . . . . . . 9 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))
8179, 80fmptd 6277 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
8253absge0d 13980 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (abs‘𝑦))
8356rexrd 9946 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ ℝ*)
84 peano2re 10061 . . . . . . . . . . . . . . . 16 ((abs‘𝑦) ∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ)
8556, 84syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ)
8685rehalfcld 11129 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ)
8786rexrd 9946 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ*)
88 iccssxr 12086 . . . . . . . . . . . . . . 15 (0[,]+∞) ⊆ ℝ*
89 eqeq1 2613 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0))
90 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
9189, 90ifbieq2d 4060 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗)))
92 eqid 2609 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))
93 c0ex 9891 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
94 ovex 6555 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 𝑗) ∈ V
9593, 94ifex 4105 . . . . . . . . . . . . . . . . . . . . 21 if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V
9691, 92, 95fvmpt 6176 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗)))
9796eqcomd 2615 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → if(𝑗 = 0, 0, (1 / 𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗))
9897oveq1d 6542 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
9998mpteq2ia 4662 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗)))
10099mpteq2i 4663 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥𝑗))))
101 0cnd 9890 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈ ℂ)
102 nn0cn 11152 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
103102adantl 480 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
104 df-ne 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ≠ 0 ↔ ¬ 𝑚 = 0)
105104biimpri 216 . . . . . . . . . . . . . . . . . . 19 𝑚 = 0 → 𝑚 ≠ 0)
106 reccl 10544 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈ ℂ)
107103, 105, 106syl2an 492 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑚 ∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ)
108101, 107ifclda 4069 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑚 ∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ)
109108, 92fmptd 6277 . . . . . . . . . . . . . . . 16 (⊤ → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ)
110 recn 9883 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ → 𝑟 ∈ ℂ)
111 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑟 → (𝑥𝑗) = (𝑟𝑗))
112111oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))
113112mpteq2dv 4667 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))))
114 eqid 2609 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))
115 nn0ex 11148 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
116115mptex 6368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) ∈ V
117113, 114, 116fvmpt 6176 . . . . . . . . . . . . . . . . . . . . . 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 2615 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟))
120119seqeq3d 12629 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)))
121120eleq1d 2671 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ → (seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ ↔ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ ))
122121rabbiia 3160 . . . . . . . . . . . . . . . . 17 {𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }
123122supeq1i 8214 . . . . . . . . . . . . . . . 16 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
124100, 109, 123radcnvcl 23920 . . . . . . . . . . . . . . 15 (⊤ → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
12588, 124sseldi 3565 . . . . . . . . . . . . . 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 9896 . . . . . . . . . . . . . . 15 1 ∈ ℝ
128 avglt1 11120 . . . . . . . . . . . . . . 15 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
12956, 127, 128sylancl 692 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)))
13066, 129mpbid 220 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))
131 0red 9898 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℝ)
132131, 56, 86, 82, 130lelttrd 10047 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2))
133131, 86, 132ltled 10037 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2))
13486, 133absidd 13958 . . . . . . . . . . . . . 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 9925 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ)
137 oveq1 6534 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗))
138137oveq2d 6543 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))
139138mpteq2dv 4667 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))
140115mptex 6368 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) ∈ V
141139, 114, 140fvmpt 6176 . . . . . . . . . . . . . . . . . 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 12629 . . . . . . . . . . . . . . . 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 11121 . . . . . . . . . . . . . . . . . . . 20 (((abs‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14556, 127, 144sylancl 692 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) < 1))
14666, 145mpbid 220 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1)
147134, 146eqbrtrd 4599 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1)
148 logtayllem 24150 . . . . . . . . . . . . . . . . 17 (((((abs‘𝑦) + 1) / 2) ∈ ℂ ∧ (abs‘(((abs‘𝑦) + 1) / 2)) < 1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
149136, 147, 148syl2anc 690 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ )
150143, 149eqeltrd 2687 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝ )
151100, 135, 123, 136, 150radcnvle 23923 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
152134, 151eqbrtrrd 4601 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
15383, 87, 126, 130, 152xrltletrd 11830 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))
154 0re 9897 . . . . . . . . . . . . 13 0 ∈ ℝ
155 elico2 12067 . . . . . . . . . . . . 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 693 . . . . . . . . . . . 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 1237 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
158 absf 13874 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
159 ffn 5944 . . . . . . . . . . . 12 (abs:ℂ⟶ℝ → abs Fn ℂ)
160 elpreima 6230 . . . . . . . . . . . 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 694 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
163 cnvimass 5391 . . . . . . . . . . . . . . . . . 18 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
164158fdmi 5951 . . . . . . . . . . . . . . . . . 18 dom abs = ℂ
165163, 164sseqtri 3599 . . . . . . . . . . . . . . . . 17 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
166165sseli 3563 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → 𝑦 ∈ ℂ)
167 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝑥𝑗) = (𝑦𝑗))
168167oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
169168mpteq2dv 4667 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
170115mptex 6368 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) ∈ V
171169, 114, 170fvmpt 6176 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
172171adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))))
173172fveq1d 6090 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛))
174 eqeq1 2613 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0))
175 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛))
176174, 175ifbieq2d 4060 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛)))
177 oveq2 6535 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → (𝑦𝑗) = (𝑦𝑛))
178176, 177oveq12d 6545 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
179 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))
180 ovex 6555 . . . . . . . . . . . . . . . . . . . 20 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ V
181178, 179, 180fvmpt 6176 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
182181adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
183173, 182eqtr2d 2644 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛))
184183sumeq2dv 14230 . . . . . . . . . . . . . . . 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 4662 . . . . . . . . . . . . . 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 2609 . . . . . . . . . . . . . 14 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
188 eqid 2609 . . . . . . . . . . . . . 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 23929 . . . . . . . . . . . . 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 22452 . . . . . . . . . . . . 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 2609 . . . . . . . . . . . . 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 6274 . . . . . . . . . . . 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 222 . . . . . . . . . . 11 (⊤ → ∀𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
195194r19.21bi 2915 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
196162, 195sylan2 489 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) ∈ ℂ)
197 eqid 2609 . . . . . . . . 9 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
198196, 197fmptd 6277 . . . . . . . 8 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))):(0(ball‘(abs ∘ − ))1)⟶ℂ)
199 cnelprrecn 9886 . . . . . . . . . . . . 13 ℂ ∈ {ℝ, ℂ}
200199a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
20177adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 − 𝑦)) ∈ ℂ)
202 ovex 6555 . . . . . . . . . . . . 13 ((1 / (1 − 𝑦)) · -1) ∈ V
203202a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈ V)
20429cnmetdval 22332 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 − 𝑦) ∈ ℂ) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
20550, 55, 204sylancr 693 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1 − 𝑦))))
206 nncan 10162 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦)
20750, 53, 206sylancr 693 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦)
208207fveq2d 6092 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦))
209205, 208eqtrd 2643 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦))
210209, 66eqbrtrd 4599 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1)
211 elbl 21951 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1)))
21238, 50, 41, 211mp3an 1415 . . . . . . . . . . . . . . 15 ((1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1))
21355, 210, 212sylanbrc 694 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
214213adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ − ))1))
215 neg1cn 10974 . . . . . . . . . . . . . 14 -1 ∈ ℂ
216215a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈ ℂ)
217 eqid 2609 . . . . . . . . . . . . . . . . . 18 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
218217dvlog2lem 24143 . . . . . . . . . . . . . . . . 17 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
219218sseli 3563 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ (ℂ ∖ (-∞(,]0)))
220219eldifad 3551 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ∈ ℂ)
221 eqid 2609 . . . . . . . . . . . . . . . . 17 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
222221logdmn0 24131 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ≠ 0)
223219, 222syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → 𝑥 ≠ 0)
224220, 223logcld 24066 . . . . . . . . . . . . . 14 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑥) ∈ ℂ)
225224adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈ ℂ)
226 ovex 6555 . . . . . . . . . . . . . 14 (1 / 𝑥) ∈ V
227226a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V)
228 simpr 475 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
22950, 228, 54sylancr 693 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
230215a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑦 ∈ ℂ) → -1 ∈ ℂ)
231 1cnd 9913 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
232 0cnd 9890 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
233 1cnd 9913 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℂ)
234200, 233dvmptc 23472 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 1)) = (𝑦 ∈ ℂ ↦ 0))
235200dvmptid 23471 . . . . . . . . . . . . . . . 16 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
236200, 231, 232, 234, 228, 231, 235dvmptsub 23481 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 − 1)))
237 df-neg 10121 . . . . . . . . . . . . . . . 16 -1 = (0 − 1)
238237mpteq2i 4663 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ -1) = (𝑦 ∈ ℂ ↦ (0 − 1))
239236, 238syl6eqr 2661 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1))
24052a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
241 eqid 2609 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
242241cnfldtop 22345 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) ∈ Top
243241cnfldtopon 22344 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
244243toponunii 20495 . . . . . . . . . . . . . . . . 17 ℂ = (TopOpen‘ℂfld)
245244restid 15866 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
246242, 245ax-mp 5 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
247246eqcomi 2618 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
248241cnfldtopn 22343 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
249248blopn 22063 . . . . . . . . . . . . . . . 16 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
25038, 28, 41, 249mp3an 1415 . . . . . . . . . . . . . . 15 (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld)
251250a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(ball‘(abs ∘ − ))1) ∈ (TopOpen‘ℂfld))
252200, 229, 230, 239, 240, 247, 241, 251dvmptres 23477 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -1))
253217dvlog2 24144 . . . . . . . . . . . . . 14 (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥))
254 logf1o 24060 . . . . . . . . . . . . . . . . . . . 20 log:(ℂ ∖ {0})–1-1-onto→ran log
255 f1of 6035 . . . . . . . . . . . . . . . . . . . 20 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
256254, 255ax-mp 5 . . . . . . . . . . . . . . . . . . 19 log:(ℂ ∖ {0})⟶ran log
257221logdmss 24133 . . . . . . . . . . . . . . . . . . . 20 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
258218, 257sstri 3576 . . . . . . . . . . . . . . . . . . 19 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
259 fssres 5968 . . . . . . . . . . . . . . . . . . 19 ((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
260256, 258, 259mp2an 703 . . . . . . . . . . . . . . . . . 18 (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log
261260a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ran log)
262261feqmptd 6144 . . . . . . . . . . . . . . . 16 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)))
263 fvres 6102 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥) = (log‘𝑥))
264263mpteq2ia 4662 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))
265262, 264syl6eq 2659 . . . . . . . . . . . . . . 15 (⊤ → (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))
266265oveq2d 6543 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))))
267253, 266syl5reqr 2658 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑥)))
268 fveq2 6088 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦)))
269 oveq2 6535 . . . . . . . . . . . . 13 (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦)))
270200, 200, 214, 216, 225, 227, 252, 267, 268, 269dvmptco 23486 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ ((1 / (1 − 𝑦)) · -1)))
271200, 201, 203, 270dvmptneg 23480 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)))
27255, 76reccld 10646 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ)
273 mulcom 9879 . . . . . . . . . . . . . . . 16 (((1 / (1 − 𝑦)) ∈ ℂ ∧ -1 ∈ ℂ) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
274272, 215, 273sylancl 692 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1 − 𝑦))))
275272mulm1d 10334 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦)))
276274, 275eqtrd 2643 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦)))
277276negeqd 10127 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦)))
278272negnegd 10235 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦)))
279277, 278eqtrd 2643 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦)))
280279mpteq2ia 4662 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
281271, 280syl6eq 2659 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
282281dmeqd 5235 . . . . . . . . 9 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
283 dmmptg 5535 . . . . . . . . . 10 (∀𝑦 ∈ (0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1))
284 ovex 6555 . . . . . . . . . . 11 (1 / (1 − 𝑦)) ∈ V
285284a1i 11 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → (1 / (1 − 𝑦)) ∈ V)
286283, 285mprg 2909 . . . . . . . . 9 dom (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ − ))1)
287282, 286syl6eq 2659 . . . . . . . 8 (⊤ → dom (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (0(ball‘(abs ∘ − ))1))
288 sumex 14215 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V
289288a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V)
290 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
291290cbvsumv 14223 . . . . . . . . . . . . . 14 Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘)
292185, 291syl6eq 2659 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
293292mpteq2ia 4662 . . . . . . . . . . . 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 / 𝑗)) · (𝑥𝑗))))‘𝑦)‘𝑘))
294 eqid 2609 . . . . . . . . . . . 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))
295100, 293, 109, 123, 187, 188, 294pserdv2 23933 . . . . . . . . . . 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)))))
296162ssriv 3571 . . . . . . . . . . . 12 (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < )))
297296a1i 11 . . . . . . . . . . 11 (⊤ → (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟𝑗)))) ∈ dom ⇝ }, ℝ*, < ))))
298200, 195, 289, 295, 297, 247, 241, 251dvmptres 23477 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))))
299 nnnn0 11149 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
300299adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
301 eqeq1 2613 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0))
302 oveq2 6535 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
303301, 302ifbieq2d 4060 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛)))
304 ovex 6555 . . . . . . . . . . . . . . . . . . . . 21 (1 / 𝑛) ∈ V
30593, 304ifex 4105 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V
306303, 92, 305fvmpt 6176 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
307300, 306syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)))
308 nnne0 10903 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
309308adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
310309neneqd 2786 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
311310iffalsed 4046 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
312307, 311eqtrd 2643 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛))
313312oveq2d 6543 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛)))
314 nncn 10878 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
315314adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
316315, 309recidd 10648 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1)
317313, 316eqtrd 2643 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1)
318317oveq1d 6542 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1))))
319 nnm1nn0 11184 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
320 expcl 12698 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
32153, 319, 320syl2an 492 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ)
322321mulid2d 9915 . . . . . . . . . . . . . 14 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
323318, 322eqtrd 2643 . . . . . . . . . . . . 13 ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1)))
324323sumeq2dv 14230 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)))
325 nnuz 11558 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
326 1e0p1 11387 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
327326fveq2i 6091 . . . . . . . . . . . . . . 15 (ℤ‘1) = (ℤ‘(0 + 1))
328325, 327eqtri 2631 . . . . . . . . . . . . . 14 ℕ = (ℤ‘(0 + 1))
329 oveq1 6534 . . . . . . . . . . . . . . 15 (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1))
330329oveq2d 6543 . . . . . . . . . . . . . 14 (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1)))
331 1zzd 11244 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 1 ∈ ℤ)
332 0zd 11225 . . . . . . . . . . . . . 14 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → 0 ∈ ℤ)
3331, 328, 330, 331, 332, 321isumshft 14359 . . . . . . . . . . . . 13 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)))
334 pncan2 10140 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚)
33550, 102, 334sylancr 693 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((1 + 𝑚) − 1) = 𝑚)
336335oveq2d 6543 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑦↑((1 + 𝑚) − 1)) = (𝑦𝑚))
337336sumeq2i 14226 . . . . . . . . . . . . 13 Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚)
338333, 337syl6eq 2659 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦𝑚))
339 geoisum 14396 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ (abs‘𝑦) < 1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
34053, 66, 339syl2anc 690 . . . . . . . . . . . 12 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦𝑚) = (1 / (1 − 𝑦)))
341324, 338, 3403eqtrd 2647 . . . . . . . . . . 11 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦)))
342341mpteq2ia 4662 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦)))
343298, 342syl6eq 2659 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))))
344281, 343eqtr4d 2646 . . . . . . . 8 (⊤ → (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))))
345 blcntr 21976 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘ − ))1))
34638, 28, 39, 345mp3an 1415 . . . . . . . . 9 0 ∈ (0(ball‘(abs ∘ − ))1)
347346a1i 11 . . . . . . . 8 (⊤ → 0 ∈ (0(ball‘(abs ∘ − ))1))
348 oveq2 6535 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (1 − 𝑦) = (1 − 0))
349 1m0e1 10981 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
350348, 349syl6eq 2659 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (1 − 𝑦) = 1)
351350fveq2d 6092 . . . . . . . . . . . . . 14 (𝑦 = 0 → (log‘(1 − 𝑦)) = (log‘1))
352 log1 24081 . . . . . . . . . . . . . 14 (log‘1) = 0
353351, 352syl6eq 2659 . . . . . . . . . . . . 13 (𝑦 = 0 → (log‘(1 − 𝑦)) = 0)
354353negeqd 10127 . . . . . . . . . . . 12 (𝑦 = 0 → -(log‘(1 − 𝑦)) = -0)
355 neg0 10179 . . . . . . . . . . . 12 -0 = 0
356354, 355syl6eq 2659 . . . . . . . . . . 11 (𝑦 = 0 → -(log‘(1 − 𝑦)) = 0)
357356, 80, 93fvmpt 6176 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
358346, 357mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0)
359 oveq1 6534 . . . . . . . . . . . . . . 15 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
360359eqeq1d 2611 . . . . . . . . . . . . . 14 (0 = if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
361 oveq1 6534 . . . . . . . . . . . . . . 15 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))
362361eqeq1d 2611 . . . . . . . . . . . . . 14 ((1 / 𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0))
363 simpll 785 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0)
364363, 28syl6eqel 2695 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ)
365 simplr 787 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0)
366364, 365expcld 12828 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦𝑛) ∈ ℂ)
367366mul02d 10086 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦𝑛)) = 0)
368 simpll 785 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑦 = 0)
369368oveq1d 6542 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = (0↑𝑛))
370 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
371370, 14sylib 206 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0))
372371ord 390 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0))
373372con1d 137 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ))
374373imp 443 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
3753740expd 12844 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (0↑𝑛) = 0)
376369, 375eqtrd 2643 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑦𝑛) = 0)
377376oveq2d 6543 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = ((1 / 𝑛) · 0))
378374nnrecred 10916 . . . . . . . . . . . . . . . . 17 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ)
379378recnd 9925 . . . . . . . . . . . . . . . 16 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ)
380379mul01d 10087 . . . . . . . . . . . . . . 15 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · 0) = 0)
381377, 380eqtrd 2643 . . . . . . . . . . . . . 14 (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((1 / 𝑛) · (𝑦𝑛)) = 0)
382360, 362, 367, 381ifbothda 4072 . . . . . . . . . . . . 13 ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
383382sumeq2dv 14230 . . . . . . . . . . . 12 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 0)
3841eqimssi 3621 . . . . . . . . . . . . . 14 0 ⊆ (ℤ‘0)
385384orci 403 . . . . . . . . . . . . 13 (ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin)
386 sumz 14249 . . . . . . . . . . . . 13 ((ℕ0 ⊆ (ℤ‘0) ∨ ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 = 0)
387385, 386ax-mp 5 . . . . . . . . . . . 12 Σ𝑛 ∈ ℕ0 0 = 0
388383, 387syl6eq 2659 . . . . . . . . . . 11 (𝑦 = 0 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = 0)
389388, 197, 93fvmpt 6176 . . . . . . . . . 10 (0 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
390346, 389mp1i 13 . . . . . . . . 9 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0) = 0)
391358, 390eqtr4d 2646 . . . . . . . 8 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘0))
39247, 48, 49, 81, 198, 287, 344, 347, 391dv11cn 23513 . . . . . . 7 (⊤ → (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛))))
393392fveq1d 6090 . . . . . 6 (⊤ → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
39446, 393mp1i 13 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴))
395 oveq2 6535 . . . . . . . 8 (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴))
396395fveq2d 6092 . . . . . . 7 (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴)))
397396negeqd 10127 . . . . . 6 (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 − 𝐴)))
398 negex 10131 . . . . . 6 -(log‘(1 − 𝐴)) ∈ V
399397, 80, 398fvmpt 6176 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴)))
400 oveq1 6534 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑛) = (𝐴𝑛))
401400oveq2d 6543 . . . . . . 7 (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
402401sumeq2sdv 14231 . . . . . 6 (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
403 sumex 14215 . . . . . 6 Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) ∈ V
404402, 197, 403fvmpt 6176 . . . . 5 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
405394, 399, 4043eqtr3d 2651 . . . 4 (𝐴 ∈ (0(ball‘(abs ∘ − ))1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
40645, 405syl 17 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
40726, 406breqtrrd 4605 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)))
408 seqex 12623 . . . 4 seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V
409408a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ∈ V)
410 seqex 12623 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V
411410a1i 11 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ∈ V)
412 1zzd 11244 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℤ)
413 elnnuz 11559 . . . . . 6 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
414 fvres 6102 . . . . . 6 (𝑛 ∈ (ℤ‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
415413, 414sylbi 205 . . . . 5 (𝑛 ∈ ℕ → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛))
416415eqcomd 2615 . . . 4 (𝑛 ∈ ℕ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛))
417 addid2 10071 . . . . . . . 8 (𝑛 ∈ ℂ → (0 + 𝑛) = 𝑛)
418417adantl 480 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℂ) → (0 + 𝑛) = 𝑛)
419 0cnd 9890 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 0 ∈ ℂ)
420 1eluzge0 11567 . . . . . . . 8 1 ∈ (ℤ‘0)
421420a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ (ℤ‘0))
422 0cnd 9890 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
423 nn0cn 11152 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
424423adantl 480 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
425 df-ne 2781 . . . . . . . . . . . . 13 (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0)
426425biimpri 216 . . . . . . . . . . . 12 𝑘 = 0 → 𝑘 ≠ 0)
427 reccl 10544 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
428424, 426, 427syl2an 492 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
429422, 428ifclda 4069 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
430 expcl 12698 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
431430adantlr 746 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
432429, 431mulcld 9917 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
433432, 8fmptd 6277 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ)
434 1nn0 11158 . . . . . . . 8 1 ∈ ℕ0
435 ffvelrn 6250 . . . . . . . 8 (((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
436433, 434, 435sylancl 692 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘1) ∈ ℂ)
437 elfz1eq 12181 . . . . . . . . . 10 (𝑛 ∈ (0...0) → 𝑛 = 0)
438 1m1e0 10939 . . . . . . . . . . 11 (1 − 1) = 0
439438oveq2i 6538 . . . . . . . . . 10 (0...(1 − 1)) = (0...0)
440437, 439eleq2s 2705 . . . . . . . . 9 (𝑛 ∈ (0...(1 − 1)) → 𝑛 = 0)
441440fveq2d 6092 . . . . . . . 8 (𝑛 ∈ (0...(1 − 1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0))
442 0nn0 11157 . . . . . . . . . 10 0 ∈ ℕ0
443 iftrue 4041 . . . . . . . . . . . 12 (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0)
444 oveq2 6535 . . . . . . . . . . . 12 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
445443, 444oveq12d 6545 . . . . . . . . . . 11 (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = (0 · (𝐴↑0)))
446 ovex 6555 . . . . . . . . . . 11 (0 · (𝐴↑0)) ∈ V
447445, 8, 446fvmpt 6176 . . . . . . . . . 10 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0)))
448442, 447ax-mp 5 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = (0 · (𝐴↑0))
449 expcl 12698 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝐴↑0) ∈ ℂ)
45027, 442, 449sylancl 692 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (𝐴↑0) ∈ ℂ)
451450mul02d 10086 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (0 · (𝐴↑0)) = 0)
452448, 451syl5eq 2655 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘0) = 0)
453441, 452sylan9eqr 2665 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (0...(1 − 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = 0)
454418, 419, 421, 436, 453seqid 12666 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))))
455308adantl 480 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
456455neneqd 2786 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
457456iffalsed 4046 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛))
458457oveq1d 6542 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((1 / 𝑛) · (𝐴𝑛)))
459299, 23sylan2 489 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ ℂ)
460314adantl 480 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
461459, 460, 455divrec2d 10657 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴𝑛)))
462458, 461eqtr4d 2646 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = ((𝐴𝑛) / 𝑛))
463299, 11sylan2 489 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
464 id 22 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑘 = 𝑛)
4656, 464oveq12d 6545 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) / 𝑘) = ((𝐴𝑛) / 𝑛))
466 eqid 2609 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))
467 ovex 6555 . . . . . . . . . . 11 ((𝐴𝑛) / 𝑛) ∈ V
468465, 466, 467fvmpt 6176 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
469468adantl 480 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛) = ((𝐴𝑛) / 𝑛))
470462, 463, 4693eqtr4d 2653 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
471413, 470sylan2br 491 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))‘𝑛))
472412, 471seqfeq 12646 . . . . . 6 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
473454, 472eqtrd 2643 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))))
474473fveq1d 6090 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ↾ (ℤ‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
475416, 474sylan9eqr 2665 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑛 ∈ ℕ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘)))‘𝑛))
476325, 409, 411, 412, 475climeq 14095 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))))
477407, 476mpbid 220 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wtru 1475  wcel 1976  wne 2779  wral 2895  {crab 2899  Vcvv 3172  cdif 3536  wss 3539  ifcif 4035  {csn 4124  {cpr 4126   class class class wbr 4577  cmpt 4637  ccnv 5027  dom cdm 5028  ran crn 5029  cres 5030  cima 5031  ccom 5032   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  Fincfn 7819  supcsup 8207  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798  +∞cpnf 9928  -∞cmnf 9929  *cxr 9930   < clt 9931  cle 9932  cmin 10118  -cneg 10119   / cdiv 10536  cn 10870  2c2 10920  0cn0 11142  cuz 11522  +crp 11667  (,]cioc 12006  [,)cico 12007  [,]cicc 12008  ...cfz 12155  seqcseq 12621  cexp 12680  abscabs 13771  cli 14012  Σcsu 14213  t crest 15853  TopOpenctopn 15854  ∞Metcxmt 19501  ballcbl 19503  fldccnfld 19516  Topctop 20465  cnccncf 22435   D cdv 23378  logclog 24050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ioc 12010  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-shft 13604  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-limsup 13999  df-clim 14016  df-rlim 14017  df-sum 14214  df-ef 14586  df-sin 14588  df-cos 14589  df-tan 14590  df-pi 14591  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-cmp 20948  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-limc 23381  df-dv 23382  df-ulm 23880  df-log 24052
This theorem is referenced by:  logtaylsum  24152  logtayl2  24153  atantayl  24409  stirlinglem5  38795
  Copyright terms: Public domain W3C validator