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 36013

Description: Lemma for dalaw 36023. First piece of dalawlem8 36015. (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 2382	. 2
2		dalawlem.l	. 2
3		simp11 1024	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		hllat 35501	. . 3
5	3, 4	syl 16	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		simp21 1027	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simp22 1028	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		dalawlem.j	. . . . . 6 $.\/$
9		dalawlem.a	. . . . . 6
10	1, 8, 9	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
11	3, 6, 7, 10	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
12		simp32 1031	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	1, 9	atbase 35427	. . . . 5
14	12, 13	syl 16	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15	1, 8	latjcl 15798	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$
16	5, 11, 14, 15	syl3anc 1226	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simp31 1030	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	1, 9	atbase 35427	. . . 4
19	17, 18	syl 16	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		dalawlem.m	. . . 4 $./\$
21	1, 20	latmcl 15799	. . 3 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
22	5, 16, 19, 21	syl3anc 1226	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
23		simp23 1029	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	1, 8, 9	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
25	3, 7, 23, 24	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simp33 1032	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	1, 9	atbase 35427	. . . . 5
28	26, 27	syl 16	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	1, 20	latmcl 15799	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $./\$
30	5, 25, 28, 29	syl3anc 1226	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
31	1, 8, 9	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
32	3, 23, 6, 31	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
33	1, 8, 9	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
34	3, 26, 17, 33	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
35	1, 20	latmcl 15799	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36	5, 32, 34, 35	syl3anc 1226	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
37	1, 8	latjcl 15798	. . 3 $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
38	5, 30, 36, 37	syl3anc 1226	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
39	1, 8, 9	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
40	3, 12, 26, 39	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 20	latmcl 15799	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42	5, 25, 40, 41	syl3anc 1226	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
43	1, 8	latjcl 15798	. . 3 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
44	5, 42, 36, 43	syl3anc 1226	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
45	1, 9	atbase 35427	. . . . . . . 8
46	6, 45	syl 16	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	1, 8, 9	hlatjcl 35504	. . . . . . . . 9 $/\$ $/\$ $.\/$
48	3, 6, 17, 47	syl3anc 1226	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	1, 8, 9	hlatjcl 35504	. . . . . . . . . 10 $/\$ $/\$ $.\/$
50	3, 7, 12, 49	syl3anc 1226	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51	1, 20	latmcl 15799	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
52	5, 25, 50, 51	syl3anc 1226	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
53	1, 20	latmcl 15799	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
54	5, 48, 52, 53	syl3anc 1226	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
55	1, 8	latjcl 15798	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
56	5, 46, 54, 55	syl3anc 1226	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
57	1, 9	atbase 35427	. . . . . . . . 9
58	23, 57	syl 16	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	1, 8	latjcl 15798	. . . . . . . 8 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
60	5, 58, 30, 59	syl3anc 1226	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
61	1, 8	latjcl 15798	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
62	5, 46, 60, 61	syl3anc 1226	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
63	1, 2, 8, 20	latmlej22 15840	. . . . . . . . 9 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
64	5, 19, 16, 46, 63	syl13anc 1228	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
65	1, 20	latmcl 15799	. . . . . . . . . . 11 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
66	5, 50, 48, 65	syl3anc 1226	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
67	1, 8	latjcl 15798	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
68	5, 46, 66, 67	syl3anc 1226	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
69	1, 8	latjcl 15798	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
70	5, 46, 52, 69	syl3anc 1226	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
71	2, 8, 9	hlatlej2 35513	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
72	3, 6, 17, 71	syl3anc 1226	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
73	1, 8	latjcl 15798	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
74	5, 46, 50, 73	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
75	1, 2, 20	latmlem2 15829	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
76	5, 19, 48, 74, 75	syl13anc 1228	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
77	72, 76	mpd 15	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	8, 9	hlatjass 35507	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
79	3, 6, 7, 12, 78	syl13anc 1228	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
80	79	oveq1d 6211	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
81	2, 8, 9	hlatlej1 35512	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
82	3, 6, 17, 81	syl3anc 1226	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
83	1, 2, 8, 20, 9	atmod1i1 35994	. . . . . . . . . . 11 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
84	3, 6, 50, 48, 82, 83	syl131anc 1239	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
85	77, 80, 84	3brtr4d 4397	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
86	1, 20	latmcom 15822	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
87	5, 50, 48, 86	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
88		simp12 1025	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
89	87, 88	eqbrtrd 4387	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
90	1, 2, 20	latmle1 15823	. . . . . . . . . . . 12 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
91	5, 50, 48, 90	syl3anc 1226	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
92	1, 2, 20	latlem12 15825	. . . . . . . . . . . 12 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
93	5, 66, 25, 50, 92	syl13anc 1228	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
94	89, 91, 93	mpbi2and 919	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
95	1, 2, 8	latjlej2 15813	. . . . . . . . . . 11 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
96	5, 66, 52, 46, 95	syl13anc 1228	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
97	94, 96	mpd 15	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
98	1, 2, 5, 22, 68, 70, 85, 97	lattrd 15805	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
99	1, 2, 20	latlem12 15825	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
100	5, 22, 48, 70, 99	syl13anc 1228	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
101	64, 98, 100	mpbi2and 919	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
102	1, 2, 8, 20, 9	atmod3i1 36001	. . . . . . . 8 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
103	3, 6, 48, 52, 82, 102	syl131anc 1239	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
104	101, 103	breqtrrd 4393	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
105		simp13 1026	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
106	1, 20	latmcl 15799	. . . . . . . . . . 11 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
107	5, 48, 50, 106	syl3anc 1226	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
108	1, 8, 9	hlatjcl 35504	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
109	3, 23, 26, 108	syl3anc 1226	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
110	1, 2, 20	latmlem2 15829	. . . . . . . . . 10 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
111	5, 107, 109, 25, 110	syl13anc 1228	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
112	105, 111	mpd 15	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
113		hlol 35499	. . . . . . . . . 10
114	3, 113	syl 16	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	1, 20	latm12 35368	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
116	114, 48, 25, 50, 115	syl13anc 1228	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
117	2, 8, 9	hlatlej2 35513	. . . . . . . . . 10 $/\$ $/\$ $.\/$
118	3, 7, 23, 117	syl3anc 1226	. . . . . . . . 9 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
119	1, 2, 8, 20, 9	atmod3i1 36001	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
120	3, 23, 25, 28, 118, 119	syl131anc 1239	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
121	112, 116, 120	3brtr4d 4397	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
122	1, 2, 8	latjlej2 15813	. . . . . . . 8 $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
123	5, 54, 60, 46, 122	syl13anc 1228	. . . . . . 7 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
124	121, 123	mpd 15	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
125	1, 2, 5, 22, 56, 62, 104, 124	lattrd 15805	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
126	1, 8	latj13 15845	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
127	5, 46, 58, 30, 126	syl13anc 1228	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
128	125, 127	breqtrd 4391	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$
129	1, 2, 8, 20	latmlej22 15840	. . . . 5 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
130	5, 19, 16, 28, 129	syl13anc 1228	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
131	1, 8	latjcl 15798	. . . . . 6 $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
132	5, 30, 32, 131	syl3anc 1226	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
133	1, 2, 20	latlem12 15825	. . . . 5 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
134	5, 22, 132, 34, 133	syl13anc 1228	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
135	128, 130, 134	mpbi2and 919	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
136	1, 2, 8, 20	latmlej21 15839	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
137	5, 28, 25, 19, 136	syl13anc 1228	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
138	1, 2, 8, 20, 9	atmod1i1m 35995	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
139	3, 26, 25, 32, 34, 137, 138	syl231anc 1246	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
140	135, 139	breqtrrd 4393	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
141	2, 8, 9	hlatlej2 35513	. . . . 5 $/\$ $/\$ $.\/$
142	3, 12, 26, 141	syl3anc 1226	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
143	1, 2, 20	latmlem2 15829	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
144	5, 28, 40, 25, 143	syl13anc 1228	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
145	142, 144	mpd 15	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
146	1, 2, 8	latjlej1 15812	. . . 4 $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
147	5, 30, 42, 36, 146	syl13anc 1228	. . 3 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
148	145, 147	mpd 15	. 2 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
149	1, 2, 5, 22, 38, 44, 140, 148	lattrd 15805	1 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826 class class class wbr 4367

cfv 5496 (class class class)co 6196

cbs 14634

cple 14709

cjn 15690

cmee 15691

clat 15792

col 35312

catm 35401

chlt 35488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-iin 4246 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-1st 6699 df-2nd 6700 df-preset 15674 df-poset 15692 df-plt 15705 df-lub 15721 df-glb 15722 df-join 15723 df-meet 15724 df-p0 15786 df-lat 15793 df-clat 15855 df-oposet 35314 df-ol 35316 df-oml 35317 df-covers 35404 df-ats 35405 df-atl 35436 df-cvlat 35460 df-hlat 35489 df-psubsp 35640 df-pmap 35641 df-padd 35933

This theorem is referenced by: dalawlem8 36015

W3C validator