Step | Hyp | Ref
| Expression |
1 | | binomcxp.a |
. . 3
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
2 | | binomcxp.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | binomcxp.lt |
. . 3
⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) |
4 | | binomcxp.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
5 | 1, 2, 3, 4 | binomcxplemnn0 38548 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) |
6 | | eqid 2622 |
. . 3
⊢ (𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗)) = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
7 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) = ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘)) |
8 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑏↑𝑥) = (𝑏↑𝑘)) |
9 | 7, 8 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝑘 → (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥)) = (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘) · (𝑏↑𝑘))) |
10 | 9 | cbvmptv 4750 |
. . . 4
⊢ (𝑥 ∈ ℕ0
↦ (((𝑗 ∈
ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))) = (𝑘 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑘) · (𝑏↑𝑘))) |
11 | 10 | mpteq2i 4741 |
. . 3
⊢ (𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑗 ∈
ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥)))) = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑘) · (𝑏↑𝑘)))) |
12 | | eqid 2622 |
. . 3
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
13 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → 𝑥 = 𝑘) |
14 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑗 → (𝐶C𝑐𝑦) = (𝐶C𝑐𝑗)) |
15 | 14 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
↦ (𝐶C𝑐𝑦)) = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦)) = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))) |
17 | 16, 13 | fveq12d 6197 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦))‘𝑥) = ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘)) |
18 | 13, 17 | oveq12d 6668 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑥 · ((𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦))‘𝑥)) = (𝑘 · ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘))) |
19 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 − 1) = (𝑘 − 1)) |
20 | 19 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑏↑(𝑥 − 1)) = (𝑏↑(𝑘 − 1))) |
21 | 18, 20 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((𝑥 · ((𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦))‘𝑥)) · (𝑏↑(𝑥 − 1))) = ((𝑘 · ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘)) · (𝑏↑(𝑘 − 1)))) |
22 | 21 | cbvmptv 4750 |
. . . 4
⊢ (𝑥 ∈ ℕ ↦ ((𝑥 · ((𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦))‘𝑥)) · (𝑏↑(𝑥 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘)) · (𝑏↑(𝑘 − 1)))) |
23 | 22 | mpteq2i 4741 |
. . 3
⊢ (𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ ↦ ((𝑥 · ((𝑦 ∈ ℕ0 ↦ (𝐶C𝑐𝑦))‘𝑥)) · (𝑏↑(𝑥 − 1))))) = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑘)) · (𝑏↑(𝑘 − 1))))) |
24 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑗 → (𝐶C𝑐𝑥) = (𝐶C𝑐𝑗)) |
25 | 24 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥)) = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
26 | 25 | fveq1i 6192 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥))‘𝑥) = ((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) |
27 | 26 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥)) = (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥)) |
28 | 27 | mpteq2i 4741 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))) = (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))) |
29 | 28 | mpteq2i 4741 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥)))) = (𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥)))) |
30 | 29 | fveq1i 6192 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟) = ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟) |
31 | | seqeq3 12806 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟) = ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟) → seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . 9
⊢ seq0( + ,
((𝑏 ∈ ℂ ↦
(𝑥 ∈
ℕ0 ↦ (((𝑥 ∈ ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) |
33 | 32 | eleq1i 2692 |
. . . . . . . 8
⊢ (seq0( +
, ((𝑏 ∈ ℂ
↦ (𝑥 ∈
ℕ0 ↦ (((𝑥 ∈ ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + ,
((𝑏 ∈ ℂ ↦
(𝑥 ∈
ℕ0 ↦ (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ ) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝑟 ∈ ℝ → (seq0( +
, ((𝑏 ∈ ℂ
↦ (𝑥 ∈
ℕ0 ↦ (((𝑥 ∈ ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + ,
((𝑏 ∈ ℂ ↦
(𝑥 ∈
ℕ0 ↦ (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ )) |
35 | 34 | rabbiia 3185 |
. . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, ((𝑏 ∈ ℂ
↦ (𝑥 ∈
ℕ0 ↦ (((𝑥 ∈ ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑗 ∈
ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ } |
36 | 35 | supeq1i 8353 |
. . . . 5
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
37 | 36 | oveq2i 6661 |
. . . 4
⊢
(0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑥 ∈ ℕ0
↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) = (0[,)sup({𝑟
∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
38 | 37 | imaeq2i 5464 |
. . 3
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) = (◡abs “
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑏
∈ ℂ ↦ (𝑥
∈ ℕ0 ↦ (((𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
39 | | eqid 2622 |
. . 3
⊢ (𝑏 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑘
∈ ℕ0 (((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑏)‘𝑘)) = (𝑏 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0
↦ (((𝑥 ∈
ℕ0 ↦ (𝐶C𝑐𝑥))‘𝑥) · (𝑏↑𝑥))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑘
∈ ℕ0 (((𝑏 ∈ ℂ ↦ (𝑥 ∈ ℕ0 ↦ (((𝑗 ∈ ℕ0
↦ (𝐶C𝑐𝑗))‘𝑥) · (𝑏↑𝑥))))‘𝑏)‘𝑘)) |
40 | 1, 2, 3, 4, 6, 11,
12, 23, 38, 39 | binomcxplemnotnn0 38555 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) |
41 | 5, 40 | pm2.61dan 832 |
1
⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) |