Description: Lemma for lcfr . Condition needed more than once. (Contributed by NM, 11-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcfrlem17.h | |
|
lcfrlem17.o | |
||
lcfrlem17.u | |
||
lcfrlem17.v | |
||
lcfrlem17.p | |
||
lcfrlem17.z | |
||
lcfrlem17.n | |
||
lcfrlem17.a | |
||
lcfrlem17.k | |
||
lcfrlem17.x | |
||
lcfrlem17.y | |
||
lcfrlem17.ne | |
||
Assertion | lcfrlem17 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem17.h | |
|
2 | lcfrlem17.o | |
|
3 | lcfrlem17.u | |
|
4 | lcfrlem17.v | |
|
5 | lcfrlem17.p | |
|
6 | lcfrlem17.z | |
|
7 | lcfrlem17.n | |
|
8 | lcfrlem17.a | |
|
9 | lcfrlem17.k | |
|
10 | lcfrlem17.x | |
|
11 | lcfrlem17.y | |
|
12 | lcfrlem17.ne | |
|
13 | 1 3 9 | dvhlmod | |
14 | 10 | eldifad | |
15 | 11 | eldifad | |
16 | 4 5 | lmodvacl | |
17 | 13 14 15 16 | syl3anc | |
18 | 4 5 6 7 13 14 15 12 | lmodindp1 | |
19 | eldifsn | |
|
20 | 17 18 19 | sylanbrc | |