dalawlem6 - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalawlem6		Structured version Unicode version

Theorem dalawlem6 33826

Description: Lemma for dalaw 33836. First piece of dalawlem8 33828. (Contributed by NM, 6-Oct-2012.)

**Hypotheses**
Ref	Expression
dalawlem.l
dalawlem.j	$.\/$
dalawlem.m	$./\$
dalawlem.a

**Assertion**
Ref	Expression
dalawlem6	$/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

**Proof of Theorem dalawlem6**
Step	Hyp	Ref	Expression
1		eqid 2451	. 2
2		dalawlem.l	. 2
3		simp11 1018	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		hllat 33314	. . 3
5	3, 4	syl 16	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		simp21 1021	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simp22 1022	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		dalawlem.j	. . . . . 6 $.\/$
9		dalawlem.a	. . . . . 6
10	1, 8, 9	hlatjcl 33317	. . . . 5 $/\$ $/\$ $.\/$
11	3, 6, 7, 10	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
12		simp32 1025	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	1, 9	atbase 33240	. . . . 5
14	12, 13	syl 16	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15	1, 8	latjcl 15323	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$
16	5, 11, 14, 15	syl3anc 1219	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simp31 1024	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	1, 9	atbase 33240	. . . 4
19	17, 18	syl 16	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		dalawlem.m	. . . 4 $./\$
21	1, 20	latmcl 15324	. . 3 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
22	5, 16, 19, 21	syl3anc 1219	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
23		simp23 1023	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	1, 8, 9	hlatjcl 33317	. . . . 5 $/\$ $/\$ $.\/$
25	3, 7, 23, 24	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simp33 1026	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	1, 9	atbase 33240	. . . . 5
28	26, 27	syl 16	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	1, 20	latmcl 15324	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $./\$
30	5, 25, 28, 29	syl3anc 1219	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
31	1, 8, 9	hlatjcl 33317	. . . . 5 $/\$ $/\$ $.\/$
32	3, 23, 6, 31	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
33	1, 8, 9	hlatjcl 33317	. . . . 5 $/\$ $/\$ $.\/$
34	3, 26, 17, 33	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
35	1, 20	latmcl 15324	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36	5, 32, 34, 35	syl3anc 1219	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
37	1, 8	latjcl 15323	. . 3 $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
38	5, 30, 36, 37	syl3anc 1219	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
39	1, 8, 9	hlatjcl 33317	. . . . 5 $/\$ $/\$ $.\/$
40	3, 12, 26, 39	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 20	latmcl 15324	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42	5, 25, 40, 41	syl3anc 1219	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
43	1, 8	latjcl 15323	. . 3 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
44	5, 42, 36, 43	syl3anc 1219	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
45	1, 9	atbase 33240	. . . . . . . 8
46	6, 45	syl 16	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	1, 8, 9	hlatjcl 33317	. . . . . . . . 9 $/\$ $/\$ $.\/$
48	3, 6, 17, 47	syl3anc 1219	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	1, 8, 9	hlatjcl 33317	. . . . . . . . . 10 $/\$ $/\$ $.\/$
50	3, 7, 12, 49	syl3anc 1219	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51	1, 20	latmcl 15324	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
52	5, 25, 50, 51	syl3anc 1219	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
53	1, 20	latmcl 15324	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
54	5, 48, 52, 53	syl3anc 1219	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
55	1, 8	latjcl 15323	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
56	5, 46, 54, 55	syl3anc 1219	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
57	1, 9	atbase 33240	. . . . . . . . 9
58	23, 57	syl 16	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	1, 8	latjcl 15323	. . . . . . . 8 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
60	5, 58, 30, 59	syl3anc 1219	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
61	1, 8	latjcl 15323	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
62	5, 46, 60, 61	syl3anc 1219	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
63	1, 2, 8, 20	latmlej22 15365	. . . . . . . . 9 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
64	5, 19, 16, 46, 63	syl13anc 1221	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
65	1, 20	latmcl 15324	. . . . . . . . . . 11 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
66	5, 50, 48, 65	syl3anc 1219	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
67	1, 8	latjcl 15323	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
68	5, 46, 66, 67	syl3anc 1219	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
69	1, 8	latjcl 15323	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
70	5, 46, 52, 69	syl3anc 1219	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
71	2, 8, 9	hlatlej2 33326	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
72	3, 6, 17, 71	syl3anc 1219	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
73	1, 8	latjcl 15323	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
74	5, 46, 50, 73	syl3anc 1219	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
75	1, 2, 20	latmlem2 15354	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
76	5, 19, 48, 74, 75	syl13anc 1221	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
77	72, 76	mpd 15	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	8, 9	hlatjass 33320	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
79	3, 6, 7, 12, 78	syl13anc 1221	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
80	79	oveq1d 6205	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
81	2, 8, 9	hlatlej1 33325	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
82	3, 6, 17, 81	syl3anc 1219	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
83	1, 2, 8, 20, 9	atmod1i1 33807	. . . . . . . . . . 11 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
84	3, 6, 50, 48, 82, 83	syl131anc 1232	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
85	77, 80, 84	3brtr4d 4420	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
86	1, 20	latmcom 15347	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
87	5, 50, 48, 86	syl3anc 1219	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
88		simp12 1019	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
89	87, 88	eqbrtrd 4410	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
90	1, 2, 20	latmle1 15348	. . . . . . . . . . . 12 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
91	5, 50, 48, 90	syl3anc 1219	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
92	1, 2, 20	latlem12 15350	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
93	5, 66, 25, 50, 92	syl13anc 1221	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
94	89, 91, 93	mpbi2and 912	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
95	1, 2, 8	latjlej2 15338	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
96	5, 66, 52, 46, 95	syl13anc 1221	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
97	94, 96	mpd 15	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
98	1, 2, 5, 22, 68, 70, 85, 97	lattrd 15330	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
99	1, 2, 20	latlem12 15350	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
100	5, 22, 48, 70, 99	syl13anc 1221	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
101	64, 98, 100	mpbi2and 912	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
102	1, 2, 8, 20, 9	atmod3i1 33814	. . . . . . . 8 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
103	3, 6, 48, 52, 82, 102	syl131anc 1232	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
104	101, 103	breqtrrd 4416	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
105		simp13 1020	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
106	1, 20	latmcl 15324	. . . . . . . . . . 11 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
107	5, 48, 50, 106	syl3anc 1219	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
108	1, 8, 9	hlatjcl 33317	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
109	3, 23, 26, 108	syl3anc 1219	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
110	1, 2, 20	latmlem2 15354	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
111	5, 107, 109, 25, 110	syl13anc 1221	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
112	105, 111	mpd 15	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
113		hlol 33312	. . . . . . . . . 10
114	3, 113	syl 16	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	1, 20	latm12 33181	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
116	114, 48, 25, 50, 115	syl13anc 1221	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
117	2, 8, 9	hlatlej2 33326	. . . . . . . . . 10 $/\$ $/\$ $.\/$
118	3, 7, 23, 117	syl3anc 1219	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
119	1, 2, 8, 20, 9	atmod3i1 33814	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
120	3, 23, 25, 28, 118, 119	syl131anc 1232	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
121	112, 116, 120	3brtr4d 4420	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
122	1, 2, 8	latjlej2 15338	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
123	5, 54, 60, 46, 122	syl13anc 1221	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
124	121, 123	mpd 15	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
125	1, 2, 5, 22, 56, 62, 104, 124	lattrd 15330	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
126	1, 8	latj13 15370	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
127	5, 46, 58, 30, 126	syl13anc 1221	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
128	125, 127	breqtrd 4414	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
129	1, 2, 8, 20	latmlej22 15365	. . . . 5 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
130	5, 19, 16, 28, 129	syl13anc 1221	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
131	1, 8	latjcl 15323	. . . . . 6 $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
132	5, 30, 32, 131	syl3anc 1219	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
133	1, 2, 20	latlem12 15350	. . . . 5 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
134	5, 22, 132, 34, 133	syl13anc 1221	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
135	128, 130, 134	mpbi2and 912	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
136	1, 2, 8, 20	latmlej21 15364	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
137	5, 28, 25, 19, 136	syl13anc 1221	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
138	1, 2, 8, 20, 9	atmod1i1m 33808	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
139	3, 26, 25, 32, 34, 137, 138	syl231anc 1239	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
140	135, 139	breqtrrd 4416	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
141	2, 8, 9	hlatlej2 33326	. . . . 5 $/\$ $/\$ $.\/$
142	3, 12, 26, 141	syl3anc 1219	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
143	1, 2, 20	latmlem2 15354	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
144	5, 28, 40, 25, 143	syl13anc 1221	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
145	142, 144	mpd 15	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
146	1, 2, 8	latjlej1 15337	. . . 4 $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
147	5, 30, 42, 36, 146	syl13anc 1221	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
148	145, 147	mpd 15	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
149	1, 2, 5, 22, 38, 44, 140, 148	lattrd 15330	1 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758 class class class wbr 4390

cfv 5516 (class class class)co 6190

cbs 14276

cple 14347

cjn 15216

cmee 15217

clat 15317

col 33125

catm 33214

chlt 33301

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-op 3982 df-uni 4190 df-iun 4271 df-iin 4272 df-br 4391 df-opab 4449 df-mpt 4450 df-id 4734 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-1st 6677 df-2nd 6678 df-poset 15218 df-plt 15230 df-lub 15246 df-glb 15247 df-join 15248 df-meet 15249 df-p0 15311 df-lat 15318 df-clat 15380 df-oposet 33127 df-ol 33129 df-oml 33130 df-covers 33217 df-ats 33218 df-atl 33249 df-cvlat 33273 df-hlat 33302 df-psubsp 33453 df-pmap 33454 df-padd 33746

This theorem is referenced by: dalawlem8 33828

W3C validator