Step | Hyp | Ref
| Expression |
1 | | gsumval3a.n |
. . . . . 6
|
2 | 1 | neneqd 2799 |
. . . . 5
|
3 | | gsumval3a.t |
. . . . . . 7
|
4 | | fz1f1o 14441 |
. . . . . . 7
|
5 | 3, 4 | syl 17 |
. . . . . 6
|
6 | 5 | ord 392 |
. . . . 5
|
7 | 2, 6 | mpd 15 |
. . . 4
|
8 | 7 | simprd 479 |
. . 3
|
9 | | excom 2042 |
. . . 4
|
10 | | exancom 1787 |
. . . . . 6
|
11 | | fvex 6201 |
. . . . . . 7
|
12 | | biidd 252 |
. . . . . . 7
|
13 | 11, 12 | ceqsexv 3242 |
. . . . . 6
|
14 | 10, 13 | bitri 264 |
. . . . 5
|
15 | 14 | exbii 1774 |
. . . 4
|
16 | 9, 15 | bitri 264 |
. . 3
|
17 | 8, 16 | sylibr 224 |
. 2
|
18 | | eeanv 2182 |
. . . 4
|
19 | | an4 865 |
. . . . . 6
|
20 | | gsumval3.g |
. . . . . . . . . . 11
|
21 | 20 | adantr 481 |
. . . . . . . . . 10
|
22 | | gsumval3.b |
. . . . . . . . . . . 12
|
23 | | gsumval3.p |
. . . . . . . . . . . 12
|
24 | 22, 23 | mndcl 17301 |
. . . . . . . . . . 11
|
25 | 24 | 3expb 1266 |
. . . . . . . . . 10
|
26 | 21, 25 | sylan 488 |
. . . . . . . . 9
|
27 | | gsumval3.c |
. . . . . . . . . . . . 13
|
28 | 27 | adantr 481 |
. . . . . . . . . . . 12
|
29 | 28 | sselda 3603 |
. . . . . . . . . . 11
|
30 | 29 | adantrr 753 |
. . . . . . . . . 10
|
31 | | simprr 796 |
. . . . . . . . . 10
|
32 | | gsumval3.z |
. . . . . . . . . . 11
Cntz |
33 | 23, 32 | cntzi 17762 |
. . . . . . . . . 10
|
34 | 30, 31, 33 | syl2anc 693 |
. . . . . . . . 9
|
35 | 22, 23 | mndass 17302 |
. . . . . . . . . 10
|
36 | 21, 35 | sylan 488 |
. . . . . . . . 9
|
37 | 7 | simpld 475 |
. . . . . . . . . . 11
|
38 | 37 | adantr 481 |
. . . . . . . . . 10
|
39 | | nnuz 11723 |
. . . . . . . . . 10
|
40 | 38, 39 | syl6eleq 2711 |
. . . . . . . . 9
|
41 | | gsumval3.f |
. . . . . . . . . . 11
|
42 | 41 | adantr 481 |
. . . . . . . . . 10
|
43 | | frn 6053 |
. . . . . . . . . 10
|
44 | 42, 43 | syl 17 |
. . . . . . . . 9
|
45 | | simprr 796 |
. . . . . . . . . . 11
|
46 | | f1ocnv 6149 |
. . . . . . . . . . 11
|
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
|
48 | | simprl 794 |
. . . . . . . . . 10
|
49 | | f1oco 6159 |
. . . . . . . . . 10
|
50 | 47, 48, 49 | syl2anc 693 |
. . . . . . . . 9
|
51 | | f1of 6137 |
. . . . . . . . . . . 12
|
52 | 45, 51 | syl 17 |
. . . . . . . . . . 11
|
53 | | fvco3 6275 |
. . . . . . . . . . 11
|
54 | 52, 53 | sylan 488 |
. . . . . . . . . 10
|
55 | | ffn 6045 |
. . . . . . . . . . . . 13
|
56 | 42, 55 | syl 17 |
. . . . . . . . . . . 12
|
57 | 56 | adantr 481 |
. . . . . . . . . . 11
|
58 | | gsumval3a.s |
. . . . . . . . . . . . . 14
|
59 | 58 | adantr 481 |
. . . . . . . . . . . . 13
|
60 | 52, 59 | fssd 6057 |
. . . . . . . . . . . 12
|
61 | 60 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
62 | | fnfvelrn 6356 |
. . . . . . . . . . 11
|
63 | 57, 61, 62 | syl2anc 693 |
. . . . . . . . . 10
|
64 | 54, 63 | eqeltrd 2701 |
. . . . . . . . 9
|
65 | | f1of 6137 |
. . . . . . . . . . . . . . 15
|
66 | 48, 65 | syl 17 |
. . . . . . . . . . . . . 14
|
67 | | fvco3 6275 |
. . . . . . . . . . . . . 14
|
68 | 66, 67 | sylan 488 |
. . . . . . . . . . . . 13
|
69 | 68 | fveq2d 6195 |
. . . . . . . . . . . 12
|
70 | 45 | adantr 481 |
. . . . . . . . . . . . 13
|
71 | 66 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
72 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . 13
|
73 | 70, 71, 72 | syl2anc 693 |
. . . . . . . . . . . 12
|
74 | 69, 73 | eqtr2d 2657 |
. . . . . . . . . . 11
|
75 | 74 | fveq2d 6195 |
. . . . . . . . . 10
|
76 | | fvco3 6275 |
. . . . . . . . . . 11
|
77 | 66, 76 | sylan 488 |
. . . . . . . . . 10
|
78 | | f1of 6137 |
. . . . . . . . . . . . 13
|
79 | 50, 78 | syl 17 |
. . . . . . . . . . . 12
|
80 | 79 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
81 | | fvco3 6275 |
. . . . . . . . . . . 12
|
82 | 60, 81 | sylan 488 |
. . . . . . . . . . 11
|
83 | 80, 82 | syldan 487 |
. . . . . . . . . 10
|
84 | 75, 77, 83 | 3eqtr4d 2666 |
. . . . . . . . 9
|
85 | 26, 34, 36, 40, 44, 50, 64, 84 | seqf1o 12842 |
. . . . . . . 8
|
86 | | eqeq12 2635 |
. . . . . . . 8
|
87 | 85, 86 | syl5ibrcom 237 |
. . . . . . 7
|
88 | 87 | expimpd 629 |
. . . . . 6
|
89 | 19, 88 | syl5bir 233 |
. . . . 5
|
90 | 89 | exlimdvv 1862 |
. . . 4
|
91 | 18, 90 | syl5bir 233 |
. . 3
|
92 | 91 | alrimivv 1856 |
. 2
|
93 | | eqeq1 2626 |
. . . . . 6
|
94 | 93 | anbi2d 740 |
. . . . 5
|
95 | 94 | exbidv 1850 |
. . . 4
|
96 | | f1oeq1 6127 |
. . . . . 6
|
97 | | coeq2 5280 |
. . . . . . . . 9
|
98 | 97 | seqeq3d 12809 |
. . . . . . . 8
|
99 | 98 | fveq1d 6193 |
. . . . . . 7
|
100 | 99 | eqeq2d 2632 |
. . . . . 6
|
101 | 96, 100 | anbi12d 747 |
. . . . 5
|
102 | 101 | cbvexv 2275 |
. . . 4
|
103 | 95, 102 | syl6bb 276 |
. . 3
|
104 | 103 | eu4 2518 |
. 2
|
105 | 17, 92, 104 | sylanbrc 698 |
1
|