Description: Lemma for cygzn . (Contributed by Mario Carneiro, 23-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cygzn.b | |
|
cygzn.n | |
||
cygzn.y | |
||
cygzn.m | |
||
cygzn.l | |
||
cygzn.e | |
||
cygzn.g | |
||
cygzn.x | |
||
cygzn.f | |
||
Assertion | cygznlem2a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygzn.b | |
|
2 | cygzn.n | |
|
3 | cygzn.y | |
|
4 | cygzn.m | |
|
5 | cygzn.l | |
|
6 | cygzn.e | |
|
7 | cygzn.g | |
|
8 | cygzn.x | |
|
9 | cygzn.f | |
|
10 | fvexd | |
|
11 | cyggrp | |
|
12 | 7 11 | syl | |
13 | 12 | adantr | |
14 | simpr | |
|
15 | 6 | ssrab3 | |
16 | 15 8 | sselid | |
17 | 16 | adantr | |
18 | 1 4 | mulgcl | |
19 | 13 14 17 18 | syl3anc | |
20 | fveq2 | |
|
21 | oveq1 | |
|
22 | 1 2 3 4 5 6 7 8 | cygznlem1 | |
23 | 22 | biimpd | |
24 | 23 | exp32 | |
25 | 24 | 3imp2 | |
26 | 9 10 19 20 21 25 | fliftfund | |
27 | 9 10 19 | fliftf | |
28 | 26 27 | mpbid | |
29 | hashcl | |
|
30 | 29 | adantl | |
31 | 0nn0 | |
|
32 | 31 | a1i | |
33 | 30 32 | ifclda | |
34 | 2 33 | eqeltrid | |
35 | eqid | |
|
36 | 3 35 5 | znzrhfo | |
37 | 34 36 | syl | |
38 | fof | |
|
39 | 37 38 | syl | |
40 | 39 | feqmptd | |
41 | 40 | rneqd | |
42 | forn | |
|
43 | 37 42 | syl | |
44 | 41 43 | eqtr3d | |
45 | 44 | feq2d | |
46 | 28 45 | mpbid | |