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