Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑚 = 0 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 0)) |
2 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 0 → (0...𝑚) = (0...0)) |
3 | | 0z 11388 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
4 | | fzsn 12383 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → (0...0) = {0}) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢ (0...0) =
{0} |
6 | 2, 5 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑚 = 0 → (0...𝑚) = {0}) |
7 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑚 = 0 → (𝑚C𝑘) = (0C𝑘)) |
8 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 0 → (𝑚 − 𝑘) = (0 − 𝑘)) |
9 | 8 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = 0 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (0 − 𝑘))) |
10 | 9 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 0 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) |
11 | 7, 10 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 0 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝑚 = 0 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
13 | 6, 12 | sumeq12dv 14437 |
. . . . . 6
⊢ (𝑚 = 0 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
14 | 1, 13 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 0 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))) |
15 | 14 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
16 | | oveq2 6658 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑛)) |
17 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) |
18 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑚C𝑘) = (𝑛C𝑘)) |
19 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑚 − 𝑘) = (𝑛 − 𝑘)) |
20 | 19 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑛 − 𝑘))) |
21 | 20 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) |
22 | 18, 21 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝑚 = 𝑛 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
24 | 17, 23 | sumeq12dv 14437 |
. . . . . 6
⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
25 | 16, 24 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 𝑛 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))) |
26 | 25 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑛 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
27 | | oveq2 6658 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac (𝑛 + 1))) |
28 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (0...𝑚) = (0...(𝑛 + 1))) |
29 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → (𝑚C𝑘) = ((𝑛 + 1)C𝑘)) |
30 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 𝑘) = ((𝑛 + 1) − 𝑘)) |
31 | 30 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac ((𝑛 + 1) − 𝑘))) |
32 | 31 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) |
33 | 29, 32 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
34 | 33 | adantr 481 |
. . . . . . 7
⊢ ((𝑚 = (𝑛 + 1) ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
35 | 28, 34 | sumeq12dv 14437 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
36 | 27, 35 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
37 | 36 | imbi2d 330 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
38 | | oveq2 6658 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑁)) |
39 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → (0...𝑚) = (0...𝑁)) |
40 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → (𝑚C𝑘) = (𝑁C𝑘)) |
41 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → (𝑚 − 𝑘) = (𝑁 − 𝑘)) |
42 | 41 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑁 − 𝑘))) |
43 | 42 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) |
44 | 40, 43 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
45 | 44 | adantr 481 |
. . . . . . 7
⊢ ((𝑚 = 𝑁 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
46 | 39, 45 | sumeq12dv 14437 |
. . . . . 6
⊢ (𝑚 = 𝑁 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
47 | 38, 46 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 𝑁 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) |
48 | 47 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
49 | | fallfac0 14759 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 0) =
1) |
50 | | fallfac0 14759 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵 FallFac 0) =
1) |
51 | 49, 50 | oveqan12d 6669 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) = (1 ·
1)) |
52 | | 1t1e1 11175 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
53 | 51, 52 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) =
1) |
54 | 53 | oveq2d 6666 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0))) =
(1 · 1)) |
55 | 54, 52 | syl6eq 2672 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0))) =
1) |
56 | | 0cn 10032 |
. . . . . 6
⊢ 0 ∈
ℂ |
57 | | ax-1cn 9994 |
. . . . . . 7
⊢ 1 ∈
ℂ |
58 | 55, 57 | syl6eqel 2709 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0)))
∈ ℂ) |
59 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (0C𝑘) = (0C0)) |
60 | | 0nn0 11307 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
61 | | bcnn 13099 |
. . . . . . . . . 10
⊢ (0 ∈
ℕ0 → (0C0) = 1) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . 9
⊢ (0C0) =
1 |
63 | 59, 62 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑘 = 0 → (0C𝑘) = 1) |
64 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (0 − 𝑘) = (0 −
0)) |
65 | | 0m0e0 11130 |
. . . . . . . . . . 11
⊢ (0
− 0) = 0 |
66 | 64, 65 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (0 − 𝑘) = 0) |
67 | 66 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝐴 FallFac (0 − 𝑘)) = (𝐴 FallFac 0)) |
68 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝐵 FallFac 𝑘) = (𝐵 FallFac 0)) |
69 | 67, 68 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac 0) · (𝐵 FallFac 0))) |
70 | 63, 69 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 0 → ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) |
71 | 70 | sumsn 14475 |
. . . . . 6
⊢ ((0
∈ ℂ ∧ (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) ∈ ℂ) →
Σ𝑘 ∈ {0}
((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) |
72 | 56, 58, 71 | sylancr 695 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
Σ𝑘 ∈ {0}
((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) |
73 | | addcl 10018 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
74 | | fallfac0 14759 |
. . . . . 6
⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵) FallFac 0) = 1) |
75 | 73, 74 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = 1) |
76 | 55, 72, 75 | 3eqtr4rd 2667 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
77 | | simprl 794 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝐴 ∈
ℂ) |
78 | | simprr 796 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝐵 ∈
ℂ) |
79 | | simpl 473 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝑛 ∈
ℕ0) |
80 | | id 22 |
. . . . . . 7
⊢ (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
81 | 77, 78, 79, 80 | binomfallfaclem2 14771 |
. . . . . 6
⊢ (((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
∧ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
82 | 81 | exp31 630 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
83 | 82 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ (((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) |
84 | 15, 26, 37, 48, 76, 83 | nn0ind 11472 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) |
85 | 84 | com12 32 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 ∈ ℕ0
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) |
86 | 85 | 3impia 1261 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |