Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . 3
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
2 | 1 | oveq1d 7299 |
. 2
⊢ (𝜓 → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
3 | | srgbinom.s |
. . . 4
⊢ 𝑆 = (Base‘𝑅) |
4 | | eqid 2739 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | srgbinom.a |
. . . 4
⊢ + =
(+g‘𝑅) |
6 | | srgbinom.m |
. . . 4
⊢ × =
(.r‘𝑅) |
7 | | srgbinomlem.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ SRing) |
8 | | ovexd 7319 |
. . . 4
⊢ (𝜑 → (0...𝑁) ∈ V) |
9 | | srgbinomlem.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
10 | | simpl 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
11 | | srgbinomlem.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
12 | | elfzelz 13265 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
13 | | bccl 14045 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
14 | 11, 12, 13 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
15 | | fznn0sub 13297 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
16 | 15 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
17 | | elfznn0 13358 |
. . . . . 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 19786 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁 − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
25 | 10, 14, 16, 18, 24 | syl13anc 1371 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
26 | | eqid 2739 |
. . . . 5
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
27 | | fzfid 13702 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
28 | | ovexd 7319 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V) |
29 | | fvexd 6798 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
30 | 26, 27, 28, 29 | fsuppmptdm 9148 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) finSupp (0g‘𝑅)) |
31 | 3, 4, 5, 6, 7, 8, 9, 25, 30 | srgsummulcr 19782 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
32 | | srgcmn 19753 |
. . . . . 6
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
33 | 7, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
34 | | 1z 12359 |
. . . . . 6
⊢ 1 ∈
ℤ |
35 | 34 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
36 | | 0zd 12340 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
37 | 11 | nn0zd 12433 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
38 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing) |
39 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ 𝑆) |
40 | 3, 6 | srgcl 19757 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
41 | 38, 25, 39, 40 | syl3anc 1370 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
42 | | oveq2 7292 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (𝑁C𝑘) = (𝑁C(𝑗 − 1))) |
43 | | oveq2 7292 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑗 − 1))) |
44 | 43 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 𝑘) ↑ 𝐴) = ((𝑁 − (𝑗 − 1)) ↑ 𝐴)) |
45 | | oveq1 7291 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → (𝑘 ↑ 𝐵) = ((𝑗 − 1) ↑ 𝐵)) |
46 | 44, 45 | oveq12d 7302 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
47 | 42, 46 | oveq12d 7302 |
. . . . . 6
⊢ (𝑘 = (𝑗 − 1) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
48 | 47 | oveq1d 7299 |
. . . . 5
⊢ (𝑘 = (𝑗 − 1) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
49 | 3, 4, 33, 35, 36, 37, 41, 48 | gsummptshft 19546 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)))) |
50 | 11 | nn0cnd 12304 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ) |
52 | | elfzelz 13265 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℤ) |
54 | 53 | zcnd 12436 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℂ) |
55 | | 1cnd 10979 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) |
56 | 51, 54, 55 | subsub3d 11371 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑗 − 1)) = ((𝑁 + 1) − 𝑗)) |
57 | 56 | oveq1d 7299 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 − (𝑗 − 1)) ↑ 𝐴) = (((𝑁 + 1) − 𝑗) ↑ 𝐴)) |
58 | 57 | oveq1d 7299 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)) = ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
59 | 58 | oveq2d 7300 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
60 | 59 | oveq1d 7299 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
61 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ SRing) |
62 | | peano2zm 12372 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → (𝑗 − 1) ∈
ℤ) |
63 | 52, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℤ) |
64 | | bccl 14045 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑗 − 1) ∈
ℤ) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
65 | 11, 63, 64 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
66 | 20 | srgmgp 19755 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) |
67 | 7, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Mnd) |
68 | 67 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
69 | | 0p1e1 12104 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
70 | 69 | oveq1i 7294 |
. . . . . . . . . . . . . 14
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) |
71 | 70 | eleq2i 2831 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↔ 𝑗 ∈ (1...(𝑁 + 1))) |
72 | | fznn0sub 13297 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
73 | 72 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
74 | 71, 73 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
75 | 74 | imp 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
76 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
77 | 20, 3 | mgpbas 19735 |
. . . . . . . . . . . 12
⊢ 𝑆 = (Base‘𝐺) |
78 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑗) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆) → (((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) |
79 | 68, 75, 76, 78 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) |
80 | | elfznn 13294 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ) |
81 | | nnm1nn0 12283 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
83 | 71, 82 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
84 | 83 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑗 − 1) ∈
ℕ0) |
85 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
86 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆) |
87 | 68, 84, 85, 86 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆) |
88 | 3, 19, 6 | srgmulgass 19776 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑗 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
89 | 61, 65, 79, 87, 88 | syl13anc 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
90 | 89 | eqcomd 2745 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵))) |
91 | 90 | oveq1d 7299 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵)) |
92 | | srgmnd 19754 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
93 | 7, 92 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Mnd) |
94 | 93 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ Mnd) |
95 | 3, 19 | mulgnn0cl 18729 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ (𝑁C(𝑗 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆) |
96 | 94, 65, 79, 95 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆) |
97 | 3, 6 | srgass 19758 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
98 | 61, 96, 87, 85, 97 | syl13anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
99 | 20, 6 | mgpplusg 19733 |
. . . . . . . . . . . 12
⊢ × =
(+g‘𝐺) |
100 | 77, 21, 99 | mulgnn0p1 18724 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) + 1) ↑ 𝐵) = (((𝑗 − 1) ↑ 𝐵) × 𝐵)) |
101 | 100 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
102 | 68, 84, 85, 101 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
103 | 102 | oveq2d 7300 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵))) |
104 | 52 | zcnd 12436 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℂ) |
105 | | 1cnd 10979 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 1 ∈
ℂ) |
106 | 104, 105 | npcand 11345 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑗 − 1) + 1) = 𝑗) |
107 | 106 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) + 1) = 𝑗) |
108 | 107 | oveq1d 7299 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) + 1) ↑ 𝐵) = (𝑗 ↑ 𝐵)) |
109 | 108 | oveq2d 7300 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
110 | 98, 103, 109 | 3eqtrd 2783 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
111 | 60, 91, 110 | 3eqtrd 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
112 | 111 | mpteq2dva 5175 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) = (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) |
113 | 112 | oveq2d 7300 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))))) |
114 | 70 | mpteq1i 5171 |
. . . . . . 7
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
115 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) |
116 | 115 | oveq2d 7300 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑁C(𝑗 − 1)) = (𝑁C(𝑘 − 1))) |
117 | | oveq2 7292 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑁 + 1) − 𝑗) = ((𝑁 + 1) − 𝑘)) |
118 | 117 | oveq1d 7299 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (((𝑁 + 1) − 𝑗) ↑ 𝐴) = (((𝑁 + 1) − 𝑘) ↑ 𝐴)) |
119 | 116, 118 | oveq12d 7302 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) = ((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴))) |
120 | | oveq1 7291 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝑗 ↑ 𝐵) = (𝑘 ↑ 𝐵)) |
121 | 119, 120 | oveq12d 7302 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)) = (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
122 | 121 | cbvmptv 5188 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
123 | 114, 122 | eqtri 2767 |
. . . . . 6
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
124 | 123 | oveq2i 7295 |
. . . . 5
⊢ (𝑅 Σg
(𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) |
125 | | fzfid 13702 |
. . . . . . . . 9
⊢ (𝜑 → (1...(𝑁 + 1)) ∈ Fin) |
126 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝜑) |
127 | | elfzelz 13265 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
128 | | peano2zm 12372 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
130 | | bccl 14045 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
131 | 11, 129, 130 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
132 | | fznn0sub 13297 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
133 | 132 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
134 | | elfznn 13294 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ) |
135 | 134 | nnnn0d 12302 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
136 | 135 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
137 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19786 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
((𝑁 + 1) − 𝑘) ∈ ℕ0
∧ 𝑘 ∈
ℕ0)) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
138 | 126, 131,
133, 136, 137 | syl13anc 1371 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
139 | 138 | ralrimiva 3104 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
140 | 3, 33, 125, 139 | gsummptcl 19577 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
141 | 3, 5, 4 | mndlid 18414 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((0g‘𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
142 | 93, 140, 141 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
143 | | 0nn0 12257 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
144 | 143 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℕ0) |
145 | | id 22 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝜑) |
146 | | 0z 12339 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
147 | 146, 34 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
148 | | zsubcl 12371 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) |
149 | 147, 148 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) ∈
ℤ) |
150 | | bccl 14045 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ) → (𝑁C(0 − 1)) ∈
ℕ0) |
151 | 11, 149, 150 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁C(0 − 1)) ∈
ℕ0) |
152 | | nn0cn 12252 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
153 | | peano2cn 11156 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
155 | 154 | subid1d 11330 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
= (𝑁 + 1)) |
156 | | peano2nn0 12282 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
157 | 155, 156 | eqeltrd 2840 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
∈ ℕ0) |
158 | 11, 157 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + 1) − 0) ∈
ℕ0) |
159 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19786 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(0 − 1)) ∈ ℕ0
∧ ((𝑁 + 1) − 0)
∈ ℕ0 ∧ 0 ∈ ℕ0)) → ((𝑁C(0 − 1)) ·
((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
160 | 145, 151,
158, 144, 159 | syl13anc 1371 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
161 | | oveq1 7291 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
162 | 161 | oveq2d 7300 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1))) |
163 | | oveq2 7292 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0)) |
164 | 163 | oveq1d 7299 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 + 1) − 0) ↑ 𝐴)) |
165 | | oveq1 7291 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 ↑ 𝐵) = (0 ↑ 𝐵)) |
166 | 164, 165 | oveq12d 7302 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) |
167 | 162, 166 | oveq12d 7302 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
168 | 3, 167 | gsumsn 19564 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
169 | 93, 144, 160, 168 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
170 | | 0lt1 11506 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
172 | 171, 69 | breqtrrdi 5117 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (0 +
1)) |
173 | | 0re 10986 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
174 | | 1re 10984 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
175 | 173, 174,
173 | 3pm3.2i 1338 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) |
176 | | ltsubadd 11454 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) → ((0
− 1) < 0 ↔ 0 < (0 + 1))) |
177 | 175, 176 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0 − 1) < 0
↔ 0 < (0 + 1))) |
178 | 172, 177 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) <
0) |
179 | 178 | orcd 870 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 − 1) < 0 ∨
𝑁 < (0 −
1))) |
180 | | bcval4 14030 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) →
(𝑁C(0 − 1)) =
0) |
181 | 11, 149, 179, 180 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C(0 − 1)) = 0) |
182 | 181 | oveq1d 7299 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
183 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 0) ∈
ℕ0 ∧ 𝐴
∈ 𝑆) → (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆) |
184 | 67, 158, 22, 183 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆) |
185 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (0 ↑ 𝐵) ∈ 𝑆) |
186 | 67, 144, 9, 185 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ↑ 𝐵) ∈ 𝑆) |
187 | 3, 6 | srgcl 19757 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆 ∧ (0 ↑ 𝐵) ∈ 𝑆) → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
188 | 7, 184, 186, 187 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
189 | 3, 4, 19 | mulg0 18716 |
. . . . . . . . . 10
⊢
(((((𝑁 + 1) −
0) ↑
𝐴) × (0 ↑ 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
190 | 188, 189 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
191 | 169, 182,
190 | 3eqtrrd 2784 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) = (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
192 | 191 | oveq1d 7299 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
193 | 142, 192 | eqtr3d 2781 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
194 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑅 ∈ SRing) |
195 | 67 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
196 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
197 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
198 | 195, 133,
196, 197 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
199 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
200 | 77, 21 | mulgnn0cl 18729 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝐵 ∈ 𝑆) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
201 | 195, 136,
199, 200 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
202 | 3, 19, 6 | srgmulgass 19776 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆 ∧ (𝑘 ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
203 | 194, 131,
198, 201, 202 | syl13anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
204 | 203 | mpteq2dva 5175 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
205 | 204 | oveq2d 7300 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
206 | 11, 156 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
207 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝜑) |
208 | | elfzelz 13265 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
209 | 208, 128 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
210 | 11, 209, 130 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
211 | | fznn0sub 13297 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
212 | 211 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
213 | | elfznn0 13358 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
214 | 213 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
215 | 207, 210,
212, 214, 137 | syl13anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
216 | 3, 5, 33, 206, 215 | gsummptfzsplitl 19543 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
217 | | snfi 8843 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
218 | 217 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {0} ∈
Fin) |
219 | 167 | eleq1d 2824 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
220 | 219 | ralsng 4610 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → (∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
221 | 143, 220 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
{0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
222 | 160, 221 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
223 | 3, 33, 218, 222 | gsummptcl 19577 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
224 | 3, 5 | cmncom 19412 |
. . . . . . . 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) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
225 | 33, 140, 223, 224 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
226 | 216, 225 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
227 | 193, 205,
226 | 3eqtr4d 2789 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
228 | 124, 227 | eqtrid 2791 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
229 | 49, 113, 228 | 3eqtrd 2783 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
230 | 31, 229 | eqtr3d 2781 |
. 2
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
231 | 2, 230 | sylan9eqr 2801 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |