Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . 3
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
2 | 1 | oveq1d 6564 |
. 2
⊢ (𝜓 → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
3 | | srgbinom.s |
. . . 4
⊢ 𝑆 = (Base‘𝑅) |
4 | | eqid 2610 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | srgbinom.a |
. . . 4
⊢ + =
(+g‘𝑅) |
6 | | srgbinom.m |
. . . 4
⊢ × =
(.r‘𝑅) |
7 | | srgbinomlem.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ SRing) |
8 | | ovex 6577 |
. . . . 5
⊢
(0...𝑁) ∈
V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (0...𝑁) ∈ V) |
10 | | srgbinomlem.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
11 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
12 | | srgbinomlem.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
13 | | elfzelz 12213 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
14 | | bccl 12971 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
15 | 12, 13, 14 | syl2an 493 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
16 | | fznn0sub 12244 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
18 | | elfznn0 12302 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
20 | | srgbinom.t |
. . . . . 6
⊢ · =
(.g‘𝑅) |
21 | | srgbinom.g |
. . . . . 6
⊢ 𝐺 = (mulGrp‘𝑅) |
22 | | srgbinom.e |
. . . . . 6
⊢ ↑ =
(.g‘𝐺) |
23 | | srgbinomlem.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
24 | | srgbinomlem.c |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
25 | 3, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12 | srgbinomlem2 18364 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁 − 𝑘) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
26 | 11, 15, 17, 19, 25 | syl13anc 1320 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
27 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
28 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
29 | | ovex 6577 |
. . . . . 6
⊢ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V |
30 | 29 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ V) |
31 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
32 | 31 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
33 | 27, 28, 30, 32 | fsuppmptdm 8169 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) finSupp (0g‘𝑅)) |
34 | 3, 4, 5, 6, 7, 9, 10, 26, 33 | srgsummulcr 18360 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵)) |
35 | | srgcmn 18331 |
. . . . . 6
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
36 | 7, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
37 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
38 | 37 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
39 | | 0zd 11266 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
40 | 12 | nn0zd 11356 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
41 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing) |
42 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ 𝑆) |
43 | 3, 6 | srgcl 18335 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
44 | 41, 26, 42, 43 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) ∈ 𝑆) |
45 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (𝑁C𝑘) = (𝑁C(𝑗 − 1))) |
46 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑗 − 1))) |
47 | 46 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 𝑘) ↑ 𝐴) = ((𝑁 − (𝑗 − 1)) ↑ 𝐴)) |
48 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 1) → (𝑘 ↑ 𝐵) = ((𝑗 − 1) ↑ 𝐵)) |
49 | 47, 48 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
50 | 45, 49 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = (𝑗 − 1) → ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
51 | 50 | oveq1d 6564 |
. . . . 5
⊢ (𝑘 = (𝑗 − 1) → (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
52 | 3, 4, 36, 38, 39, 40, 44, 51 | gsummptshft 18159 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)))) |
53 | 12 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
54 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ) |
55 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℤ) |
57 | 56 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℂ) |
58 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) |
59 | 54, 57, 58 | subsub3d 10301 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑗 − 1)) = ((𝑁 + 1) − 𝑗)) |
60 | 59 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 − (𝑗 − 1)) ↑ 𝐴) = (((𝑁 + 1) − 𝑗) ↑ 𝐴)) |
61 | 60 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)) = ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) |
62 | 61 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
63 | 62 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) |
64 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ SRing) |
65 | | peano2zm 11297 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → (𝑗 − 1) ∈
ℤ) |
66 | 55, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℤ) |
67 | | bccl 12971 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑗 − 1) ∈
ℤ) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
68 | 12, 66, 67 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁C(𝑗 − 1)) ∈
ℕ0) |
69 | 21 | srgmgp 18333 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) |
70 | 7, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Mnd) |
71 | 70 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
72 | | 0p1e1 11009 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
73 | 72 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) |
74 | 73 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↔ 𝑗 ∈ (1...(𝑁 + 1))) |
75 | | fznn0sub 12244 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
77 | 74, 76 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈
ℕ0)) |
78 | 77 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 + 1) − 𝑗) ∈
ℕ0) |
79 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
80 | 21, 3 | mgpbas 18318 |
. . . . . . . . . . . 12
⊢ 𝑆 = (Base‘𝐺) |
81 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑗) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆) → (((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) |
82 | 71, 78, 79, 81 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) |
83 | | elfznn 12241 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ) |
84 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
86 | 74, 85 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
87 | 86 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑗 − 1) ∈
ℕ0) |
88 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
89 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆) |
90 | 71, 87, 88, 89 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆) |
91 | 3, 20, 6 | srgmulgass 18354 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑗 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
92 | 64, 68, 82, 90, 91 | syl13anc 1320 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵)))) |
93 | 92 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵))) |
94 | 93 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵)) |
95 | | srgmnd 18332 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
96 | 7, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Mnd) |
97 | 96 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ Mnd) |
98 | 3, 20 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ (𝑁C(𝑗 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑗) ↑ 𝐴) ∈ 𝑆) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆) |
99 | 97, 68, 82, 98 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆) |
100 | 3, 6 | srgass 18336 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) ∈ 𝑆 ∧ ((𝑗 − 1) ↑ 𝐵) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
101 | 64, 99, 90, 88, 100 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵))) |
102 | 21, 6 | mgpplusg 18316 |
. . . . . . . . . . . 12
⊢ × =
(+g‘𝐺) |
103 | 80, 22, 102 | mulgnn0p1 17375 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) + 1) ↑ 𝐵) = (((𝑗 − 1) ↑ 𝐵) × 𝐵)) |
104 | 103 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
105 | 71, 87, 88, 104 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) ↑ 𝐵) × 𝐵) = (((𝑗 − 1) + 1) ↑ 𝐵)) |
106 | 105 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) ↑ 𝐵) × 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵))) |
107 | 55 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℂ) |
108 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 1 ∈
ℂ) |
109 | 107, 108 | npcand 10275 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑗 − 1) + 1) = 𝑗) |
110 | 109 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) + 1) = 𝑗) |
111 | 110 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) + 1) ↑ 𝐵) = (𝑗 ↑ 𝐵)) |
112 | 111 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (((𝑗 − 1) + 1) ↑ 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
113 | 101, 106,
112 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × ((𝑗 − 1) ↑ 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
114 | 63, 94, 113 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
115 | 114 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵)) = (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) |
116 | 115 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) ↑ 𝐴) × ((𝑗 − 1) ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))))) |
117 | | mpteq1 4665 |
. . . . . . . 8
⊢ (((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) |
118 | 73, 117 | ax-mp 5 |
. . . . . . 7
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) |
119 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) |
120 | 119 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑁C(𝑗 − 1)) = (𝑁C(𝑘 − 1))) |
121 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑁 + 1) − 𝑗) = ((𝑁 + 1) − 𝑘)) |
122 | 121 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (((𝑁 + 1) − 𝑗) ↑ 𝐴) = (((𝑁 + 1) − 𝑘) ↑ 𝐴)) |
123 | 120, 122 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) = ((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴))) |
124 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝑗 ↑ 𝐵) = (𝑘 ↑ 𝐵)) |
125 | 123, 124 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)) = (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
126 | 125 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
127 | 118, 126 | eqtri 2632 |
. . . . . 6
⊢ (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) |
128 | 127 | oveq2i 6560 |
. . . . 5
⊢ (𝑅 Σg
(𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) |
129 | | fzfid 12634 |
. . . . . . . . 9
⊢ (𝜑 → (1...(𝑁 + 1)) ∈ Fin) |
130 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝜑) |
131 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
132 | | peano2zm 11297 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
134 | | bccl 12971 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
135 | 12, 133, 134 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
136 | | fznn0sub 12244 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
137 | 136 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
138 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ) |
139 | 138 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
140 | 139 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
141 | 3, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12 | srgbinomlem2 18364 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
((𝑁 + 1) − 𝑘) ∈ ℕ0
∧ 𝑘 ∈
ℕ0)) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
142 | 130, 135,
137, 140, 141 | syl13anc 1320 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
143 | 142 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
144 | 3, 36, 129, 143 | gsummptcl 18189 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
145 | 3, 5, 4 | mndlid 17134 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) → ((0g‘𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
146 | 96, 144, 145 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
147 | | 0nn0 11184 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
148 | 147 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℕ0) |
149 | | id 22 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝜑) |
150 | | 0z 11265 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
151 | 150, 37 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
152 | | zsubcl 11296 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) |
153 | 151, 152 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) ∈
ℤ) |
154 | | bccl 12971 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ) → (𝑁C(0 − 1)) ∈
ℕ0) |
155 | 12, 153, 154 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁C(0 − 1)) ∈
ℕ0) |
156 | | nn0cn 11179 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
157 | | peano2cn 10087 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
159 | 158 | subid1d 10260 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
= (𝑁 + 1)) |
160 | | peano2nn0 11210 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
161 | 159, 160 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 0)
∈ ℕ0) |
162 | 12, 161 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + 1) − 0) ∈
ℕ0) |
163 | 3, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12 | srgbinomlem2 18364 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑁C(0 − 1)) ∈ ℕ0
∧ ((𝑁 + 1) − 0)
∈ ℕ0 ∧ 0 ∈ ℕ0)) → ((𝑁C(0 − 1)) ·
((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
164 | 149, 155,
162, 148, 163 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
165 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
166 | 165 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1))) |
167 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0)) |
168 | 167 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (((𝑁 + 1) − 𝑘) ↑ 𝐴) = (((𝑁 + 1) − 0) ↑ 𝐴)) |
169 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 ↑ 𝐵) = (0 ↑ 𝐵)) |
170 | 168, 169 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) = ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) |
171 | 166, 170 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
172 | 3, 171 | gsumsn 18177 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
173 | 96, 148, 164, 172 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
174 | | 0lt1 10429 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
176 | 175, 72 | syl6breqr 4625 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (0 +
1)) |
177 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
178 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
179 | 177, 178,
177 | 3pm3.2i 1232 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) |
180 | | ltsubadd 10377 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) → ((0
− 1) < 0 ↔ 0 < (0 + 1))) |
181 | 179, 180 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0 − 1) < 0
↔ 0 < (0 + 1))) |
182 | 176, 181 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 1) <
0) |
183 | 182 | orcd 406 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 − 1) < 0 ∨
𝑁 < (0 −
1))) |
184 | | bcval4 12956 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) →
(𝑁C(0 − 1)) =
0) |
185 | 12, 153, 183, 184 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C(0 − 1)) = 0) |
186 | 185 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)))) |
187 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 0) ∈
ℕ0 ∧ 𝐴
∈ 𝑆) → (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆) |
188 | 70, 162, 23, 187 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆) |
189 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ 𝐵
∈ 𝑆) → (0 ↑ 𝐵) ∈ 𝑆) |
190 | 70, 148, 10, 189 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ↑ 𝐵) ∈ 𝑆) |
191 | 3, 6 | srgcl 18335 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ SRing ∧ (((𝑁 + 1) − 0) ↑ 𝐴) ∈ 𝑆 ∧ (0 ↑ 𝐵) ∈ 𝑆) → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
192 | 7, 188, 190, 191 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵)) ∈ 𝑆) |
193 | 3, 4, 20 | mulg0 17369 |
. . . . . . . . . 10
⊢
(((((𝑁 + 1) −
0) ↑
𝐴) × (0 ↑ 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
194 | 192, 193 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) = (0g‘𝑅)) |
195 | 173, 186,
194 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) = (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
196 | 195 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑅 Σg
(𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
197 | 146, 196 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
198 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑅 ∈ SRing) |
199 | 70 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
200 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
201 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
202 | 199, 137,
200, 201 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
203 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
204 | 80, 22 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝐵 ∈ 𝑆) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
205 | 199, 140,
203, 204 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
206 | 3, 20, 6 | srgmulgass 18354 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
(((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆 ∧ (𝑘 ↑ 𝐵) ∈ 𝑆)) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
207 | 198, 135,
202, 205, 206 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
208 | 207 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
209 | 208 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
210 | 12, 160 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
211 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝜑) |
212 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
213 | 212, 132 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
214 | 12, 213, 134 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
215 | | fznn0sub 12244 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
216 | 215 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
217 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
218 | 217 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
219 | 211, 214,
216, 218, 141 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
220 | 3, 5, 36, 210, 219 | gsummptfzsplitl 18156 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
221 | | snfi 7923 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
222 | 221 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {0} ∈
Fin) |
223 | 171 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
224 | 223 | ralsng 4165 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → (∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆)) |
225 | 147, 224 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
{0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) ↑ 𝐴) × (0 ↑ 𝐵))) ∈ 𝑆) |
226 | 164, 225 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
227 | 3, 36, 222, 226 | gsummptcl 18189 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) ∈ 𝑆) |
228 | 3, 5 | cmncom 18032 |
. . . . . . . 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) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
229 | 36, 144, 227, 228 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
230 | 220, 229 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
231 | 197, 209,
230 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) ↑ 𝐴)) × (𝑘 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
232 | 128, 231 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) ↑ 𝐴)) × (𝑗 ↑ 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
233 | 52, 116, 232 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) × 𝐵))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
234 | 34, 233 | eqtr3d 2646 |
. 2
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
235 | 2, 234 | sylan9eqr 2666 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |