Proof of Theorem srgbinomlem3
Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . . 4
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
3 | 2 | oveq1d 6564 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴)) |
4 | | srgbinom.s |
. . . . . 6
⊢ 𝑆 = (Base‘𝑅) |
5 | | srgbinom.a |
. . . . . 6
⊢ + =
(+g‘𝑅) |
6 | | srgbinomlem.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ SRing) |
7 | | srgcmn 18331 |
. . . . . . 7
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
9 | | srgbinomlem.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
10 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝜑) |
11 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
12 | | bccl 12971 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
13 | 9, 11, 12 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) |
14 | | fznn0sub 12244 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
16 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
18 | | srgbinom.m |
. . . . . . . 8
⊢ × =
(.r‘𝑅) |
19 | | srgbinom.t |
. . . . . . . 8
⊢ · =
(.g‘𝑅) |
20 | | srgbinom.g |
. . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝑅) |
21 | | srgbinom.e |
. . . . . . . 8
⊢ ↑ =
(.g‘𝐺) |
22 | | srgbinomlem.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
23 | | srgbinomlem.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
24 | | srgbinomlem.c |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
25 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18364 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
26 | 10, 13, 15, 17, 25 | syl13anc 1320 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
27 | 4, 5, 8, 9, 26 | gsummptfzsplit 18155 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
28 | | srgmnd 18332 |
. . . . . . . . 9
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
29 | 6, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) |
30 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑁 + 1) ∈ V |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
32 | | id 22 |
. . . . . . . . 9
⊢ (𝜑 → 𝜑) |
33 | 9 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
34 | 33 | peano2zd 11361 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
35 | | bccl 12971 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ) → (𝑁C(𝑁 + 1)) ∈
ℕ0) |
36 | 9, 34, 35 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁C(𝑁 + 1)) ∈
ℕ0) |
37 | 9 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
38 | | peano2cn 10087 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
40 | 39 | subidd 10259 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) = 0) |
41 | | 0nn0 11184 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
42 | 40, 41 | syl6eqel 2696 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) ∈
ℕ0) |
43 | | peano2nn0 11210 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
44 | 9, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
45 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑁C(𝑁 + 1)) ∈ ℕ0 ∧
((𝑁 + 1) − (𝑁 + 1)) ∈
ℕ0 ∧ (𝑁 + 1) ∈ ℕ0)) →
((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) |
46 | 32, 36, 42, 44, 45 | syl13anc 1320 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) |
47 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) |
48 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑁 + 1) → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − (𝑁 + 1))) |
49 | 48 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴)) |
50 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → (𝑘 ↑ 𝐵) = ((𝑁 + 1) ↑ 𝐵)) |
51 | 49, 50 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) |
52 | 47, 51 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
53 | 4, 52 | gsumsn 18177 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑁 + 1) ∈ V ∧ ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
54 | 29, 31, 46, 53 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
55 | 9 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
56 | 55 | ltp1d 10833 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
57 | 56 | olcd 407 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) |
58 | | bcval4 12956 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ ∧ ((𝑁 + 1) <
0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0) |
59 | 9, 34, 57, 58 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) |
60 | 59 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
61 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem1 18363 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (((𝑁 + 1) − (𝑁 + 1)) ∈ ℕ0 ∧
(𝑁 + 1) ∈
ℕ0)) → ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆) |
62 | 32, 42, 44, 61 | syl12anc 1316 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆) |
63 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
64 | 4, 63, 19 | mulg0 17369 |
. . . . . . . 8
⊢
(((((𝑁 + 1) −
(𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0g‘𝑅)) |
65 | 62, 64 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0g‘𝑅)) |
66 | 54, 60, 65 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (0g‘𝑅)) |
67 | 66 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅))) |
68 | | fzfid 12634 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
69 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
70 | | bccl2 12972 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈ ℕ) |
71 | 70 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈
ℕ0) |
72 | 71 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
73 | | fzelp1 12263 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...(𝑁 + 1))) |
74 | 73, 15 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
75 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
76 | 75 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
77 | 69, 72, 74, 76, 25 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
78 | 77 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
79 | 4, 8, 68, 78 | gsummptcl 18189 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
80 | 4, 5, 63 | mndrid 17135 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ (𝑅 Σg
(𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
81 | 29, 79, 80 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
82 | 27, 67, 81 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
83 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing) |
84 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) |
85 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ 𝑆) |
86 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
87 | | fznn0sub 12244 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
88 | 87 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
89 | 4, 18, 20, 21, 83, 84, 85, 76, 86, 88, 19, 72 | srgpcomppsc 18357 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴) = ((𝑁C𝑘) · ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
90 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℂ) |
91 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) |
92 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
93 | 92 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) |
94 | 93 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) |
95 | 90, 91, 94 | addsubd 10292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) |
96 | 95 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 − 𝑘) + 1) ↑ 𝐴)) |
97 | 96 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
98 | 97 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C𝑘) · ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
99 | 89, 98 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴) = ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
100 | 99 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴)) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
101 | 100 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴))) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
102 | | ovex 6577 |
. . . . . 6
⊢
(0...𝑁) ∈
V |
103 | 102 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ V) |
104 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18364 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁 − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
105 | 69, 72, 88, 76, 104 | syl13anc 1320 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
106 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
107 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V |
108 | 107 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V) |
109 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
110 | 109 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
111 | 106, 68, 108, 110 | fsuppmptdm 8169 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) finSupp (0g‘𝑅)) |
112 | 4, 63, 5, 18, 6, 103, 22, 105, 111 | srgsummulcr 18360 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴)) |
113 | 82, 101, 112 | 3eqtr2rd 2651 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
114 | 113 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
115 | 3, 114 | eqtrd 2644 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |