Step |
Hyp |
Ref |
Expression |
1 |
|
gsumval3.b |
|
2 |
|
gsumval3.0 |
|
3 |
|
gsumval3.p |
|
4 |
|
gsumval3.z |
|
5 |
|
gsumval3.g |
|
6 |
|
gsumval3.a |
|
7 |
|
gsumval3.f |
|
8 |
|
gsumval3.c |
|
9 |
|
gsumval3.m |
|
10 |
|
gsumval3.h |
|
11 |
|
gsumval3.n |
|
12 |
|
gsumval3.w |
|
13 |
10
|
ad2antrr |
|
14 |
|
suppssdm |
|
15 |
12 14
|
eqsstri |
|
16 |
|
f1f |
|
17 |
10 16
|
syl |
|
18 |
|
fco |
|
19 |
7 17 18
|
syl2anc |
|
20 |
15 19
|
fssdm |
|
21 |
20
|
ad2antrr |
|
22 |
|
f1ores |
|
23 |
13 21 22
|
syl2anc |
|
24 |
12
|
imaeq2i |
|
25 |
|
fex |
|
26 |
7 6 25
|
syl2anc |
|
27 |
|
ovex |
|
28 |
|
fex |
|
29 |
16 27 28
|
sylancl |
|
30 |
10 29
|
syl |
|
31 |
|
f1fun |
|
32 |
10 31
|
syl |
|
33 |
32 11
|
jca |
|
34 |
26 30 33
|
jca31 |
|
35 |
34
|
ad2antrr |
|
36 |
|
imacosupp |
|
37 |
36
|
imp |
|
38 |
35 37
|
syl |
|
39 |
24 38
|
syl5eq |
|
40 |
39
|
f1oeq3d |
|
41 |
23 40
|
mpbid |
|
42 |
|
isof1o |
|
43 |
42
|
ad2antll |
|
44 |
|
f1oco |
|
45 |
41 43 44
|
syl2anc |
|
46 |
|
f1of |
|
47 |
|
frn |
|
48 |
43 46 47
|
3syl |
|
49 |
|
cores |
|
50 |
|
f1oeq1 |
|
51 |
48 49 50
|
3syl |
|
52 |
45 51
|
mpbid |
|
53 |
|
fzfi |
|
54 |
|
ssfi |
|
55 |
53 20 54
|
sylancr |
|
56 |
55
|
ad2antrr |
|
57 |
12
|
a1i |
|
58 |
57
|
imaeq2d |
|
59 |
53
|
a1i |
|
60 |
|
fex2 |
|
61 |
17 59 6 60
|
syl3anc |
|
62 |
26 61 33
|
jca31 |
|
63 |
62
|
ad2antrr |
|
64 |
63 37
|
syl |
|
65 |
58 64
|
eqtrd |
|
66 |
65
|
f1oeq3d |
|
67 |
23 66
|
mpbid |
|
68 |
56 67
|
hasheqf1od |
|
69 |
68
|
oveq2d |
|
70 |
69
|
f1oeq2d |
|
71 |
52 70
|
mpbid |
|