Proof of Theorem dalem38
Step | Hyp | Ref
| Expression |
1 | | dalem38.y |
. 2
|
2 | | dalem.ph |
. . . . . . 7
|
3 | | dalem.l |
. . . . . . 7
|
4 | | dalem.j |
. . . . . . 7
|
5 | | dalem.a |
. . . . . . 7
|
6 | | dalem.ps |
. . . . . . 7
|
7 | | dalem38.m |
. . . . . . 7
|
8 | | dalem38.o |
. . . . . . 7
|
9 | | dalem38.z |
. . . . . . 7
|
10 | | dalem38.g |
. . . . . . 7
|
11 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 10 | dalem28 34986 |
. . . . . 6
|
12 | | dalem38.h |
. . . . . . 7
|
13 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 12 | dalem33 34991 |
. . . . . 6
|
14 | 2 | dalemkelat 34910 |
. . . . . . . 8
|
15 | 14 | 3ad2ant1 1082 |
. . . . . . 7
|
16 | 2, 5 | dalempeb 34925 |
. . . . . . . 8
|
17 | 16 | 3ad2ant1 1082 |
. . . . . . 7
|
18 | 2 | dalemkehl 34909 |
. . . . . . . . 9
|
19 | 18 | 3ad2ant1 1082 |
. . . . . . . 8
|
20 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 10 | dalem23 34982 |
. . . . . . . 8
|
21 | 6 | dalemccea 34969 |
. . . . . . . . 9
|
22 | 21 | 3ad2ant3 1084 |
. . . . . . . 8
|
23 | | eqid 2622 |
. . . . . . . . 9
|
24 | 23, 4, 5 | hlatjcl 34653 |
. . . . . . . 8
|
25 | 19, 20, 22, 24 | syl3anc 1326 |
. . . . . . 7
|
26 | 2, 5 | dalemqeb 34926 |
. . . . . . . 8
|
27 | 26 | 3ad2ant1 1082 |
. . . . . . 7
|
28 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 12 | dalem29 34987 |
. . . . . . . 8
|
29 | 23, 4, 5 | hlatjcl 34653 |
. . . . . . . 8
|
30 | 19, 28, 22, 29 | syl3anc 1326 |
. . . . . . 7
|
31 | 23, 3, 4 | latjlej12 17067 |
. . . . . . 7
|
32 | 15, 17, 25, 27, 30, 31 | syl122anc 1335 |
. . . . . 6
|
33 | 11, 13, 32 | mp2and 715 |
. . . . 5
|
34 | 23, 5 | atbase 34576 |
. . . . . . 7
|
35 | 20, 34 | syl 17 |
. . . . . 6
|
36 | 23, 5 | atbase 34576 |
. . . . . . 7
|
37 | 28, 36 | syl 17 |
. . . . . 6
|
38 | 6, 5 | dalemcceb 34975 |
. . . . . . 7
|
39 | 38 | 3ad2ant3 1084 |
. . . . . 6
|
40 | 23, 4 | latjjdir 17104 |
. . . . . 6
|
41 | 15, 35, 37, 39, 40 | syl13anc 1328 |
. . . . 5
|
42 | 33, 41 | breqtrrd 4681 |
. . . 4
|
43 | | dalem38.i |
. . . . 5
|
44 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 43 | dalem37 34995 |
. . . 4
|
45 | 2, 4, 5 | dalempjqeb 34931 |
. . . . . 6
|
46 | 45 | 3ad2ant1 1082 |
. . . . 5
|
47 | 23, 4, 5 | hlatjcl 34653 |
. . . . . . 7
|
48 | 19, 20, 28, 47 | syl3anc 1326 |
. . . . . 6
|
49 | 23, 4 | latjcl 17051 |
. . . . . 6
|
50 | 15, 48, 39, 49 | syl3anc 1326 |
. . . . 5
|
51 | 2, 5 | dalemreb 34927 |
. . . . . 6
|
52 | 51 | 3ad2ant1 1082 |
. . . . 5
|
53 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 43 | dalem34 34992 |
. . . . . 6
|
54 | 23, 4, 5 | hlatjcl 34653 |
. . . . . 6
|
55 | 19, 53, 22, 54 | syl3anc 1326 |
. . . . 5
|
56 | 23, 3, 4 | latjlej12 17067 |
. . . . 5
|
57 | 15, 46, 50, 52, 55, 56 | syl122anc 1335 |
. . . 4
|
58 | 42, 44, 57 | mp2and 715 |
. . 3
|
59 | 23, 5 | atbase 34576 |
. . . . 5
|
60 | 53, 59 | syl 17 |
. . . 4
|
61 | 23, 4 | latjjdir 17104 |
. . . 4
|
62 | 15, 48, 60, 39, 61 | syl13anc 1328 |
. . 3
|
63 | 58, 62 | breqtrrd 4681 |
. 2
|
64 | 1, 63 | syl5eqbr 4688 |
1
|