Step | Hyp | Ref
| Expression |
1 | | srgbinomlem.i |
. . 3
โข (๐ โ (๐ โ (๐ด + ๐ต)) = (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
2 | 1 | oveq1d 7373 |
. 2
โข (๐ โ ((๐ โ (๐ด + ๐ต)) ร ๐ต) = ((๐
ฮฃg (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) ร ๐ต)) |
3 | | srgbinom.s |
. . . 4
โข ๐ = (Baseโ๐
) |
4 | | eqid 2733 |
. . . 4
โข
(0gโ๐
) = (0gโ๐
) |
5 | | srgbinom.a |
. . . 4
โข + =
(+gโ๐
) |
6 | | srgbinom.m |
. . . 4
โข ร =
(.rโ๐
) |
7 | | srgbinomlem.r |
. . . 4
โข (๐ โ ๐
โ SRing) |
8 | | ovexd 7393 |
. . . 4
โข (๐ โ (0...๐) โ V) |
9 | | srgbinomlem.b |
. . . 4
โข (๐ โ ๐ต โ ๐) |
10 | | simpl 484 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ ๐) |
11 | | srgbinomlem.n |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
12 | | elfzelz 13447 |
. . . . . 6
โข (๐ โ (0...๐) โ ๐ โ โค) |
13 | | bccl 14228 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
14 | 11, 12, 13 | syl2an 597 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ (๐C๐) โ
โ0) |
15 | | fznn0sub 13479 |
. . . . . 6
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
16 | 15 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ (๐ โ ๐) โ
โ0) |
17 | | elfznn0 13540 |
. . . . . 6
โข (๐ โ (0...๐) โ ๐ โ โ0) |
18 | 17 | adantl 483 |
. . . . 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 19963 |
. . . . 5
โข ((๐ โง ((๐C๐) โ โ0 โง (๐ โ ๐) โ โ0 โง ๐ โ โ0))
โ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
25 | 10, 14, 16, 18, 24 | syl13anc 1373 |
. . . 4
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
26 | | eqid 2733 |
. . . . 5
โข (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)))) = (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)))) |
27 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...๐) โ Fin) |
28 | | ovexd 7393 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ V) |
29 | | fvexd 6858 |
. . . . 5
โข (๐ โ (0gโ๐
) โ V) |
30 | 26, 27, 28, 29 | fsuppmptdm 9321 |
. . . 4
โข (๐ โ (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)))) finSupp (0gโ๐
)) |
31 | 3, 4, 5, 6, 7, 8, 9, 25, 30 | srgsummulcr 19959 |
. . 3
โข (๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต))) = ((๐
ฮฃg (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) ร ๐ต)) |
32 | | srgcmn 19925 |
. . . . . 6
โข (๐
โ SRing โ ๐
โ CMnd) |
33 | 7, 32 | syl 17 |
. . . . 5
โข (๐ โ ๐
โ CMnd) |
34 | | 1z 12538 |
. . . . . 6
โข 1 โ
โค |
35 | 34 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ
โค) |
36 | | 0zd 12516 |
. . . . 5
โข (๐ โ 0 โ
โค) |
37 | 11 | nn0zd 12530 |
. . . . 5
โข (๐ โ ๐ โ โค) |
38 | 7 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ๐
โ SRing) |
39 | 9 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ๐ต โ ๐) |
40 | 3, 6 | srgcl 19929 |
. . . . . 6
โข ((๐
โ SRing โง ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐ โง ๐ต โ ๐) โ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต) โ ๐) |
41 | 38, 25, 39, 40 | syl3anc 1372 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต) โ ๐) |
42 | | oveq2 7366 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ (๐C๐) = (๐C(๐ โ 1))) |
43 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = (๐ โ 1) โ (๐ โ ๐) = (๐ โ (๐ โ 1))) |
44 | 43 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = (๐ โ 1) โ ((๐ โ ๐) โ ๐ด) = ((๐ โ (๐ โ 1)) โ ๐ด)) |
45 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = (๐ โ 1) โ (๐ โ ๐ต) = ((๐ โ 1) โ ๐ต)) |
46 | 44, 45 | oveq12d 7376 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)) = (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) |
47 | 42, 46 | oveq12d 7376 |
. . . . . 6
โข (๐ = (๐ โ 1) โ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) = ((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต)))) |
48 | 47 | oveq1d 7373 |
. . . . 5
โข (๐ = (๐ โ 1) โ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต) = (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต)) |
49 | 3, 4, 33, 35, 36, 37, 41, 48 | gsummptshft 19718 |
. . . 4
โข (๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต))) = (๐
ฮฃg (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต)))) |
50 | 11 | nn0cnd 12480 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
51 | 50 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โ) |
52 | | elfzelz 13447 |
. . . . . . . . . . . . . 14
โข (๐ โ ((0 + 1)...(๐ + 1)) โ ๐ โ โค) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โค) |
54 | 53 | zcnd 12613 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โ) |
55 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ 1 โ
โ) |
56 | 51, 54, 55 | subsub3d 11547 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐ โ (๐ โ 1)) = ((๐ + 1) โ ๐)) |
57 | 56 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ โ (๐ โ 1)) โ ๐ด) = (((๐ + 1) โ ๐) โ ๐ด)) |
58 | 57 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต)) = ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) |
59 | 58 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) = ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต)))) |
60 | 59 | oveq1d 7373 |
. . . . . . 7
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต) = (((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต)) |
61 | 7 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐
โ SRing) |
62 | | peano2zm 12551 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
63 | 52, 62 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((0 + 1)...(๐ + 1)) โ (๐ โ 1) โ
โค) |
64 | | bccl 14228 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง (๐ โ 1) โ
โค) โ (๐C(๐ โ 1)) โ
โ0) |
65 | 11, 63, 64 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐C(๐ โ 1)) โ
โ0) |
66 | 20, 3 | mgpbas 19907 |
. . . . . . . . . . 11
โข ๐ = (Baseโ๐บ) |
67 | 20 | srgmgp 19927 |
. . . . . . . . . . . . 13
โข (๐
โ SRing โ ๐บ โ Mnd) |
68 | 7, 67 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐บ โ Mnd) |
69 | 68 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐บ โ Mnd) |
70 | | 0p1e1 12280 |
. . . . . . . . . . . . . . 15
โข (0 + 1) =
1 |
71 | 70 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((0 +
1)...(๐ + 1)) = (1...(๐ + 1)) |
72 | 71 | eleq2i 2826 |
. . . . . . . . . . . . 13
โข (๐ โ ((0 + 1)...(๐ + 1)) โ ๐ โ (1...(๐ + 1))) |
73 | | fznn0sub 13479 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0) |
74 | 73 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (1...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0)) |
75 | 72, 74 | biimtrid 241 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ ((0 + 1)...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0)) |
76 | 75 | imp 408 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ + 1) โ ๐) โ
โ0) |
77 | 22 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ด โ ๐) |
78 | 66, 21, 69, 76, 77 | mulgnn0cld 18902 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐ + 1) โ ๐) โ ๐ด) โ ๐) |
79 | | elfznn 13476 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โ) |
80 | | nnm1nn0 12459 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (1...(๐ + 1)) โ (๐ โ 1) โ
โ0) |
82 | 72, 81 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ ((0 + 1)...(๐ + 1)) โ (๐ โ 1) โ
โ0) |
83 | 82 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐ โ 1) โ
โ0) |
84 | 9 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ต โ ๐) |
85 | 66, 21, 69, 83, 84 | mulgnn0cld 18902 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ โ 1) โ ๐ต) โ ๐) |
86 | 3, 19, 6 | srgmulgass 19953 |
. . . . . . . . . 10
โข ((๐
โ SRing โง ((๐C(๐ โ 1)) โ โ0 โง
(((๐ + 1) โ ๐) โ ๐ด) โ ๐ โง ((๐ โ 1) โ ๐ต) โ ๐)) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) = ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต)))) |
87 | 61, 65, 78, 85, 86 | syl13anc 1373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) = ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต)))) |
88 | 87 | eqcomd 2739 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต))) |
89 | 88 | oveq1d 7373 |
. . . . . . 7
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต) = ((((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) ร ๐ต)) |
90 | | srgmnd 19926 |
. . . . . . . . . . . 12
โข (๐
โ SRing โ ๐
โ Mnd) |
91 | 7, 90 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ Mnd) |
92 | 91 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐
โ Mnd) |
93 | 3, 19, 92, 65, 78 | mulgnn0cld 18902 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) โ ๐) |
94 | 3, 6 | srgass 19930 |
. . . . . . . . 9
โข ((๐
โ SRing โง (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) โ ๐ โง ((๐ โ 1) โ ๐ต) โ ๐ โง ๐ต โ ๐)) โ ((((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) ร ๐ต) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (((๐ โ 1) โ ๐ต) ร ๐ต))) |
95 | 61, 93, 85, 84, 94 | syl13anc 1373 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) ร ๐ต) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (((๐ โ 1) โ ๐ต) ร ๐ต))) |
96 | 20, 6 | mgpplusg 19905 |
. . . . . . . . . . . 12
โข ร =
(+gโ๐บ) |
97 | 66, 21, 96 | mulgnn0p1 18892 |
. . . . . . . . . . 11
โข ((๐บ โ Mnd โง (๐ โ 1) โ
โ0 โง ๐ต
โ ๐) โ (((๐ โ 1) + 1) โ ๐ต) = (((๐ โ 1) โ ๐ต) ร ๐ต)) |
98 | 97 | eqcomd 2739 |
. . . . . . . . . 10
โข ((๐บ โ Mnd โง (๐ โ 1) โ
โ0 โง ๐ต
โ ๐) โ (((๐ โ 1) โ ๐ต) ร ๐ต) = (((๐ โ 1) + 1) โ ๐ต)) |
99 | 69, 83, 84, 98 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐ โ 1) โ ๐ต) ร ๐ต) = (((๐ โ 1) + 1) โ ๐ต)) |
100 | 99 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (((๐ โ 1) โ ๐ต) ร ๐ต)) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (((๐ โ 1) + 1) โ ๐ต))) |
101 | 52 | zcnd 12613 |
. . . . . . . . . . . 12
โข (๐ โ ((0 + 1)...(๐ + 1)) โ ๐ โ โ) |
102 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข (๐ โ ((0 + 1)...(๐ + 1)) โ 1 โ
โ) |
103 | 101, 102 | npcand 11521 |
. . . . . . . . . . 11
โข (๐ โ ((0 + 1)...(๐ + 1)) โ ((๐ โ 1) + 1) = ๐) |
104 | 103 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ โ 1) + 1) = ๐) |
105 | 104 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐ โ 1) + 1) โ ๐ต) = (๐ โ ๐ต)) |
106 | 105 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (((๐ โ 1) + 1) โ ๐ต)) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
107 | 95, 100, 106 | 3eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร ((๐ โ 1) โ ๐ต)) ร ๐ต) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
108 | 60, 89, 107 | 3eqtrd 2777 |
. . . . . 6
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
109 | 108 | mpteq2dva 5206 |
. . . . 5
โข (๐ โ (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต)) = (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) |
110 | 109 | oveq2d 7374 |
. . . 4
โข (๐ โ (๐
ฮฃg (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ โ (๐ โ 1)) โ ๐ด) ร ((๐ โ 1) โ ๐ต))) ร ๐ต))) = (๐
ฮฃg (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))))) |
111 | 71 | mpteq1i 5202 |
. . . . . . 7
โข (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) = (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
112 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
113 | 112 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐C(๐ โ 1)) = (๐C(๐ โ 1))) |
114 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ + 1) โ ๐) = ((๐ + 1) โ ๐)) |
115 | 114 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((๐ + 1) โ ๐) โ ๐ด) = (((๐ + 1) โ ๐) โ ๐ด)) |
116 | 113, 115 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) = ((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด))) |
117 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐ต) = (๐ โ ๐ต)) |
118 | 116, 117 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)) = (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
119 | 118 | cbvmptv 5219 |
. . . . . . 7
โข (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) = (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
120 | 111, 119 | eqtri 2761 |
. . . . . 6
โข (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) = (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) |
121 | 120 | oveq2i 7369 |
. . . . 5
โข (๐
ฮฃg
(๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) = (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) |
122 | | fzfid 13884 |
. . . . . . . . 9
โข (๐ โ (1...(๐ + 1)) โ Fin) |
123 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐) |
124 | | elfzelz 13447 |
. . . . . . . . . . . . 13
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โค) |
125 | | peano2zm 12551 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (1...(๐ + 1)) โ (๐ โ 1) โ โค) |
127 | | bccl 14228 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง (๐ โ 1) โ
โค) โ (๐C(๐ โ 1)) โ
โ0) |
128 | 11, 126, 127 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (๐C(๐ โ 1)) โ
โ0) |
129 | | fznn0sub 13479 |
. . . . . . . . . . . 12
โข (๐ โ (1...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0) |
130 | 129 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ((๐ + 1) โ ๐) โ
โ0) |
131 | | elfznn 13476 |
. . . . . . . . . . . . 13
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โ) |
132 | 131 | nnnn0d 12478 |
. . . . . . . . . . . 12
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โ0) |
133 | 132 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐ โ โ0) |
134 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19963 |
. . . . . . . . . . 11
โข ((๐ โง ((๐C(๐ โ 1)) โ โ0 โง
((๐ + 1) โ ๐) โ โ0
โง ๐ โ
โ0)) โ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
135 | 123, 128,
130, 133, 134 | syl13anc 1373 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
136 | 135 | ralrimiva 3140 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (1...(๐ + 1))((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
137 | 3, 33, 122, 136 | gsummptcl 19749 |
. . . . . . . 8
โข (๐ โ (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) โ ๐) |
138 | 3, 5, 4 | mndlid 18581 |
. . . . . . . 8
โข ((๐
โ Mnd โง (๐
ฮฃg
(๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) โ ๐) โ ((0gโ๐
) + (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) = (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
139 | 91, 137, 138 | syl2anc 585 |
. . . . . . 7
โข (๐ โ
((0gโ๐
)
+ (๐
ฮฃg
(๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) = (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
140 | | 0nn0 12433 |
. . . . . . . . . . 11
โข 0 โ
โ0 |
141 | 140 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ0) |
142 | | id 22 |
. . . . . . . . . . 11
โข (๐ โ ๐) |
143 | | 0z 12515 |
. . . . . . . . . . . . . 14
โข 0 โ
โค |
144 | 143, 34 | pm3.2i 472 |
. . . . . . . . . . . . 13
โข (0 โ
โค โง 1 โ โค) |
145 | | zsubcl 12550 |
. . . . . . . . . . . . 13
โข ((0
โ โค โง 1 โ โค) โ (0 โ 1) โ
โค) |
146 | 144, 145 | mp1i 13 |
. . . . . . . . . . . 12
โข (๐ โ (0 โ 1) โ
โค) |
147 | | bccl 14228 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง (0 โ 1) โ โค) โ (๐C(0 โ 1)) โ
โ0) |
148 | 11, 146, 147 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐C(0 โ 1)) โ
โ0) |
149 | | nn0cn 12428 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ๐ โ
โ) |
150 | | peano2cn 11332 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ + 1) โ
โ) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
152 | 151 | subid1d 11506 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ((๐ + 1) โ 0)
= (๐ + 1)) |
153 | | peano2nn0 12458 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
154 | 152, 153 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ((๐ + 1) โ 0)
โ โ0) |
155 | 11, 154 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1) โ 0) โ
โ0) |
156 | 3, 6, 19, 5, 20, 21, 7, 22, 9, 23, 11 | srgbinomlem2 19963 |
. . . . . . . . . . 11
โข ((๐ โง ((๐C(0 โ 1)) โ โ0
โง ((๐ + 1) โ 0)
โ โ0 โง 0 โ โ0)) โ ((๐C(0 โ 1)) ยท
((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐) |
157 | 142, 148,
155, 141, 156 | syl13anc 1373 |
. . . . . . . . . 10
โข (๐ โ ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐) |
158 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (๐ โ 1) = (0 โ 1)) |
159 | 158 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (๐C(๐ โ 1)) = (๐C(0 โ 1))) |
160 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = 0 โ ((๐ + 1) โ ๐) = ((๐ + 1) โ 0)) |
161 | 160 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (((๐ + 1) โ ๐) โ ๐ด) = (((๐ + 1) โ 0) โ ๐ด)) |
162 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (๐ โ ๐ต) = (0 โ ๐ต)) |
163 | 161, 162 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ = 0 โ ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)) = ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) |
164 | 159, 163 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = 0 โ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) = ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)))) |
165 | 3, 164 | gsumsn 19736 |
. . . . . . . . . 10
โข ((๐
โ Mnd โง 0 โ
โ0 โง ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐) โ (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) = ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)))) |
166 | 91, 141, 157, 165 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ โ (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) = ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)))) |
167 | | 0lt1 11682 |
. . . . . . . . . . . . . . 15
โข 0 <
1 |
168 | 167 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < 1) |
169 | 168, 70 | breqtrrdi 5148 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < (0 +
1)) |
170 | | 0re 11162 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ |
171 | | 1re 11160 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
172 | 170, 171,
170 | 3pm3.2i 1340 |
. . . . . . . . . . . . . 14
โข (0 โ
โ โง 1 โ โ โง 0 โ โ) |
173 | | ltsubadd 11630 |
. . . . . . . . . . . . . 14
โข ((0
โ โ โง 1 โ โ โง 0 โ โ) โ ((0
โ 1) < 0 โ 0 < (0 + 1))) |
174 | 172, 173 | mp1i 13 |
. . . . . . . . . . . . 13
โข (๐ โ ((0 โ 1) < 0
โ 0 < (0 + 1))) |
175 | 169, 174 | mpbird 257 |
. . . . . . . . . . . 12
โข (๐ โ (0 โ 1) <
0) |
176 | 175 | orcd 872 |
. . . . . . . . . . 11
โข (๐ โ ((0 โ 1) < 0 โจ
๐ < (0 โ
1))) |
177 | | bcval4 14213 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง (0 โ 1) โ โค โง ((0 โ 1) < 0 โจ ๐ < (0 โ 1))) โ
(๐C(0 โ 1)) =
0) |
178 | 11, 146, 176, 177 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ (๐C(0 โ 1)) = 0) |
179 | 178 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) = (0 ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)))) |
180 | 66, 21, 68, 155, 22 | mulgnn0cld 18902 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + 1) โ 0) โ ๐ด) โ ๐) |
181 | 66, 21, 68, 141, 9 | mulgnn0cld 18902 |
. . . . . . . . . . 11
โข (๐ โ (0 โ ๐ต) โ ๐) |
182 | 3, 6 | srgcl 19929 |
. . . . . . . . . . 11
โข ((๐
โ SRing โง (((๐ + 1) โ 0) โ ๐ด) โ ๐ โง (0 โ ๐ต) โ ๐) โ ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)) โ ๐) |
183 | 7, 180, 181, 182 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต)) โ ๐) |
184 | 3, 4, 19 | mulg0 18884 |
. . . . . . . . . 10
โข
(((((๐ + 1) โ
0) โ
๐ด) ร (0 โ ๐ต)) โ ๐ โ (0 ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) = (0gโ๐
)) |
185 | 183, 184 | syl 17 |
. . . . . . . . 9
โข (๐ โ (0 ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) = (0gโ๐
)) |
186 | 166, 179,
185 | 3eqtrrd 2778 |
. . . . . . . 8
โข (๐ โ (0gโ๐
) = (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
187 | 186 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ
((0gโ๐
)
+ (๐
ฮฃg
(๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) = ((๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
188 | 139, 187 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) = ((๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
189 | 7 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐
โ SRing) |
190 | 68 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐บ โ Mnd) |
191 | 22 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐ด โ ๐) |
192 | 66, 21, 190, 130, 191 | mulgnn0cld 18902 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (((๐ + 1) โ ๐) โ ๐ด) โ ๐) |
193 | 9 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐ต โ ๐) |
194 | 66, 21, 190, 133, 193 | mulgnn0cld 18902 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (๐ โ ๐ต) โ ๐) |
195 | 3, 19, 6 | srgmulgass 19953 |
. . . . . . . . 9
โข ((๐
โ SRing โง ((๐C(๐ โ 1)) โ โ0 โง
(((๐ + 1) โ ๐) โ ๐ด) โ ๐ โง (๐ โ ๐ต) โ ๐)) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)) = ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))) |
196 | 189, 128,
192, 194, 195 | syl13anc 1373 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)) = ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))) |
197 | 196 | mpteq2dva 5206 |
. . . . . . 7
โข (๐ โ (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต))) = (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) |
198 | 197 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) = (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
199 | 11, 153 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ
โ0) |
200 | | simpl 484 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ๐) |
201 | | elfzelz 13447 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ + 1)) โ ๐ โ โค) |
202 | 201, 125 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ + 1)) โ (๐ โ 1) โ โค) |
203 | 11, 202, 127 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐C(๐ โ 1)) โ
โ0) |
204 | | fznn0sub 13479 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0) |
205 | 204 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ((๐ + 1) โ ๐) โ
โ0) |
206 | | elfznn0 13540 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ + 1)) โ ๐ โ โ0) |
207 | 206 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ๐ โ โ0) |
208 | 200, 203,
205, 207, 134 | syl13anc 1373 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
209 | 3, 5, 33, 199, 208 | gsummptfzsplitl 19715 |
. . . . . . 7
โข (๐ โ (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) = ((๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
210 | | snfi 8991 |
. . . . . . . . . 10
โข {0}
โ Fin |
211 | 210 | a1i 11 |
. . . . . . . . 9
โข (๐ โ {0} โ
Fin) |
212 | 164 | eleq1d 2819 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐ โ ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐)) |
213 | 212 | ralsng 4635 |
. . . . . . . . . . 11
โข (0 โ
โ0 โ (โ๐ โ {0} ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐ โ ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐)) |
214 | 140, 213 | ax-mp 5 |
. . . . . . . . . 10
โข
(โ๐ โ
{0} ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐ โ ((๐C(0 โ 1)) ยท ((((๐ + 1) โ 0) โ ๐ด) ร (0 โ ๐ต))) โ ๐) |
215 | 157, 214 | sylibr 233 |
. . . . . . . . 9
โข (๐ โ โ๐ โ {0} ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))) โ ๐) |
216 | 3, 33, 211, 215 | gsummptcl 19749 |
. . . . . . . 8
โข (๐ โ (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) โ ๐) |
217 | 3, 5 | cmncom 19585 |
. . . . . . . 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) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
218 | 33, 137, 216, 217 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ ((๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) = ((๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
219 | 209, 218 | eqtrd 2773 |
. . . . . 6
โข (๐ โ (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) = ((๐
ฮฃg (๐ โ {0} โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) + (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต))))))) |
220 | 188, 198,
219 | 3eqtr4d 2783 |
. . . . 5
โข (๐ โ (๐
ฮฃg (๐ โ (1...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) = (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
221 | 121, 220 | eqtrid 2785 |
. . . 4
โข (๐ โ (๐
ฮฃg (๐ โ ((0 + 1)...(๐ + 1)) โฆ (((๐C(๐ โ 1)) ยท (((๐ + 1) โ ๐) โ ๐ด)) ร (๐ โ ๐ต)))) = (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
222 | 49, 110, 221 | 3eqtrd 2777 |
. . 3
โข (๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ (((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))) ร ๐ต))) = (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
223 | 31, 222 | eqtr3d 2775 |
. 2
โข (๐ โ ((๐
ฮฃg (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต))))) ร ๐ต) = (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |
224 | 2, 223 | sylan9eqr 2795 |
1
โข ((๐ โง ๐) โ ((๐ โ (๐ด + ๐ต)) ร ๐ต) = (๐
ฮฃg (๐ โ (0...(๐ + 1)) โฆ ((๐C(๐ โ 1)) ยท ((((๐ + 1) โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) |