Step |
Hyp |
Ref |
Expression |
1 |
|
gsumpart.b |
|
2 |
|
gsumpart.z |
|
3 |
|
gsumpart.g |
|
4 |
|
gsumpart.a |
|
5 |
|
gsumpart.x |
|
6 |
|
gsumpart.f |
|
7 |
|
gsumpart.w |
|
8 |
|
gsumpart.1 |
|
9 |
|
gsumpart.2 |
|
10 |
|
eqid |
|
11 |
10 4 5 8 9
|
2ndresdjuf1o |
|
12 |
1 2 3 4 6 7 11
|
gsumf1o |
|
13 |
|
snex |
|
14 |
13
|
a1i |
|
15 |
4
|
adantr |
|
16 |
|
ssidd |
|
17 |
9 16
|
eqsstrd |
|
18 |
|
iunss |
|
19 |
17 18
|
sylib |
|
20 |
19
|
r19.21bi |
|
21 |
15 20
|
ssexd |
|
22 |
14 21
|
xpexd |
|
23 |
22
|
ralrimiva |
|
24 |
|
iunexg |
|
25 |
5 23 24
|
syl2anc |
|
26 |
|
relxp |
|
27 |
26
|
a1i |
|
28 |
27
|
ralrimiva |
|
29 |
|
reliun |
|
30 |
28 29
|
sylibr |
|
31 |
|
dmiun |
|
32 |
|
dmxpss |
|
33 |
32
|
rgenw |
|
34 |
|
ss2iun |
|
35 |
33 34
|
ax-mp |
|
36 |
31 35
|
eqsstri |
|
37 |
|
iunid |
|
38 |
36 37
|
sseqtri |
|
39 |
38
|
a1i |
|
40 |
|
fo2nd |
|
41 |
|
fof |
|
42 |
40 41
|
ax-mp |
|
43 |
|
ssv |
|
44 |
|
fssres |
|
45 |
42 43 44
|
mp2an |
|
46 |
|
ffn |
|
47 |
45 46
|
mp1i |
|
48 |
|
djussxp2 |
|
49 |
|
imass2 |
|
50 |
48 49
|
ax-mp |
|
51 |
|
ima0 |
|
52 |
|
xpeq1 |
|
53 |
|
0xp |
|
54 |
52 53
|
eqtrdi |
|
55 |
54
|
imaeq2d |
|
56 |
|
iuneq1 |
|
57 |
|
0iun |
|
58 |
56 57
|
eqtrdi |
|
59 |
51 55 58
|
3eqtr4a |
|
60 |
59
|
adantl |
|
61 |
|
2ndimaxp |
|
62 |
61
|
adantl |
|
63 |
60 62
|
pm2.61dane |
|
64 |
63 9
|
eqtrd |
|
65 |
50 64
|
sseqtrid |
|
66 |
|
resssxp |
|
67 |
65 66
|
sylib |
|
68 |
|
dff2 |
|
69 |
47 67 68
|
sylanbrc |
|
70 |
6 69
|
fcod |
|
71 |
10 4 5 8 9
|
2ndresdju |
|
72 |
2
|
fvexi |
|
73 |
72
|
a1i |
|
74 |
6 4
|
fexd |
|
75 |
7 71 73 74
|
fsuppco |
|
76 |
1 2 3 25 30 5 39 70 75
|
gsum2d |
|
77 |
|
nfcsb1v |
|
78 |
|
csbeq1a |
|
79 |
5 21 77 78
|
iunsnima2 |
|
80 |
|
df-ov |
|
81 |
69
|
ad2antrr |
|
82 |
|
simplr |
|
83 |
|
vsnid |
|
84 |
83
|
a1i |
|
85 |
79
|
eleq2d |
|
86 |
85
|
biimpa |
|
87 |
84 86
|
opelxpd |
|
88 |
|
nfcv |
|
89 |
88 77
|
nfxp |
|
90 |
89
|
nfel2 |
|
91 |
|
sneq |
|
92 |
91 78
|
xpeq12d |
|
93 |
92
|
eleq2d |
|
94 |
90 93
|
rspce |
|
95 |
82 87 94
|
syl2anc |
|
96 |
|
eliun |
|
97 |
95 96
|
sylibr |
|
98 |
81 97
|
fvco3d |
|
99 |
97
|
fvresd |
|
100 |
|
vex |
|
101 |
|
vex |
|
102 |
100 101
|
op2nd |
|
103 |
99 102
|
eqtrdi |
|
104 |
103
|
fveq2d |
|
105 |
98 104
|
eqtrd |
|
106 |
80 105
|
syl5eq |
|
107 |
79 106
|
mpteq12dva |
|
108 |
6
|
adantr |
|
109 |
|
imassrn |
|
110 |
9
|
xpeq2d |
|
111 |
48 110
|
sseqtrid |
|
112 |
|
rnss |
|
113 |
111 112
|
syl |
|
114 |
113
|
adantr |
|
115 |
|
rnxpss |
|
116 |
114 115
|
sstrdi |
|
117 |
109 116
|
sstrid |
|
118 |
79 117
|
eqsstrrd |
|
119 |
108 118
|
feqresmpt |
|
120 |
107 119
|
eqtr4d |
|
121 |
120
|
oveq2d |
|
122 |
121
|
mpteq2dva |
|
123 |
|
nfcv |
|
124 |
|
nfcv |
|
125 |
|
nfcv |
|
126 |
|
nfcv |
|
127 |
126 77
|
nfres |
|
128 |
124 125 127
|
nfov |
|
129 |
78
|
reseq2d |
|
130 |
129
|
oveq2d |
|
131 |
123 128 130
|
cbvmpt |
|
132 |
122 131
|
eqtr4di |
|
133 |
132
|
oveq2d |
|
134 |
12 76 133
|
3eqtrd |
|