Description: Lemma for lcfr . (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 | lcfrlem21 | |
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 | 9 | adantr | |
14 | 10 | adantr | |
15 | 11 | adantr | |
16 | 12 | adantr | |
17 | simpr | |
|
18 | 1 2 3 4 5 6 7 8 13 14 15 16 17 | lcfrlem20 | |
19 | 1 3 9 | dvhlmod | |
20 | 10 | eldifad | |
21 | 11 | eldifad | |
22 | 4 5 | lmodcom | |
23 | 19 20 21 22 | syl3anc | |
24 | 23 | sneqd | |
25 | 24 | fveq2d | |
26 | 25 | eleq2d | |
27 | 26 | biimprd | |
28 | 27 | con3dimp | |
29 | prcom | |
|
30 | 29 | fveq2i | |
31 | 30 | a1i | |
32 | 31 25 | ineq12d | |
33 | 32 | adantr | |
34 | 9 | adantr | |
35 | 11 | adantr | |
36 | 10 | adantr | |
37 | 12 | necomd | |
38 | 37 | adantr | |
39 | simpr | |
|
40 | 1 2 3 4 5 6 7 8 34 35 36 38 39 | lcfrlem20 | |
41 | 33 40 | eqeltrd | |
42 | 28 41 | syldan | |
43 | 1 2 3 4 5 6 7 8 9 10 11 12 | lcfrlem19 | |
44 | 18 42 43 | mpjaodan | |