| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | binomcxplem.s | . . . 4
⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 2 |  | binomcxplem.p | . . . . 5
⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) | 
| 3 |  | binomcxplem.d | . . . . . . 7
⊢ 𝐷 = (◡abs “ (0[,)𝑅)) | 
| 4 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑏◡abs | 
| 5 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑏0 | 
| 6 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑏[,) | 
| 7 |  | binomcxplem.r | . . . . . . . . . 10
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 8 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑏
+ | 
| 9 |  | nfmpt1 5249 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 10 | 1, 9 | nfcxfr 2902 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏𝑆 | 
| 11 |  | nfcv 2904 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏𝑟 | 
| 12 | 10, 11 | nffv 6915 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑏(𝑆‘𝑟) | 
| 13 | 5, 8, 12 | nfseq 14053 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑏seq0(
+ , (𝑆‘𝑟)) | 
| 14 | 13 | nfel1 2921 | . . . . . . . . . . . 12
⊢
Ⅎ𝑏seq0( + ,
(𝑆‘𝑟)) ∈ dom ⇝ | 
| 15 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑏ℝ | 
| 16 | 14, 15 | nfrabw 3474 | . . . . . . . . . . 11
⊢
Ⅎ𝑏{𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } | 
| 17 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑏ℝ* | 
| 18 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑏
< | 
| 19 | 16, 17, 18 | nfsup 9492 | . . . . . . . . . 10
⊢
Ⅎ𝑏sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 20 | 7, 19 | nfcxfr 2902 | . . . . . . . . 9
⊢
Ⅎ𝑏𝑅 | 
| 21 | 5, 6, 20 | nfov 7462 | . . . . . . . 8
⊢
Ⅎ𝑏(0[,)𝑅) | 
| 22 | 4, 21 | nfima 6085 | . . . . . . 7
⊢
Ⅎ𝑏(◡abs
“ (0[,)𝑅)) | 
| 23 | 3, 22 | nfcxfr 2902 | . . . . . 6
⊢
Ⅎ𝑏𝐷 | 
| 24 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑦𝐷 | 
| 25 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑦Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘) | 
| 26 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑏ℕ0 | 
| 27 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑏𝑦 | 
| 28 | 10, 27 | nffv 6915 | . . . . . . . 8
⊢
Ⅎ𝑏(𝑆‘𝑦) | 
| 29 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑏𝑚 | 
| 30 | 28, 29 | nffv 6915 | . . . . . . 7
⊢
Ⅎ𝑏((𝑆‘𝑦)‘𝑚) | 
| 31 | 26, 30 | nfsum 15728 | . . . . . 6
⊢
Ⅎ𝑏Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚) | 
| 32 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → 𝑏 = 𝑦) | 
| 33 | 32 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑏) = (𝑆‘𝑦)) | 
| 34 | 33 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑏)‘𝑘) = ((𝑆‘𝑦)‘𝑘)) | 
| 35 | 34 | sumeq2dv 15739 | . . . . . . 7
⊢ (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘) = Σ𝑘 ∈ ℕ0 ((𝑆‘𝑦)‘𝑘)) | 
| 36 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝑆‘𝑦)‘𝑘) = ((𝑆‘𝑦)‘𝑚)) | 
| 37 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑚((𝑆‘𝑦)‘𝑘) | 
| 38 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘ℂ | 
| 39 |  | nfmpt1 5249 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))) | 
| 40 | 38, 39 | nfmpt 5248 | . . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 41 | 1, 40 | nfcxfr 2902 | . . . . . . . . . 10
⊢
Ⅎ𝑘𝑆 | 
| 42 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑘𝑦 | 
| 43 | 41, 42 | nffv 6915 | . . . . . . . . 9
⊢
Ⅎ𝑘(𝑆‘𝑦) | 
| 44 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑘𝑚 | 
| 45 | 43, 44 | nffv 6915 | . . . . . . . 8
⊢
Ⅎ𝑘((𝑆‘𝑦)‘𝑚) | 
| 46 | 36, 37, 45 | cbvsum 15732 | . . . . . . 7
⊢
Σ𝑘 ∈
ℕ0 ((𝑆‘𝑦)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚) | 
| 47 | 35, 46 | eqtrdi 2792 | . . . . . 6
⊢ (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚)) | 
| 48 | 23, 24, 25, 31, 47 | cbvmptf 5250 | . . . . 5
⊢ (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) = (𝑦 ∈ 𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚)) | 
| 49 | 2, 48 | eqtri 2764 | . . . 4
⊢ 𝑃 = (𝑦 ∈ 𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚)) | 
| 50 |  | ovexd 7467 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐶C𝑐𝑗) ∈ V) | 
| 51 |  | binomcxplem.f | . . . . . 6
⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) | 
| 52 | 51 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))) | 
| 53 | 51 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))) | 
| 54 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) | 
| 55 | 54 | oveq2d 7448 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝐶C𝑐𝑗) = (𝐶C𝑐𝑘)) | 
| 56 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 57 |  | binomcxp.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 58 | 57 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) | 
| 59 | 58, 56 | bcccl 44363 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐𝑘) ∈
ℂ) | 
| 60 | 53, 55, 56, 59 | fvmptd 7022 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐶C𝑐𝑘)) | 
| 61 | 60, 59 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ) | 
| 62 | 50, 52, 61 | fmpt2d 7143 | . . . 4
⊢ (𝜑 → 𝐹:ℕ0⟶ℂ) | 
| 63 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑟ℝ | 
| 64 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑧ℝ | 
| 65 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑧seq0( + ,
(𝑆‘𝑟)) ∈ dom ⇝ | 
| 66 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑟0 | 
| 67 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑟
+ | 
| 68 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑟(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 69 | 1, 68 | nfcxfr 2902 | . . . . . . . . . 10
⊢
Ⅎ𝑟𝑆 | 
| 70 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑟𝑧 | 
| 71 | 69, 70 | nffv 6915 | . . . . . . . . 9
⊢
Ⅎ𝑟(𝑆‘𝑧) | 
| 72 | 66, 67, 71 | nfseq 14053 | . . . . . . . 8
⊢
Ⅎ𝑟seq0(
+ , (𝑆‘𝑧)) | 
| 73 | 72 | nfel1 2921 | . . . . . . 7
⊢
Ⅎ𝑟seq0( + ,
(𝑆‘𝑧)) ∈ dom ⇝ | 
| 74 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑟 = 𝑧 → (𝑆‘𝑟) = (𝑆‘𝑧)) | 
| 75 | 74 | seqeq3d 14051 | . . . . . . . 8
⊢ (𝑟 = 𝑧 → seq0( + , (𝑆‘𝑟)) = seq0( + , (𝑆‘𝑧))) | 
| 76 | 75 | eleq1d 2825 | . . . . . . 7
⊢ (𝑟 = 𝑧 → (seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ )) | 
| 77 | 63, 64, 65, 73, 76 | cbvrabw 3472 | . . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑟)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑧)) ∈ dom ⇝
} | 
| 78 | 77 | supeq1i 9488 | . . . . 5
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑧 ∈
ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 79 | 7, 78 | eqtri 2764 | . . . 4
⊢ 𝑅 = sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 80 | 1 | fveq1i 6906 | . . . . . . . . . . 11
⊢ (𝑆‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) | 
| 81 |  | seqeq3 14048 | . . . . . . . . . . 11
⊢ ((𝑆‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) → seq0( + , (𝑆‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧))) | 
| 82 | 80, 81 | ax-mp 5 | . . . . . . . . . 10
⊢ seq0( + ,
(𝑆‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) | 
| 83 | 82 | eleq1i 2831 | . . . . . . . . 9
⊢ (seq0( +
, (𝑆‘𝑧)) ∈ dom ⇝ ↔
seq0( + , ((𝑏 ∈
ℂ ↦ (𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ ) | 
| 84 | 83 | rabbii 3441 | . . . . . . . 8
⊢ {𝑧 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( +
, ((𝑏 ∈ ℂ
↦ (𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ } | 
| 85 | 84 | supeq1i 9488 | . . . . . . 7
⊢
sup({𝑧 ∈
ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 86 | 7, 78, 85 | 3eqtrri 2769 | . . . . . 6
⊢
sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) = 𝑅 | 
| 87 | 86 | eleq1i 2831 | . . . . 5
⊢
(sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ ↔ 𝑅 ∈ ℝ) | 
| 88 | 86 | oveq2i 7443 | . . . . . 6
⊢
((abs‘𝑥) +
sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑏
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) = ((abs‘𝑥) +
𝑅) | 
| 89 | 88 | oveq1i 7442 | . . . . 5
⊢
(((abs‘𝑥) +
sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑏
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2) = (((abs‘𝑥) + 𝑅) / 2) | 
| 90 |  | eqid 2736 | . . . . 5
⊢
((abs‘𝑥) + 1)
= ((abs‘𝑥) +
1) | 
| 91 | 87, 89, 90 | ifbieq12i 4552 | . . . 4
⊢
if(sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1)) = if(𝑅 ∈ ℝ, (((abs‘𝑥) + 𝑅) / 2), ((abs‘𝑥) + 1)) | 
| 92 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑏 → (𝑤↑𝑘) = (𝑏↑𝑘)) | 
| 93 | 92 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑏 → ((𝐹‘𝑘) · (𝑤↑𝑘)) = ((𝐹‘𝑘) · (𝑏↑𝑘))) | 
| 94 | 93 | mpteq2dv 5243 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑏 → (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 95 | 94 | cbvmptv 5254 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘)))) = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | 
| 96 | 95 | fveq1i 6906 | . . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) | 
| 97 |  | seqeq3 14048 | . . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) → seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧))) | 
| 98 | 96, 97 | ax-mp 5 | . . . . . . . . . . . 12
⊢ seq0( + ,
((𝑤 ∈ ℂ ↦
(𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) | 
| 99 | 98 | eleq1i 2831 | . . . . . . . . . . 11
⊢ (seq0( +
, ((𝑤 ∈ ℂ
↦ (𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ ↔ seq0( + ,
((𝑏 ∈ ℂ ↦
(𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ ) | 
| 100 | 99 | rabbii 3441 | . . . . . . . . . 10
⊢ {𝑧 ∈ ℝ ∣ seq0( +
, ((𝑤 ∈ ℂ
↦ (𝑘 ∈
ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ } | 
| 101 | 100 | supeq1i 9488 | . . . . . . . . 9
⊢
sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 102 | 101 | eleq1i 2831 | . . . . . . . 8
⊢
(sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ ↔ sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ) | 
| 103 | 101 | oveq2i 7443 | . . . . . . . . 9
⊢
((abs‘𝑥) +
sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑤
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) = ((abs‘𝑥) +
sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑏
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) | 
| 104 | 103 | oveq1i 7442 | . . . . . . . 8
⊢
(((abs‘𝑥) +
sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑤
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2) = (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2) | 
| 105 | 102, 104,
90 | ifbieq12i 4552 | . . . . . . 7
⊢
if(sup({𝑧 ∈
ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1)) = if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1)) | 
| 106 | 105 | oveq2i 7443 | . . . . . 6
⊢
((abs‘𝑥) +
if(sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑤
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) = ((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) | 
| 107 | 106 | oveq1i 7442 | . . . . 5
⊢
(((abs‘𝑥) +
if(sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑤
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) / 2) = (((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) / 2) | 
| 108 | 107 | oveq2i 7443 | . . . 4
⊢
(0(ball‘(abs ∘ − ))(((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) / 2)) = (0(ball‘(abs ∘
− ))(((abs‘𝑥) +
if(sup({𝑧 ∈ ℝ
∣ seq0( + , ((𝑏
∈ ℂ ↦ (𝑘
∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑥) + 1))) / 2)) | 
| 109 | 1, 49, 62, 79, 3, 91, 108 | pserdv2 26475 | . . 3
⊢ (𝜑 → (ℂ D 𝑃) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))) | 
| 110 |  | cnvimass 6099 | . . . . . . . 8
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs | 
| 111 | 3, 110 | eqsstri 4029 | . . . . . . 7
⊢ 𝐷 ⊆ dom
abs | 
| 112 |  | absf 15377 | . . . . . . . 8
⊢
abs:ℂ⟶ℝ | 
| 113 | 112 | fdmi 6746 | . . . . . . 7
⊢ dom abs =
ℂ | 
| 114 | 111, 113 | sseqtri 4031 | . . . . . 6
⊢ 𝐷 ⊆
ℂ | 
| 115 | 114 | sseli 3978 | . . . . 5
⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ) | 
| 116 |  | binomcxplem.e | . . . . . . . . . 10
⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) | 
| 117 | 116 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))) | 
| 118 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → 𝑏 = 𝑦) | 
| 119 | 118 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → (𝑏↑(𝑘 − 1)) = (𝑦↑(𝑘 − 1))) | 
| 120 | 119 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))) = ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))) | 
| 121 | 120 | mpteq2dva 5241 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))))) | 
| 122 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) | 
| 123 |  | nnex 12273 | . . . . . . . . . . 11
⊢ ℕ
∈ V | 
| 124 | 123 | mptex 7244 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V | 
| 125 | 124 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V) | 
| 126 | 117, 121,
122, 125 | fvmptd 7022 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐸‘𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))))) | 
| 127 | 126 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))))) | 
| 128 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛) | 
| 129 | 128 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝐹‘𝑘) = (𝐹‘𝑛)) | 
| 130 | 128, 129 | oveq12d 7450 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 · (𝐹‘𝑘)) = (𝑛 · (𝐹‘𝑛))) | 
| 131 | 128 | oveq1d 7447 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 − 1) = (𝑛 − 1)) | 
| 132 | 131 | oveq2d 7448 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑦↑(𝑘 − 1)) = (𝑦↑(𝑛 − 1))) | 
| 133 | 130, 132 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))) = ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))) | 
| 134 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) | 
| 135 |  | ovexd 7467 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V) | 
| 136 | 127, 133,
134, 135 | fvmptd 7022 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑦)‘𝑛) = ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))) | 
| 137 | 136 | sumeq2dv 15739 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))) | 
| 138 | 115, 137 | sylan2 593 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))) | 
| 139 | 138 | mpteq2dva 5241 | . . 3
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))) | 
| 140 | 109, 139 | eqtr4d 2779 | . 2
⊢ (𝜑 → (ℂ D 𝑃) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛))) | 
| 141 |  | nfcv 2904 | . . . 4
⊢
Ⅎ𝑏ℕ | 
| 142 |  | nfmpt1 5249 | . . . . . . 7
⊢
Ⅎ𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) | 
| 143 | 116, 142 | nfcxfr 2902 | . . . . . 6
⊢
Ⅎ𝑏𝐸 | 
| 144 | 143, 27 | nffv 6915 | . . . . 5
⊢
Ⅎ𝑏(𝐸‘𝑦) | 
| 145 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑏𝑛 | 
| 146 | 144, 145 | nffv 6915 | . . . 4
⊢
Ⅎ𝑏((𝐸‘𝑦)‘𝑛) | 
| 147 | 141, 146 | nfsum 15728 | . . 3
⊢
Ⅎ𝑏Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) | 
| 148 |  | nfcv 2904 | . . 3
⊢
Ⅎ𝑦Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘) | 
| 149 |  | simpl 482 | . . . . . . 7
⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → 𝑦 = 𝑏) | 
| 150 | 149 | fveq2d 6909 | . . . . . 6
⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑦) = (𝐸‘𝑏)) | 
| 151 | 150 | fveq1d 6907 | . . . . 5
⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑦)‘𝑛) = ((𝐸‘𝑏)‘𝑛)) | 
| 152 | 151 | sumeq2dv 15739 | . . . 4
⊢ (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝐸‘𝑏)‘𝑛)) | 
| 153 |  | fveq2 6905 | . . . . 5
⊢ (𝑛 = 𝑘 → ((𝐸‘𝑏)‘𝑛) = ((𝐸‘𝑏)‘𝑘)) | 
| 154 |  | nfmpt1 5249 | . . . . . . . . 9
⊢
Ⅎ𝑘(𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))) | 
| 155 | 38, 154 | nfmpt 5248 | . . . . . . . 8
⊢
Ⅎ𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) | 
| 156 | 116, 155 | nfcxfr 2902 | . . . . . . 7
⊢
Ⅎ𝑘𝐸 | 
| 157 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑘𝑏 | 
| 158 | 156, 157 | nffv 6915 | . . . . . 6
⊢
Ⅎ𝑘(𝐸‘𝑏) | 
| 159 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑘𝑛 | 
| 160 | 158, 159 | nffv 6915 | . . . . 5
⊢
Ⅎ𝑘((𝐸‘𝑏)‘𝑛) | 
| 161 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑛((𝐸‘𝑏)‘𝑘) | 
| 162 | 153, 160,
161 | cbvsum 15732 | . . . 4
⊢
Σ𝑛 ∈
ℕ ((𝐸‘𝑏)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘) | 
| 163 | 152, 162 | eqtrdi 2792 | . . 3
⊢ (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)) | 
| 164 | 24, 23, 147, 148, 163 | cbvmptf 5250 | . 2
⊢ (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)) | 
| 165 | 140, 164 | eqtrdi 2792 | 1
⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))) |