Proof of Theorem srgbinomlem3
Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . . 4
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
2 | 1 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
3 | 2 | oveq1d 7282 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴)) |
4 | | srgbinom.s |
. . . . . 6
⊢ 𝑆 = (Base‘𝑅) |
5 | | srgbinom.a |
. . . . . 6
⊢ + =
(+g‘𝑅) |
6 | | srgbinomlem.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ SRing) |
7 | | srgcmn 19754 |
. . . . . . 7
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
9 | | srgbinomlem.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
10 | | simpl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝜑) |
11 | | elfzelz 13266 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
12 | | bccl 14046 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
13 | 9, 11, 12 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) |
14 | | fznn0sub 13298 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
15 | 14 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
16 | | elfznn0 13359 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
17 | 16 | adantl 482 |
. . . . . . 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 19787 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
26 | 10, 13, 15, 17, 25 | syl13anc 1371 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
27 | 4, 5, 8, 9, 26 | gsummptfzsplit 19543 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
28 | | srgmnd 19755 |
. . . . . . . . 9
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
29 | 6, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) |
30 | | ovexd 7302 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
31 | | id 22 |
. . . . . . . . 9
⊢ (𝜑 → 𝜑) |
32 | 9 | nn0zd 12434 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
33 | 32 | peano2zd 12439 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
34 | | bccl 14046 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ) → (𝑁C(𝑁 + 1)) ∈
ℕ0) |
35 | 9, 33, 34 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁C(𝑁 + 1)) ∈
ℕ0) |
36 | 9 | nn0cnd 12305 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
37 | | peano2cn 11157 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
39 | 38 | subidd 11330 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) = 0) |
40 | | 0nn0 12258 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
41 | 39, 40 | eqeltrdi 2847 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) ∈
ℕ0) |
42 | | peano2nn0 12283 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
43 | 9, 42 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
44 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 19787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑁C(𝑁 + 1)) ∈ ℕ0 ∧
((𝑁 + 1) − (𝑁 + 1)) ∈
ℕ0 ∧ (𝑁 + 1) ∈ ℕ0)) →
((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) |
45 | 31, 35, 41, 43, 44 | syl13anc 1371 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) |
46 | | oveq2 7275 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) |
47 | | oveq2 7275 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑁 + 1) → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − (𝑁 + 1))) |
48 | 47 | oveq1d 7282 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴)) |
49 | | oveq1 7274 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → (𝑘 ↑ 𝐵) = ((𝑁 + 1) ↑ 𝐵)) |
50 | 48, 49 | oveq12d 7285 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) |
51 | 46, 50 | oveq12d 7285 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
52 | 4, 51 | gsumsn 19565 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑁 + 1) ∈ V ∧ ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
53 | 29, 30, 45, 52 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
54 | 9 | nn0red 12304 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
55 | 54 | ltp1d 11915 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
56 | 55 | olcd 871 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) |
57 | | bcval4 14031 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ ∧ ((𝑁 + 1) <
0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0) |
58 | 9, 33, 56, 57 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) |
59 | 58 | oveq1d 7282 |
. . . . . . 7
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)))) |
60 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem1 19786 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (((𝑁 + 1) − (𝑁 + 1)) ∈ ℕ0 ∧
(𝑁 + 1) ∈
ℕ0)) → ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆) |
61 | 31, 41, 43, 60 | syl12anc 834 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆) |
62 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
63 | 4, 62, 19 | mulg0 18717 |
. . . . . . . 8
⊢
(((((𝑁 + 1) −
(𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0g‘𝑅)) |
64 | 61, 63 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0 · ((((𝑁 + 1) − (𝑁 + 1)) ↑ 𝐴) × ((𝑁 + 1) ↑ 𝐵))) = (0g‘𝑅)) |
65 | 53, 59, 64 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (0g‘𝑅)) |
66 | 65 | oveq2d 7283 |
. . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅))) |
67 | | fzfid 13703 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
68 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
69 | | bccl2 14047 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈ ℕ) |
70 | 69 | nnnn0d 12303 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈
ℕ0) |
71 | 70 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
72 | | fzelp1 13318 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...(𝑁 + 1))) |
73 | 72, 15 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
74 | | elfznn0 13359 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
75 | 74 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
76 | 68, 71, 73, 75, 25 | syl13anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
77 | 76 | ralrimiva 3108 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
78 | 4, 8, 67, 77 | gsummptcl 19578 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
79 | 4, 5, 62 | mndrid 18416 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ (𝑅 Σg
(𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
80 | 29, 78, 79 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (0g‘𝑅)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
81 | 27, 66, 80 | 3eqtrd 2782 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
82 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing) |
83 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) |
84 | 23 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ 𝑆) |
85 | 24 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
86 | | fznn0sub 13298 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
87 | 86 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
88 | 4, 18, 20, 21, 82, 83, 84, 75, 85, 87, 19, 71 | srgpcomppsc 19780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴) = ((𝑁C𝑘) · ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
89 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℂ) |
90 | | 1cnd 10980 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) |
91 | | elfzelz 13266 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
92 | 91 | zcnd 12437 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) |
93 | 92 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) |
94 | 89, 90, 93 | addsubd 11363 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) |
95 | 94 | oveq1d 7282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 − 𝑘) + 1) ↑ 𝐴)) |
96 | 95 | oveq1d 7282 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵))) |
97 | 96 | oveq2d 7283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C𝑘) · ((((𝑁 − 𝑘) + 1) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
98 | 88, 97 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴) = ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
99 | 98 | mpteq2dva 5173 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴)) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
100 | 99 | oveq2d 7283 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴))) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
101 | | ovexd 7302 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ V) |
102 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 19787 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁 − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
103 | 68, 71, 87, 75, 102 | syl13anc 1371 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
104 | | eqid 2738 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
105 | | ovexd 7302 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V) |
106 | | fvexd 6781 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
107 | 104, 67, 105, 106 | fsuppmptdm 9126 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) finSupp (0g‘𝑅)) |
108 | 4, 62, 5, 18, 6, 101, 22, 103, 107 | srgsummulcr 19783 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐴))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴)) |
109 | 81, 100, 108 | 3eqtr2rd 2785 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
110 | 109 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
111 | 3, 110 | eqtrd 2778 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |