Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
++ ++ |
2 | 1 | oveq2d 6666 |
. . 3
g ++
g ++ |
3 | | oveq2 6658 |
. . . . 5
g g |
4 | | eqid 2622 |
. . . . . 6
|
5 | 4 | gsum0 17278 |
. . . . 5
g |
6 | 3, 5 | syl6eq 2672 |
. . . 4
g |
7 | 6 | oveq1d 6665 |
. . 3
g g g |
8 | 2, 7 | eqeq12d 2637 |
. 2
g ++ g g
g ++ g |
9 | | oveq2 6658 |
. . . . 5
++ ++ |
10 | 9 | oveq2d 6666 |
. . . 4
g ++
g ++
|
11 | | oveq2 6658 |
. . . . . 6
g g |
12 | 11, 5 | syl6eq 2672 |
. . . . 5
g |
13 | 12 | oveq2d 6666 |
. . . 4
g g g |
14 | 10, 13 | eqeq12d 2637 |
. . 3
g ++ g g
g ++ g |
15 | | gsumwcl.b |
. . . . . 6
|
16 | | gsumccat.p |
. . . . . 6
|
17 | | simpl1 1064 |
. . . . . 6
Word
Word
|
18 | | lennncl 13325 |
. . . . . . . . . . 11
Word |
19 | 18 | 3ad2antl2 1224 |
. . . . . . . . . 10
Word
Word
|
20 | 19 | adantrr 753 |
. . . . . . . . 9
Word
Word |
21 | | lennncl 13325 |
. . . . . . . . . . 11
Word |
22 | 21 | 3ad2antl3 1225 |
. . . . . . . . . 10
Word
Word
|
23 | 22 | adantrl 752 |
. . . . . . . . 9
Word
Word |
24 | 20, 23 | nnaddcld 11067 |
. . . . . . . 8
Word
Word |
25 | | nnm1nn0 11334 |
. . . . . . . 8
|
26 | 24, 25 | syl 17 |
. . . . . . 7
Word
Word |
27 | | nn0uz 11722 |
. . . . . . 7
|
28 | 26, 27 | syl6eleq 2711 |
. . . . . 6
Word
Word |
29 | | simpl2 1065 |
. . . . . . . . 9
Word
Word
Word |
30 | | simpl3 1066 |
. . . . . . . . 9
Word
Word
Word |
31 | | ccatcl 13359 |
. . . . . . . . 9
Word
Word ++ Word |
32 | 29, 30, 31 | syl2anc 693 |
. . . . . . . 8
Word
Word ++ Word |
33 | | wrdf 13310 |
. . . . . . . 8
++ Word ++ ..^ ++ |
34 | 32, 33 | syl 17 |
. . . . . . 7
Word
Word ++ ..^ ++ |
35 | | ccatlen 13360 |
. . . . . . . . . . 11
Word
Word ++ |
36 | 29, 30, 35 | syl2anc 693 |
. . . . . . . . . 10
Word
Word ++ |
37 | 36 | oveq2d 6666 |
. . . . . . . . 9
Word
Word ..^ ++ ..^ |
38 | 20 | nnzd 11481 |
. . . . . . . . . . 11
Word
Word |
39 | 23 | nnzd 11481 |
. . . . . . . . . . 11
Word
Word |
40 | 38, 39 | zaddcld 11486 |
. . . . . . . . . 10
Word
Word |
41 | | fzoval 12471 |
. . . . . . . . . 10
..^ |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
Word
Word ..^ |
43 | 37, 42 | eqtrd 2656 |
. . . . . . . 8
Word
Word ..^ ++ |
44 | 43 | feq2d 6031 |
. . . . . . 7
Word
Word ++ ..^ ++ ++ |
45 | 34, 44 | mpbid 222 |
. . . . . 6
Word
Word ++ |
46 | 15, 16, 17, 28, 45 | gsumval2 17280 |
. . . . 5
Word
Word g ++ ++ |
47 | | nnm1nn0 11334 |
. . . . . . . . . 10
|
48 | 20, 47 | syl 17 |
. . . . . . . . 9
Word
Word |
49 | 48, 27 | syl6eleq 2711 |
. . . . . . . 8
Word
Word |
50 | | wrdf 13310 |
. . . . . . . . . 10
Word ..^ |
51 | 29, 50 | syl 17 |
. . . . . . . . 9
Word
Word ..^ |
52 | | fzoval 12471 |
. . . . . . . . . . 11
..^ |
53 | 38, 52 | syl 17 |
. . . . . . . . . 10
Word
Word ..^ |
54 | 53 | feq2d 6031 |
. . . . . . . . 9
Word
Word ..^
|
55 | 51, 54 | mpbid 222 |
. . . . . . . 8
Word
Word |
56 | 15, 16, 17, 49, 55 | gsumval2 17280 |
. . . . . . 7
Word
Word g |
57 | | nnm1nn0 11334 |
. . . . . . . . . 10
|
58 | 23, 57 | syl 17 |
. . . . . . . . 9
Word
Word |
59 | 58, 27 | syl6eleq 2711 |
. . . . . . . 8
Word
Word |
60 | | wrdf 13310 |
. . . . . . . . . 10
Word ..^ |
61 | 30, 60 | syl 17 |
. . . . . . . . 9
Word
Word ..^ |
62 | | fzoval 12471 |
. . . . . . . . . . 11
..^ |
63 | 39, 62 | syl 17 |
. . . . . . . . . 10
Word
Word ..^ |
64 | 63 | feq2d 6031 |
. . . . . . . . 9
Word
Word ..^
|
65 | 61, 64 | mpbid 222 |
. . . . . . . 8
Word
Word |
66 | 15, 16, 17, 59, 65 | gsumval2 17280 |
. . . . . . 7
Word
Word g |
67 | 56, 66 | oveq12d 6668 |
. . . . . 6
Word
Word g g
|
68 | 15, 16 | mndcl 17301 |
. . . . . . . . . 10
|
69 | 68 | 3expb 1266 |
. . . . . . . . 9
|
70 | 17, 69 | sylan 488 |
. . . . . . . 8
Word Word
|
71 | 15, 16 | mndass 17302 |
. . . . . . . . 9
|
72 | 17, 71 | sylan 488 |
. . . . . . . 8
Word Word
|
73 | | uzid 11702 |
. . . . . . . . . . 11
|
74 | 38, 73 | syl 17 |
. . . . . . . . . 10
Word
Word |
75 | | uzaddcl 11744 |
. . . . . . . . . 10
|
76 | 74, 58, 75 | syl2anc 693 |
. . . . . . . . 9
Word
Word |
77 | 20 | nncnd 11036 |
. . . . . . . . . 10
Word
Word |
78 | 23 | nncnd 11036 |
. . . . . . . . . 10
Word
Word |
79 | | 1cnd 10056 |
. . . . . . . . . 10
Word
Word |
80 | 77, 78, 79 | addsubassd 10412 |
. . . . . . . . 9
Word
Word |
81 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
82 | | npcan 10290 |
. . . . . . . . . . 11
|
83 | 77, 81, 82 | sylancl 694 |
. . . . . . . . . 10
Word
Word |
84 | 83 | fveq2d 6195 |
. . . . . . . . 9
Word
Word |
85 | 76, 80, 84 | 3eltr4d 2716 |
. . . . . . . 8
Word
Word |
86 | 45 | ffvelrnda 6359 |
. . . . . . . 8
Word Word
++ |
87 | 70, 72, 85, 49, 86 | seqsplit 12834 |
. . . . . . 7
Word
Word ++
++ ++ |
88 | | simpll2 1101 |
. . . . . . . . . 10
Word Word
Word |
89 | | simpll3 1102 |
. . . . . . . . . 10
Word Word
Word |
90 | 53 | eleq2d 2687 |
. . . . . . . . . . 11
Word
Word ..^
|
91 | 90 | biimpar 502 |
. . . . . . . . . 10
Word Word
..^ |
92 | | ccatval1 13361 |
. . . . . . . . . 10
Word
Word ..^ ++ |
93 | 88, 89, 91, 92 | syl3anc 1326 |
. . . . . . . . 9
Word Word
++ |
94 | 49, 93 | seqfveq 12825 |
. . . . . . . 8
Word
Word ++
|
95 | 77 | addid2d 10237 |
. . . . . . . . . . . 12
Word
Word |
96 | 83, 95 | eqtr4d 2659 |
. . . . . . . . . . 11
Word
Word |
97 | 96 | seqeq1d 12807 |
. . . . . . . . . 10
Word
Word ++ ++ |
98 | 77, 78 | addcomd 10238 |
. . . . . . . . . . . 12
Word
Word |
99 | 98 | oveq1d 6665 |
. . . . . . . . . . 11
Word
Word |
100 | 78, 77, 79 | addsubd 10413 |
. . . . . . . . . . 11
Word
Word |
101 | 99, 100 | eqtrd 2656 |
. . . . . . . . . 10
Word
Word |
102 | 97, 101 | fveq12d 6197 |
. . . . . . . . 9
Word
Word ++ ++ |
103 | | simpll2 1101 |
. . . . . . . . . . . 12
Word Word
Word |
104 | | simpll3 1102 |
. . . . . . . . . . . 12
Word Word
Word |
105 | 63 | eleq2d 2687 |
. . . . . . . . . . . . 13
Word
Word ..^
|
106 | 105 | biimpar 502 |
. . . . . . . . . . . 12
Word Word
..^ |
107 | | ccatval3 13363 |
. . . . . . . . . . . 12
Word
Word ..^ ++ |
108 | 103, 104,
106, 107 | syl3anc 1326 |
. . . . . . . . . . 11
Word Word
++ |
109 | 108 | eqcomd 2628 |
. . . . . . . . . 10
Word Word
++ |
110 | 59, 38, 109 | seqshft2 12827 |
. . . . . . . . 9
Word
Word ++ |
111 | 102, 110 | eqtr4d 2659 |
. . . . . . . 8
Word
Word ++ |
112 | 94, 111 | oveq12d 6668 |
. . . . . . 7
Word
Word
++ ++
|
113 | 87, 112 | eqtrd 2656 |
. . . . . 6
Word
Word ++
|
114 | 67, 113 | eqtr4d 2659 |
. . . . 5
Word
Word g g ++ |
115 | 46, 114 | eqtr4d 2659 |
. . . 4
Word
Word g ++ g g |
116 | 115 | anassrs 680 |
. . 3
Word Word
g ++
g g |
117 | | simpl2 1065 |
. . . . . 6
Word
Word
Word |
118 | | ccatrid 13370 |
. . . . . 6
Word ++ |
119 | 117, 118 | syl 17 |
. . . . 5
Word
Word
++ |
120 | 119 | oveq2d 6666 |
. . . 4
Word
Word
g ++ g |
121 | | simpl1 1064 |
. . . . 5
Word
Word
|
122 | 15 | gsumwcl 17377 |
. . . . . . 7
Word g |
123 | 122 | 3adant3 1081 |
. . . . . 6
Word Word g |
124 | 123 | adantr 481 |
. . . . 5
Word
Word
g |
125 | 15, 16, 4 | mndrid 17312 |
. . . . 5
g
g g |
126 | 121, 124,
125 | syl2anc 693 |
. . . 4
Word
Word
g g |
127 | 120, 126 | eqtr4d 2659 |
. . 3
Word
Word
g ++ g |
128 | 14, 116, 127 | pm2.61ne 2879 |
. 2
Word
Word
g ++ g g |
129 | | ccatlid 13369 |
. . . . 5
Word ++ |
130 | 129 | 3ad2ant3 1084 |
. . . 4
Word Word ++ |
131 | 130 | oveq2d 6666 |
. . 3
Word Word g
++ g |
132 | | simp1 1061 |
. . . 4
Word Word |
133 | 15 | gsumwcl 17377 |
. . . . 5
Word g |
134 | 133 | 3adant2 1080 |
. . . 4
Word Word g |
135 | 15, 16, 4 | mndlid 17311 |
. . . 4
g
g g |
136 | 132, 134,
135 | syl2anc 693 |
. . 3
Word Word
g g |
137 | 131, 136 | eqtr4d 2659 |
. 2
Word Word g
++ g |
138 | 8, 128, 137 | pm2.61ne 2879 |
1
Word Word g ++ g g |