Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cygzn.b | |
|
cygzn.n | |
||
cygzn.y | |
||
cygzn.m | |
||
cygzn.l | |
||
cygzn.e | |
||
cygzn.g | |
||
cygzn.x | |
||
Assertion | cygznlem1 | |
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 | hashcl | |
|
10 | 9 | adantl | |
11 | 0nn0 | |
|
12 | 11 | a1i | |
13 | 10 12 | ifclda | |
14 | 2 13 | eqeltrid | |
15 | 14 | adantr | |
16 | simprl | |
|
17 | simprr | |
|
18 | 3 5 | zndvds | |
19 | 15 16 17 18 | syl3anc | |
20 | cyggrp | |
|
21 | 7 20 | syl | |
22 | eqid | |
|
23 | 1 4 6 22 | cyggenod2 | |
24 | 21 8 23 | syl2anc | |
25 | 24 2 | eqtr4di | |
26 | 25 | adantr | |
27 | 26 | breq1d | |
28 | 21 | adantr | |
29 | 1 4 6 | iscyggen | |
30 | 29 | simplbi | |
31 | 8 30 | syl | |
32 | 31 | adantr | |
33 | eqid | |
|
34 | 1 22 4 33 | odcong | |
35 | 28 32 16 17 34 | syl112anc | |
36 | 19 27 35 | 3bitr2d | |