cdleme22eALTN - Mathbox for Norm Megill

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

Theorem cdleme22eALTN 30827

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.

represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s)

f_z(t) $\/$ v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
cdleme22.l
cdleme22.j	$.\/$
cdleme22.m	$./\$
cdleme22.a
cdleme22.h
cdleme22eALT.u	$.\/$ $./\$
cdleme22eALT.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme22eALT.g	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme22eALT.n	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme22eALT.o	$.\/$ $./\$ $.\/$ $.\/$ $./\$

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

**Proof of Theorem cdleme22eALTN**
Step	Hyp	Ref	Expression
1		cdleme22eALT.n	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
2		simp11 987	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
3		hllat 29846	. . . . 5
4	2, 3	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
5		simp21l 1074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
6		simp22l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
7		eqid 2404	. . . . . 6
8		cdleme22.j	. . . . . 6 $.\/$
9		cdleme22.a	. . . . . 6
10	7, 8, 9	hlatjcl 29849	. . . . 5 $/\$ $/\$ $.\/$
11	2, 5, 6, 10	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
12		simp12 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
13		simp3ll 1028	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
14	13	3ad2ant3 980	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
15		cdleme22.l	. . . . . . 7
16		cdleme22.m	. . . . . . 7 $./\$
17		cdleme22.h	. . . . . . 7
18		cdleme22eALT.u	. . . . . . 7 $.\/$ $./\$
19		cdleme22eALT.f	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
20	15, 8, 16, 9, 17, 18, 19, 7	cdleme1b 30708	. . . . . 6 $/\$ $/\$ $/\$ $/\$
21	2, 12, 5, 6, 14, 20	syl23anc 1191	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
22		simp31 993	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
23	7, 8, 9	hlatjcl 29849	. . . . . . 7 $/\$ $/\$ $.\/$
24	2, 22, 14, 23	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
25	7, 17	lhpbase 30480	. . . . . . 7
26	12, 25	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
27	7, 16	latmcl 14435	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
28	4, 24, 26, 27	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
29	7, 8	latjcl 14434	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
30	4, 21, 28, 29	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
31	7, 15, 16	latmle1 14460	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
32	4, 11, 30, 31	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
33	1, 32	syl5eqbr 4205	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
34		simp21 990	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp13 989	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
36		simp321 1107	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
37		simp322 1108	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
38	36, 37	jca 519	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp23 992	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
40		simp323 1109	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
41	15, 8, 16, 9, 17, 18	cdleme22a 30822	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
42	2, 12, 34, 6, 35, 38, 39, 40, 41	syl233anc 1213	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
43	42	oveq2d 6056	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44		cdleme22eALT.o	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$
45	44	oveq1i 6050	. . . 4 $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
46		simp21r 1075	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
47	15, 8, 16, 9, 17, 18	cdleme0a 30693	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	2, 12, 5, 46, 6, 39, 47	syl222anc 1200	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
49		simp3rl 1030	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
50	49	3ad2ant3 980	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
51		cdleme22eALT.g	. . . . . . . 8 $.\/$ $./\$ $.\/$ $.\/$ $./\$
52	15, 8, 16, 9, 17, 18, 51, 7	cdleme1b 30708	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
53	2, 12, 5, 6, 50, 52	syl23anc 1191	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
54	7, 8, 9	hlatjcl 29849	. . . . . . . 8 $/\$ $/\$ $.\/$
55	2, 35, 50, 54	syl3anc 1184	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	7, 16	latmcl 14435	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
57	4, 55, 26, 56	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
58	7, 8	latjcl 14434	. . . . . 6 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	4, 53, 57, 58	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
60	15, 8, 16, 9, 17, 18	cdlemeulpq 30702	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
61	2, 12, 5, 6, 60	syl22anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
62	7, 15, 8, 16, 9	atmod2i1 30343	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
63	2, 48, 11, 59, 61, 62	syl131anc 1197	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
64	45, 63	syl5req 2449	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
65	42	oveq2d 6056	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	40, 65	eqtr3d 2438	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	7, 8, 9	hlatjcl 29849	. . . . . . . 8 $/\$ $/\$ $.\/$
68	2, 35, 48, 67	syl3anc 1184	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
69	7, 9	atbase 29772	. . . . . . . 8
70	50, 69	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
71	7, 15, 8	latlej1 14444	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
72	4, 68, 70, 71	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
73	8, 9	hlatj32 29854	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
74	2, 35, 48, 50, 73	syl13anc 1186	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
75	7, 9	atbase 29772	. . . . . . . . . 10
76	48, 75	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
77	7, 8	latj32 14481	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	4, 70, 76, 57, 77	syl13anc 1186	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
79	7, 8	latj32 14481	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
80	4, 53, 57, 76, 79	syl13anc 1186	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
81	7, 8, 9	hlatjcl 29849	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $.\/$
82	2, 5, 50, 81	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
83	15, 8, 9	hlatlej1 29857	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $.\/$
84	2, 5, 50, 83	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
85	7, 15, 8, 16, 9	atmod3i1 30346	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
86	2, 5, 82, 26, 84, 85	syl131anc 1197	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
87		eqid 2404	. . . . . . . . . . . . . . . . . . . 20
88	15, 8, 87, 9, 17	lhpjat2 30503	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $.\/$
89	2, 12, 34, 88	syl21anc 1183	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
90	89	oveq2d 6056	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
91		hlol 29844	. . . . . . . . . . . . . . . . . . 19
92	2, 91	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
93	7, 16, 87	olm11 29710	. . . . . . . . . . . . . . . . . 18 $/\$ $.\/$ $.\/$ $./\$ $.\/$
94	92, 82, 93	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
95	86, 90, 94	3eqtrd 2440	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
96	95	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$
97	18	oveq2i 6051	. . . . . . . . . . . . . . . . . . 19 $.\/$ $.\/$ $.\/$ $./\$
98	15, 8, 9	hlatlej2 29858	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $.\/$
99	2, 5, 6, 98	syl3anc 1184	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
100	7, 15, 8, 16, 9	atmod3i1 30346	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
101	2, 6, 11, 26, 99, 100	syl131anc 1197	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
102	97, 101	syl5eq 2448	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
103		simp22 991	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
104	15, 8, 87, 9, 17	lhpjat2 30503	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $.\/$
105	2, 12, 103, 104	syl21anc 1183	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
106	105	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
107	7, 16, 87	olm11 29710	. . . . . . . . . . . . . . . . . . 19 $/\$ $.\/$ $.\/$ $./\$ $.\/$
108	92, 11, 107	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
109	102, 106, 108	3eqtrd 2440	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
110	109	oveq1d 6055	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
111	7, 9	atbase 29772	. . . . . . . . . . . . . . . . . 18
112	5, 111	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
113	7, 16	latmcl 14435	. . . . . . . . . . . . . . . . . 18 $/\$ $.\/$ $/\$ $.\/$ $./\$
114	4, 82, 26, 113	syl3anc 1184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
115	7, 9	atbase 29772	. . . . . . . . . . . . . . . . . 18
116	6, 115	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$
117	7, 8	latj32 14481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
118	4, 112, 114, 116, 117	syl13anc 1186	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
119	110, 118	eqtr4d 2439	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
120	8, 9	hlatj32 29854	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
121	2, 5, 6, 50, 120	syl13anc 1186	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
122	96, 119, 121	3eqtr4rd 2447	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
123	7, 8	latj32 14481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
124	4, 116, 76, 114, 123	syl13anc 1186	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
125	122, 124	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
126	125	oveq2d 6056	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
127	7, 8	latjcl 14434	. . . . . . . . . . . . . 14 $/\$ $.\/$ $/\$ $.\/$ $.\/$
128	4, 11, 70, 127	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
129	7, 15, 8	latlej2 14445	. . . . . . . . . . . . . 14 $/\$ $.\/$ $/\$ $.\/$ $.\/$
130	4, 11, 70, 129	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
131	7, 15, 8, 16, 9	atmod1i1 30339	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
132	2, 50, 76, 128, 130, 131	syl131anc 1197	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
133	51	oveq1i 6050	. . . . . . . . . . . . 13 $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
134	7, 8, 9	hlatjcl 29849	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
135	2, 50, 48, 134	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
136	7, 8	latjcl 14434	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
137	4, 116, 114, 136	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
138	15, 8, 9	hlatlej2 29858	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
139	2, 50, 48, 138	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
140	7, 15, 8, 16, 9	atmod2i1 30343	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
141	2, 48, 135, 137, 139, 140	syl131anc 1197	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
142	133, 141	syl5eq 2448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
143	126, 132, 142	3eqtr4rd 2447	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
144	7, 15, 8	latlej1 14444	. . . . . . . . . . . . . . 15 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
145	4, 11, 70, 144	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
146	7, 15, 4, 76, 11, 128, 61, 145	lattrd 14442	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
147	7, 15, 16	latleeqm1 14463	. . . . . . . . . . . . . 14 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
148	4, 76, 128, 147	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
149	146, 148	mpbid 202	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$ $.\/$
150	149	oveq2d 6056	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$
151	143, 150	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
152	151	oveq1d 6055	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$
153	80, 152	eqtrd 2436	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
154	15, 8, 9	hlatlej2 29858	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
155	2, 35, 50, 154	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
156	7, 15, 8, 16, 9	atmod3i1 30346	. . . . . . . . . . 11 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
157	2, 50, 55, 26, 155, 156	syl131anc 1197	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
158		simp33r 1085	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
159	15, 8, 87, 9, 17	lhpjat2 30503	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$
160	2, 12, 158, 159	syl21anc 1183	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
161	160	oveq2d 6056	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
162	7, 16, 87	olm11 29710	. . . . . . . . . . 11 $/\$ $.\/$ $.\/$ $./\$ $.\/$
163	92, 55, 162	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
164	157, 161, 163	3eqtrrd 2441	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
165	164	oveq1d 6055	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
166	78, 153, 165	3eqtr4rd 2447	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
167	74, 166	eqtrd 2436	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
168	72, 167	breqtrd 4196	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
169	66, 168	eqbrtrd 4192	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
170	7, 8	latjcl 14434	. . . . . 6 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
171	4, 59, 76, 170	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
172	7, 15, 16	latleeqm1 14463	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
173	4, 11, 171, 172	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
174	169, 173	mpbid 202	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
175	43, 64, 174	3eqtr2rd 2443	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
176	33, 175	breqtrd 4196	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567 class class class wbr 4172

cfv 5413 (class class class)co 6040

cbs 13424

cple 13491

cjn 14356

cmee 14357

cp1 14422

clat 14429

col 29657

catm 29746

chlt 29833

clh 30466

This theorem is referenced by: cdleme26eALTN 30843

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-op 3783 df-uni 3976 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-id 4458 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-undef 6502 df-riota 6508 df-poset 14358 df-plt 14370 df-lub 14386 df-glb 14387 df-join 14388 df-meet 14389 df-p0 14423 df-p1 14424 df-lat 14430 df-clat 14492 df-oposet 29659 df-ol 29661 df-oml 29662 df-covers 29749 df-ats 29750 df-atl 29781 df-cvlat 29805 df-hlat 29834 df-psubsp 29985 df-pmap 29986 df-padd 30278 df-lhyp 30470

W3C validator