# Metamath Proof Explorer

## Theorem srgbinomlem3

Description: Lemma 3 for srgbinomlem . (Contributed by AV, 23-Aug-2019) (Proof shortened by AV, 27-Oct-2019)

Ref Expression
Hypotheses srgbinom.s ${⊢}{S}={\mathrm{Base}}_{{R}}$
srgbinom.m
srgbinom.t
srgbinom.a
srgbinom.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
srgbinom.e
srgbinomlem.r ${⊢}{\phi }\to {R}\in \mathrm{SRing}$
srgbinomlem.a ${⊢}{\phi }\to {A}\in {S}$
srgbinomlem.b ${⊢}{\phi }\to {B}\in {S}$
srgbinomlem.c
srgbinomlem.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
srgbinomlem.i
Assertion srgbinomlem3

### Proof

Step Hyp Ref Expression
1 srgbinom.s ${⊢}{S}={\mathrm{Base}}_{{R}}$
2 srgbinom.m
3 srgbinom.t
4 srgbinom.a
5 srgbinom.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
6 srgbinom.e
7 srgbinomlem.r ${⊢}{\phi }\to {R}\in \mathrm{SRing}$
8 srgbinomlem.a ${⊢}{\phi }\to {A}\in {S}$
9 srgbinomlem.b ${⊢}{\phi }\to {B}\in {S}$
10 srgbinomlem.c
11 srgbinomlem.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
12 srgbinomlem.i
13 12 adantl
14 13 oveq1d
15 srgcmn ${⊢}{R}\in \mathrm{SRing}\to {R}\in \mathrm{CMnd}$
16 7 15 syl ${⊢}{\phi }\to {R}\in \mathrm{CMnd}$
17 simpl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {\phi }$
18 elfzelz ${⊢}{k}\in \left(0\dots {N}+1\right)\to {k}\in ℤ$
19 bccl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in ℤ\right)\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)\in {ℕ}_{0}$
20 11 18 19 syl2an ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)\in {ℕ}_{0}$
21 fznn0sub ${⊢}{k}\in \left(0\dots {N}+1\right)\to {N}+1-{k}\in {ℕ}_{0}$
22 21 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {N}+1-{k}\in {ℕ}_{0}$
23 elfznn0 ${⊢}{k}\in \left(0\dots {N}+1\right)\to {k}\in {ℕ}_{0}$
24 23 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}\in {ℕ}_{0}$
25 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2
26 17 20 22 24 25 syl13anc
27 1 4 16 11 26 gsummptfzsplit
28 srgmnd ${⊢}{R}\in \mathrm{SRing}\to {R}\in \mathrm{Mnd}$
29 7 28 syl ${⊢}{\phi }\to {R}\in \mathrm{Mnd}$
30 ovexd ${⊢}{\phi }\to {N}+1\in \mathrm{V}$
31 id ${⊢}{\phi }\to {\phi }$
32 11 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
33 32 peano2zd ${⊢}{\phi }\to {N}+1\in ℤ$
34 bccl ${⊢}\left({N}\in {ℕ}_{0}\wedge {N}+1\in ℤ\right)\to \left(\genfrac{}{}{0}{}{{N}}{{N}+1}\right)\in {ℕ}_{0}$
35 11 33 34 syl2anc ${⊢}{\phi }\to \left(\genfrac{}{}{0}{}{{N}}{{N}+1}\right)\in {ℕ}_{0}$
36 11 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
37 peano2cn ${⊢}{N}\in ℂ\to {N}+1\in ℂ$
38 36 37 syl ${⊢}{\phi }\to {N}+1\in ℂ$
39 38 subidd ${⊢}{\phi }\to {N}+1-\left({N}+1\right)=0$
40 0nn0 ${⊢}0\in {ℕ}_{0}$
41 39 40 eqeltrdi ${⊢}{\phi }\to {N}+1-\left({N}+1\right)\in {ℕ}_{0}$
42 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
43 11 42 syl ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
44 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2
45 31 35 41 43 44 syl13anc
46 oveq2 ${⊢}{k}={N}+1\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)=\left(\genfrac{}{}{0}{}{{N}}{{N}+1}\right)$
47 oveq2 ${⊢}{k}={N}+1\to {N}+1-{k}={N}+1-\left({N}+1\right)$
48 47 oveq1d
49 oveq1
50 48 49 oveq12d
51 46 50 oveq12d
52 1 51 gsumsn
53 29 30 45 52 syl3anc
54 11 nn0red ${⊢}{\phi }\to {N}\in ℝ$
55 54 ltp1d ${⊢}{\phi }\to {N}<{N}+1$
56 55 olcd ${⊢}{\phi }\to \left({N}+1<0\vee {N}<{N}+1\right)$
57 bcval4 ${⊢}\left({N}\in {ℕ}_{0}\wedge {N}+1\in ℤ\wedge \left({N}+1<0\vee {N}<{N}+1\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{N}+1}\right)=0$
58 11 33 56 57 syl3anc ${⊢}{\phi }\to \left(\genfrac{}{}{0}{}{{N}}{{N}+1}\right)=0$
59 58 oveq1d
60 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem1
61 31 41 43 60 syl12anc
62 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
63 1 62 3 mulg0
64 61 63 syl
65 53 59 64 3eqtrd
66 65 oveq2d
67 fzfid ${⊢}{\phi }\to \left(0\dots {N}\right)\in \mathrm{Fin}$
68 simpl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {\phi }$
69 bccl2 ${⊢}{k}\in \left(0\dots {N}\right)\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)\in ℕ$
70 69 nnnn0d ${⊢}{k}\in \left(0\dots {N}\right)\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)\in {ℕ}_{0}$
71 70 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{k}}\right)\in {ℕ}_{0}$
72 fzelp1 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in \left(0\dots {N}+1\right)$
73 72 22 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {N}+1-{k}\in {ℕ}_{0}$
74 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
75 74 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in {ℕ}_{0}$
76 68 71 73 75 25 syl13anc
77 76 ralrimiva
78 1 16 67 77 gsummptcl
79 1 4 62 mndrid
80 29 78 79 syl2anc
81 27 66 80 3eqtrd
82 7 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {R}\in \mathrm{SRing}$
83 8 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}\in {S}$
84 9 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {B}\in {S}$
85 10 adantr
86 fznn0sub ${⊢}{k}\in \left(0\dots {N}\right)\to {N}-{k}\in {ℕ}_{0}$
87 86 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {N}-{k}\in {ℕ}_{0}$
88 1 2 5 6 82 83 84 75 85 87 3 71 srgpcomppsc
89 36 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {N}\in ℂ$
90 1cnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to 1\in ℂ$
91 elfzelz ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in ℤ$
92 91 zcnd ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in ℂ$
93 92 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in ℂ$
94 89 90 93 addsubd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {N}+1-{k}={N}-{k}+1$
95 94 oveq1d
96 95 oveq1d
97 96 oveq2d
98 88 97 eqtr4d
99 98 mpteq2dva
100 99 oveq2d
101 ovexd ${⊢}{\phi }\to \left(0\dots {N}\right)\in \mathrm{V}$
102 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2
103 68 71 87 75 102 syl13anc
104 eqid
105 ovexd
106 fvexd ${⊢}{\phi }\to {0}_{{R}}\in \mathrm{V}$
107 104 67 105 106 fsuppmptdm
108 1 62 4 2 7 101 8 103 107 srgsummulcr
109 81 100 108 3eqtr2rd
110 109 adantr
111 14 110 eqtrd