Description: Part of proof of Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 29-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemc1.b | |
|
cdlemc1.l | |
||
cdlemc1.j | |
||
cdlemc1.m | |
||
cdlemc1.a | |
||
cdlemc1.h | |
||
Assertion | cdlemc1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemc1.b | |
|
2 | cdlemc1.l | |
|
3 | cdlemc1.j | |
|
4 | cdlemc1.m | |
|
5 | cdlemc1.a | |
|
6 | cdlemc1.h | |
|
7 | simp1l | |
|
8 | 7 | hllatd | |
9 | simp3l | |
|
10 | 1 5 | atbase | |
11 | 9 10 | syl | |
12 | simp2 | |
|
13 | 1 3 | latjcl | |
14 | 8 11 12 13 | syl3anc | |
15 | simp1r | |
|
16 | 1 6 | lhpbase | |
17 | 15 16 | syl | |
18 | 1 4 | latmcl | |
19 | 8 14 17 18 | syl3anc | |
20 | 1 3 | latjcom | |
21 | 8 11 19 20 | syl3anc | |
22 | 1 2 3 | latlej1 | |
23 | 8 11 12 22 | syl3anc | |
24 | 1 2 3 4 5 | atmod2i1 | |
25 | 7 9 14 17 23 24 | syl131anc | |
26 | eqid | |
|
27 | 2 3 26 5 6 | lhpjat1 | |
28 | 27 | 3adant2 | |
29 | 28 | oveq2d | |
30 | hlol | |
|
31 | 7 30 | syl | |
32 | 1 4 26 | olm11 | |
33 | 31 14 32 | syl2anc | |
34 | 29 33 | eqtrd | |
35 | 21 25 34 | 3eqtrd | |