Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . 3
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
2 | 1 | oveq1d 7372 |
. 2
⊢ (𝜓 → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
3 | | srgbinom.s |
. . . 4
⊢ 𝑆 = (Base‘𝑅) |
4 | | eqid 2736 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | srgbinom.a |
. . . 4
⊢ + =
(+g‘𝑅) |
6 | | srgbinom.m |
. . . 4
⊢ × =
(.r‘𝑅) |
7 | | srgbinomlem.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ SRing) |
8 | | ovexd 7392 |
. . . 4
⊢ (𝜑 → (0...𝑁) ∈ V) |
9 | | srgbinomlem.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
10 | | simpl 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
11 | | srgbinomlem.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
12 | | elfzelz 13441 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
13 | | bccl 14222 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
14 | 11, 12, 13 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
15 | | fznn0sub 13473 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
16 | 15 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
17 | | elfznn0 13534 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
18 | 17 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
19 | | srgbinom.t |
. . . . . 6
⊢ · =
(.g‘𝑅) |
20 | | srgbinom.g |
. . . . . 6
⊢ 𝐺 = (mulGrp‘𝑅) |
21 | | srgbinom.e |
. . . . . 6
⊢ ↑ =
(.g‘𝐺) |
22 | | srgbinomlem.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
23 | | srgbinomlem.c |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
24 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19958 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁 − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
25 | 10, 14, 16, 18, 24 | syl13anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
26 | | eqid 2736 |
. . . . 5
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
27 | | fzfid 13878 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
28 | | ovexd 7392 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V) |
29 | | fvexd 6857 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
30 | 26, 27, 28, 29 | fsuppmptdm 9316 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) finSupp (0g‘𝑅)) |
31 | 3, 4, 5, 6, 7, 8, 9, 25, 30 | srgsummulcr 19954 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
32 | | srgcmn 19920 |
. . . . . 6
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
33 | 7, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
34 | | 1z 12533 |
. . . . . 6
⊢ 1 ∈
ℤ |
35 | 34 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
36 | | 0zd 12511 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
37 | 11 | nn0zd 12525 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
38 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing) |
39 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ 𝑆) |
40 | 3, 6 | srgcl 19924 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
41 | 38, 25, 39, 40 | syl3anc 1371 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
42 | | oveq2 7365 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (𝑁C𝑘) = (𝑁C(𝑗 − 1))) |
43 | | oveq2 7365 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑗 − 1))) |
44 | 43 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 𝑘) ↑ 𝐴) = ((𝑁 − (𝑗 − 1)) ↑ 𝐴)) |
45 | | oveq1 7364 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → (𝑘 ↑ 𝐵) = ((𝑗 − 1) ↑ 𝐵)) |
46 | 44, 45 | oveq12d 7375 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
47 | 42, 46 | oveq12d 7375 |
. . . . . 6
⊢ (𝑘 = (𝑗 − 1) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
48 | 47 | oveq1d 7372 |
. . . . 5
⊢ (𝑘 = (𝑗 − 1) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
49 | 3, 4, 33, 35, 36, 37, 41, 48 | gsummptshft 19713 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)))) |
50 | 11 | nn0cnd 12475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ) |
52 | | elfzelz 13441 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℤ) |
54 | 53 | zcnd 12608 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℂ) |
55 | | 1cnd 11150 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) |
56 | 51, 54, 55 | subsub3d 11542 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑗 − 1)) = ((𝑁 + 1) − 𝑗)) |
57 | 56 | oveq1d 7372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 − (𝑗 − 1)) ↑ 𝐴) = (((𝑁 + 1) − 𝑗) ↑ 𝐴)) |
58 | 57 | oveq1d 7372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)) = ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
59 | 58 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
60 | 59 | oveq1d 7372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
61 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ SRing) |
62 | | peano2zm 12546 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → (𝑗 − 1) ∈
ℤ) |
63 | 52, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℤ) |
64 | | bccl 14222 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑗 − 1) ∈
ℤ) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
65 | 11, 63, 64 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
66 | 20, 3 | mgpbas 19902 |
. . . . . . . . . . 11
⊢ 𝑆 = (Base‘𝐺) |
67 | 20 | srgmgp 19922 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) |
68 | 7, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Mnd) |
69 | 68 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
70 | | 0p1e1 12275 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
71 | 70 | oveq1i 7367 |
. . . . . . . . . . . . . 14
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) |
72 | 71 | eleq2i 2829 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↔ 𝑗 ∈ (1...(𝑁 + 1))) |
73 | | fznn0sub 13473 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
74 | 73 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
75 | 72, 74 | biimtrid 241 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
76 | 75 | imp 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
77 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
78 | 66, 21, 69, 76, 77 | mulgnn0cld 18897 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) |
79 | | elfznn 13470 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ) |
80 | | nnm1nn0 12454 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
82 | 72, 81 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
83 | 82 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑗 − 1) ∈
ℕ0) |
84 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
85 | 66, 21, 69, 83, 84 | mulgnn0cld 18897 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆) |
86 | 3, 19, 6 | srgmulgass 19948 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑗 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
87 | 61, 65, 78, 85, 86 | syl13anc 1372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
88 | 87 | eqcomd 2742 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵))) |
89 | 88 | oveq1d 7372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵)) |
90 | | srgmnd 19921 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
91 | 7, 90 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Mnd) |
92 | 91 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ Mnd) |
93 | 3, 19, 92, 65, 78 | mulgnn0cld 18897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆) |
94 | 3, 6 | srgass 19925 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
95 | 61, 93, 85, 84, 94 | syl13anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
96 | 20, 6 | mgpplusg 19900 |
. . . . . . . . . . . 12
⊢ × =
(+g‘𝐺) |
97 | 66, 21, 96 | mulgnn0p1 18887 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) + 1) ↑ 𝐵) = (((𝑗 − 1) ↑ 𝐵) × 𝐵)) |
98 | 97 | eqcomd 2742 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
99 | 69, 83, 84, 98 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
100 | 99 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵))) |
101 | 52 | zcnd 12608 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℂ) |
102 | | 1cnd 11150 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 1 ∈
ℂ) |
103 | 101, 102 | npcand 11516 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑗 − 1) + 1) = 𝑗) |
104 | 103 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) + 1) = 𝑗) |
105 | 104 | oveq1d 7372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) + 1) ↑ 𝐵) = (𝑗 ↑ 𝐵)) |
106 | 105 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
107 | 95, 100, 106 | 3eqtrd 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
108 | 60, 89, 107 | 3eqtrd 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
109 | 108 | mpteq2dva 5205 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) = (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) |
110 | 109 | oveq2d 7373 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))))) |
111 | 71 | mpteq1i 5201 |
. . . . . . 7
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
112 | | oveq1 7364 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) |
113 | 112 | oveq2d 7373 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑁C(𝑗 − 1)) = (𝑁C(𝑘 − 1))) |
114 | | oveq2 7365 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑁 + 1) − 𝑗) = ((𝑁 + 1) − 𝑘)) |
115 | 114 | oveq1d 7372 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (((𝑁 + 1) − 𝑗) ↑ 𝐴) = (((𝑁 + 1) − 𝑘) ↑ 𝐴)) |
116 | 113, 115 | oveq12d 7375 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) = ((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴))) |
117 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝑗 ↑ 𝐵) = (𝑘 ↑ 𝐵)) |
118 | 116, 117 | oveq12d 7375 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)) = (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
119 | 118 | cbvmptv 5218 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
120 | 111, 119 | eqtri 2764 |
. . . . . 6
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
121 | 120 | oveq2i 7368 |
. . . . 5
⊢ (𝑅 Σg
(𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) |
122 | | fzfid 13878 |
. . . . . . . . 9
⊢ (𝜑 → (1...(𝑁 + 1)) ∈ Fin) |
123 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝜑) |
124 | | elfzelz 13441 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
125 | | peano2zm 12546 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
127 | | bccl 14222 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
128 | 11, 126, 127 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
129 | | fznn0sub 13473 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
130 | 129 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
131 | | elfznn 13470 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ) |
132 | 131 | nnnn0d 12473 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
133 | 132 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
134 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19958 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
((𝑁 + 1) − 𝑘) ∈ ℕ0
∧ 𝑘 ∈
ℕ0)) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
135 | 123, 128,
130, 133, 134 | syl13anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
136 | 135 | ralrimiva 3143 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
137 | 3, 33, 122, 136 | gsummptcl 19744 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
138 | 3, 5, 4 | mndlid 18576 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((0g‘𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
139 | 91, 137, 138 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
140 | | 0nn0 12428 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
141 | 140 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℕ0) |
142 | | id 22 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝜑) |
143 | | 0z 12510 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
144 | 143, 34 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
145 | | zsubcl 12545 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) |
146 | 144, 145 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) ∈
ℤ) |
147 | | bccl 14222 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ) → (𝑁C(0 − 1)) ∈
ℕ0) |
148 | 11, 146, 147 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁C(0 − 1)) ∈
ℕ0) |
149 | | nn0cn 12423 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
150 | | peano2cn 11327 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
152 | 151 | subid1d 11501 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
= (𝑁 + 1)) |
153 | | peano2nn0 12453 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
154 | 152, 153 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
∈ ℕ0) |
155 | 11, 154 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + 1) − 0) ∈
ℕ0) |
156 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19958 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(0 − 1)) ∈ ℕ0
∧ ((𝑁 + 1) − 0)
∈ ℕ0 ∧ 0 ∈ ℕ0)) → ((𝑁C(0 − 1)) ·
((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
157 | 142, 148,
155, 141, 156 | syl13anc 1372 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
158 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
159 | 158 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1))) |
160 | | oveq2 7365 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0)) |
161 | 160 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 + 1) − 0) ↑ 𝐴)) |
162 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 ↑ 𝐵) = (0 ↑ 𝐵)) |
163 | 161, 162 | oveq12d 7375 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) |
164 | 159, 163 | oveq12d 7375 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
165 | 3, 164 | gsumsn 19731 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
166 | 91, 141, 157, 165 | syl3anc 1371 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
167 | | 0lt1 11677 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
168 | 167 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
169 | 168, 70 | breqtrrdi 5147 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (0 +
1)) |
170 | | 0re 11157 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
171 | | 1re 11155 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
172 | 170, 171,
170 | 3pm3.2i 1339 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) |
173 | | ltsubadd 11625 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) → ((0
− 1) < 0 ↔ 0 < (0 + 1))) |
174 | 172, 173 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0 − 1) < 0
↔ 0 < (0 + 1))) |
175 | 169, 174 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) <
0) |
176 | 175 | orcd 871 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 − 1) < 0 ∨
𝑁 < (0 −
1))) |
177 | | bcval4 14207 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) →
(𝑁C(0 − 1)) =
0) |
178 | 11, 146, 176, 177 | syl3anc 1371 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C(0 − 1)) = 0) |
179 | 178 | oveq1d 7372 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
180 | 66, 21, 68, 155, 22 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆) |
181 | 66, 21, 68, 141, 9 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ↑ 𝐵) ∈ 𝑆) |
182 | 3, 6 | srgcl 19924 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆 ∧ (0 ↑ 𝐵) ∈ 𝑆) → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
183 | 7, 180, 181, 182 | syl3anc 1371 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
184 | 3, 4, 19 | mulg0 18879 |
. . . . . . . . . 10
⊢
(((((𝑁 + 1) −
0) ↑
𝐴) × (0 ↑ 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
185 | 183, 184 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
186 | 166, 179,
185 | 3eqtrrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) = (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
187 | 186 | oveq1d 7372 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
188 | 139, 187 | eqtr3d 2778 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
189 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑅 ∈ SRing) |
190 | 68 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
191 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
192 | 66, 21, 190, 130, 191 | mulgnn0cld 18897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
193 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
194 | 66, 21, 190, 133, 193 | mulgnn0cld 18897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
195 | 3, 19, 6 | srgmulgass 19948 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆 ∧ (𝑘 ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
196 | 189, 128,
192, 194, 195 | syl13anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
197 | 196 | mpteq2dva 5205 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
198 | 197 | oveq2d 7373 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
199 | 11, 153 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
200 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝜑) |
201 | | elfzelz 13441 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
202 | 201, 125 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
203 | 11, 202, 127 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
204 | | fznn0sub 13473 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
205 | 204 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
206 | | elfznn0 13534 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
207 | 206 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
208 | 200, 203,
205, 207, 134 | syl13anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
209 | 3, 5, 33, 199, 208 | gsummptfzsplitl 19710 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
210 | | snfi 8988 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
211 | 210 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {0} ∈
Fin) |
212 | 164 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
213 | 212 | ralsng 4634 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → (∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
214 | 140, 213 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
{0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
215 | 157, 214 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
216 | 3, 33, 211, 215 | gsummptcl 19744 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
217 | 3, 5 | cmncom 19580 |
. . . . . . . 8
⊢ ((𝑅 ∈ CMnd ∧ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆 ∧ (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
218 | 33, 137, 216, 217 | syl3anc 1371 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
219 | 209, 218 | eqtrd 2776 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
220 | 188, 198,
219 | 3eqtr4d 2786 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
221 | 121, 220 | eqtrid 2788 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
222 | 49, 110, 221 | 3eqtrd 2780 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
223 | 31, 222 | eqtr3d 2778 |
. 2
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
224 | 2, 223 | sylan9eqr 2798 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |