Proof of Theorem srgbinomlem3
Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . . 4
g |
2 | 1 | adantl 482 |
. . 3
g |
3 | 2 | oveq1d 6665 |
. 2
g
|
4 | | srgbinom.s |
. . . . . 6
|
5 | | srgbinom.a |
. . . . . 6
|
6 | | srgbinomlem.r |
. . . . . . 7
SRing |
7 | | srgcmn 18508 |
. . . . . . 7
SRing CMnd |
8 | 6, 7 | syl 17 |
. . . . . 6
CMnd |
9 | | srgbinomlem.n |
. . . . . 6
|
10 | | simpl 473 |
. . . . . . 7
|
11 | | elfzelz 12342 |
. . . . . . . 8
|
12 | | bccl 13109 |
. . . . . . . 8
|
13 | 9, 11, 12 | syl2an 494 |
. . . . . . 7
|
14 | | fznn0sub 12373 |
. . . . . . . 8
|
15 | 14 | adantl 482 |
. . . . . . 7
|
16 | | elfznn0 12433 |
. . . . . . . 8
|
17 | 16 | adantl 482 |
. . . . . . 7
|
18 | | srgbinom.m |
. . . . . . . 8
|
19 | | srgbinom.t |
. . . . . . . 8
.g |
20 | | srgbinom.g |
. . . . . . . 8
mulGrp |
21 | | srgbinom.e |
. . . . . . . 8
.g |
22 | | srgbinomlem.a |
. . . . . . . 8
|
23 | | srgbinomlem.b |
. . . . . . . 8
|
24 | | srgbinomlem.c |
. . . . . . . 8
|
25 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18541 |
. . . . . . 7
|
26 | 10, 13, 15, 17, 25 | syl13anc 1328 |
. . . . . 6
|
27 | 4, 5, 8, 9, 26 | gsummptfzsplit 18332 |
. . . . 5
g
g
g |
28 | | srgmnd 18509 |
. . . . . . . . 9
SRing |
29 | 6, 28 | syl 17 |
. . . . . . . 8
|
30 | | ovexd 6680 |
. . . . . . . 8
|
31 | | id 22 |
. . . . . . . . 9
|
32 | 9 | nn0zd 11480 |
. . . . . . . . . . 11
|
33 | 32 | peano2zd 11485 |
. . . . . . . . . 10
|
34 | | bccl 13109 |
. . . . . . . . . 10
|
35 | 9, 33, 34 | syl2anc 693 |
. . . . . . . . 9
|
36 | 9 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
37 | | peano2cn 10208 |
. . . . . . . . . . . 12
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
|
39 | 38 | subidd 10380 |
. . . . . . . . . 10
|
40 | | 0nn0 11307 |
. . . . . . . . . 10
|
41 | 39, 40 | syl6eqel 2709 |
. . . . . . . . 9
|
42 | | peano2nn0 11333 |
. . . . . . . . . 10
|
43 | 9, 42 | syl 17 |
. . . . . . . . 9
|
44 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18541 |
. . . . . . . . 9
|
45 | 31, 35, 41, 43, 44 | syl13anc 1328 |
. . . . . . . 8
|
46 | | oveq2 6658 |
. . . . . . . . . 10
|
47 | | oveq2 6658 |
. . . . . . . . . . . 12
|
48 | 47 | oveq1d 6665 |
. . . . . . . . . . 11
|
49 | | oveq1 6657 |
. . . . . . . . . . 11
|
50 | 48, 49 | oveq12d 6668 |
. . . . . . . . . 10
|
51 | 46, 50 | oveq12d 6668 |
. . . . . . . . 9
|
52 | 4, 51 | gsumsn 18354 |
. . . . . . . 8
g
|
53 | 29, 30, 45, 52 | syl3anc 1326 |
. . . . . . 7
g |
54 | 9 | nn0red 11352 |
. . . . . . . . . . 11
|
55 | 54 | ltp1d 10954 |
. . . . . . . . . 10
|
56 | 55 | olcd 408 |
. . . . . . . . 9
|
57 | | bcval4 13094 |
. . . . . . . . 9
|
58 | 9, 33, 56, 57 | syl3anc 1326 |
. . . . . . . 8
|
59 | 58 | oveq1d 6665 |
. . . . . . 7
|
60 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem1 18540 |
. . . . . . . . 9
|
61 | 31, 41, 43, 60 | syl12anc 1324 |
. . . . . . . 8
|
62 | | eqid 2622 |
. . . . . . . . 9
|
63 | 4, 62, 19 | mulg0 17546 |
. . . . . . . 8
|
64 | 61, 63 | syl 17 |
. . . . . . 7
|
65 | 53, 59, 64 | 3eqtrd 2660 |
. . . . . 6
g |
66 | 65 | oveq2d 6666 |
. . . . 5
g g g
|
67 | | fzfid 12772 |
. . . . . . 7
|
68 | | simpl 473 |
. . . . . . . . 9
|
69 | | bccl2 13110 |
. . . . . . . . . . 11
|
70 | 69 | nnnn0d 11351 |
. . . . . . . . . 10
|
71 | 70 | adantl 482 |
. . . . . . . . 9
|
72 | | fzelp1 12393 |
. . . . . . . . . 10
|
73 | 72, 15 | sylan2 491 |
. . . . . . . . 9
|
74 | | elfznn0 12433 |
. . . . . . . . . 10
|
75 | 74 | adantl 482 |
. . . . . . . . 9
|
76 | 68, 71, 73, 75, 25 | syl13anc 1328 |
. . . . . . . 8
|
77 | 76 | ralrimiva 2966 |
. . . . . . 7
|
78 | 4, 8, 67, 77 | gsummptcl 18366 |
. . . . . 6
g
|
79 | 4, 5, 62 | mndrid 17312 |
. . . . . 6
g
g
g |
80 | 29, 78, 79 | syl2anc 693 |
. . . . 5
g g |
81 | 27, 66, 80 | 3eqtrd 2660 |
. . . 4
g
g
|
82 | 6 | adantr 481 |
. . . . . . . 8
SRing |
83 | 22 | adantr 481 |
. . . . . . . 8
|
84 | 23 | adantr 481 |
. . . . . . . 8
|
85 | 24 | adantr 481 |
. . . . . . . 8
|
86 | | fznn0sub 12373 |
. . . . . . . . 9
|
87 | 86 | adantl 482 |
. . . . . . . 8
|
88 | 4, 18, 20, 21, 82, 83, 84, 75, 85, 87, 19, 71 | srgpcomppsc 18534 |
. . . . . . 7
|
89 | 36 | adantr 481 |
. . . . . . . . . . 11
|
90 | | 1cnd 10056 |
. . . . . . . . . . 11
|
91 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
92 | 91 | zcnd 11483 |
. . . . . . . . . . . 12
|
93 | 92 | adantl 482 |
. . . . . . . . . . 11
|
94 | 89, 90, 93 | addsubd 10413 |
. . . . . . . . . 10
|
95 | 94 | oveq1d 6665 |
. . . . . . . . 9
|
96 | 95 | oveq1d 6665 |
. . . . . . . 8
|
97 | 96 | oveq2d 6666 |
. . . . . . 7
|
98 | 88, 97 | eqtr4d 2659 |
. . . . . 6
|
99 | 98 | mpteq2dva 4744 |
. . . . 5
|
100 | 99 | oveq2d 6666 |
. . . 4
g
g
|
101 | | ovexd 6680 |
. . . . 5
|
102 | 4, 18, 19, 5, 20, 21, 6, 22, 23, 24, 9 | srgbinomlem2 18541 |
. . . . . 6
|
103 | 68, 71, 87, 75, 102 | syl13anc 1328 |
. . . . 5
|
104 | | eqid 2622 |
. . . . . 6
|
105 | | ovexd 6680 |
. . . . . 6
|
106 | | fvexd 6203 |
. . . . . 6
|
107 | 104, 67, 105, 106 | fsuppmptdm 8286 |
. . . . 5
finSupp |
108 | 4, 62, 5, 18, 6, 101, 22, 103, 107 | srgsummulcr 18537 |
. . . 4
g
g
|
109 | 81, 100, 108 | 3eqtr2rd 2663 |
. . 3
g
g |
110 | 109 | adantr 481 |
. 2
g
g |
111 | 3, 110 | eqtrd 2656 |
1
g |