Proof of Theorem srgbinomlem
Step | Hyp | Ref
| Expression |
1 | | srgbinom.s |
. . . 4
⊢ 𝑆 = (Base‘𝑅) |
2 | | srgbinom.m |
. . . 4
⊢ × =
(.r‘𝑅) |
3 | | srgbinom.t |
. . . 4
⊢ · =
(.g‘𝑅) |
4 | | srgbinom.a |
. . . 4
⊢ + =
(+g‘𝑅) |
5 | | srgbinom.g |
. . . 4
⊢ 𝐺 = (mulGrp‘𝑅) |
6 | | srgbinom.e |
. . . 4
⊢ ↑ =
(.g‘𝐺) |
7 | | srgbinomlem.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ SRing) |
8 | | srgbinomlem.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
9 | | srgbinomlem.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
10 | | srgbinomlem.c |
. . . 4
⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) |
11 | | srgbinomlem.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
12 | | srgbinomlem.i |
. . . 4
⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | srgbinomlem3 19959 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | srgbinomlem4 19960 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
15 | 13, 14 | oveq12d 7375 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) + ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵)) = ((𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
16 | 5 | srgmgp 19922 |
. . . . . . 7
⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) |
17 | 7, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
18 | | srgmnd 19921 |
. . . . . . . 8
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
19 | 7, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
20 | 1, 4 | mndcl 18564 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 + 𝐵) ∈ 𝑆) |
21 | 19, 8, 9, 20 | syl3anc 1371 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐵) ∈ 𝑆) |
22 | 17, 11, 21 | 3jca 1128 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ (𝐴 + 𝐵) ∈ 𝑆)) |
23 | 22 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ (𝐴 + 𝐵) ∈ 𝑆)) |
24 | 5, 1 | mgpbas 19902 |
. . . . 5
⊢ 𝑆 = (Base‘𝐺) |
25 | 5, 2 | mgpplusg 19900 |
. . . . 5
⊢ × =
(+g‘𝐺) |
26 | 24, 6, 25 | mulgnn0p1 18887 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0
∧ (𝐴 + 𝐵) ∈ 𝑆) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = ((𝑁 ↑ (𝐴 + 𝐵)) × (𝐴 + 𝐵))) |
27 | 23, 26 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = ((𝑁 ↑ (𝐴 + 𝐵)) × (𝐴 + 𝐵))) |
28 | 24, 6, 17, 11, 21 | mulgnn0cld 18897 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ↑ (𝐴 + 𝐵)) ∈ 𝑆) |
29 | 28, 8, 9 | 3jca 1128 |
. . . . . 6
⊢ (𝜑 → ((𝑁 ↑ (𝐴 + 𝐵)) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
30 | 7, 29 | jca 512 |
. . . . 5
⊢ (𝜑 → (𝑅 ∈ SRing ∧ ((𝑁 ↑ (𝐴 + 𝐵)) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))) |
31 | 30 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ SRing ∧ ((𝑁 ↑ (𝐴 + 𝐵)) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))) |
32 | 1, 4, 2 | srgdi 19928 |
. . . 4
⊢ ((𝑅 ∈ SRing ∧ ((𝑁 ↑ (𝐴 + 𝐵)) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → ((𝑁 ↑ (𝐴 + 𝐵)) × (𝐴 + 𝐵)) = (((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) + ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵))) |
33 | 31, 32 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × (𝐴 + 𝐵)) = (((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) + ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵))) |
34 | 27, 33 | eqtrd 2776 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = (((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) + ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵))) |
35 | | elfzelz 13441 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
36 | | bcpasc 14221 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
37 | 11, 35, 36 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
38 | 37 | oveq1d 7372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
39 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑅 ∈ Mnd) |
40 | | bccl 14222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
41 | 11, 35, 40 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) |
42 | 35 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℤ) |
43 | | peano2zm 12546 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑘 − 1) ∈ ℤ) |
45 | | bccl 14222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
46 | 11, 44, 45 | syl2an2r 683 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
47 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑅 ∈ SRing) |
48 | 17 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐺 ∈ Mnd) |
49 | | fznn0sub 13473 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
50 | 49 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
51 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐴 ∈ 𝑆) |
52 | 24, 6, 48, 50, 51 | mulgnn0cld 18897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆) |
53 | | elfznn0 13534 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
54 | 53 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
55 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐵 ∈ 𝑆) |
56 | 24, 6, 48, 54, 55 | mulgnn0cld 18897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑘 ↑ 𝐵) ∈ 𝑆) |
57 | 1, 2 | srgcl 19924 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ (((𝑁 + 1) − 𝑘) ↑ 𝐴) ∈ 𝑆 ∧ (𝑘 ↑ 𝐵) ∈ 𝑆) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) ∈ 𝑆) |
58 | 47, 52, 56, 57 | syl3anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) ∈ 𝑆) |
59 | 1, 3, 4 | mulgnn0dir 18906 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁C(𝑘 − 1)) ∈ ℕ0 ∧
((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)) ∈ 𝑆)) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
60 | 39, 41, 46, 58, 59 | syl13anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
61 | 38, 60 | eqtr3d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) = (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) |
62 | 61 | mpteq2dva 5205 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |
63 | 62 | oveq2d 7373 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
64 | | srgcmn 19920 |
. . . . . 6
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) |
65 | 7, 64 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
66 | | fzfid 13878 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) |
67 | 1, 3, 39, 41, 58 | mulgnn0cld 18897 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
68 | 35, 43 | syl 17 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
69 | 11, 68, 45 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
70 | 1, 3, 39, 69, 58 | mulgnn0cld 18897 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) ∈ 𝑆) |
71 | | eqid 2736 |
. . . . 5
⊢ (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
72 | | eqid 2736 |
. . . . 5
⊢ (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) = (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))) |
73 | 1, 4, 65, 66, 67, 70, 71, 72 | gsummptfidmadd 19702 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))) + ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
74 | 63, 73 | eqtrd 2776 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
75 | 74 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))) + (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))) |
76 | 15, 34, 75 | 3eqtr4d 2786 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) |