2lplnja - Mathbox for Norm Megill

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

Theorem 2lplnja 30101

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 30102 in terms of atoms). (Contributed by NM, 12-Jul-2012.)

**Hypotheses**
Ref	Expression
2lplnja.l
2lplnja.j	$.\/$
2lplnja.a
2lplnja.v

**Assertion**
Ref	Expression
2lplnja	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

**Proof of Theorem 2lplnja**
Step	Hyp	Ref	Expression
1		eqid 2404	. 2
2		2lplnja.l	. 2
3		simp11l 1068	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
4		hllat 29846	. . 3
5	3, 4	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
6		simp121 1089	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
7		simp122 1090	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
8		2lplnja.j	. . . . . 6 $.\/$
9		2lplnja.a	. . . . . 6
10	1, 8, 9	hlatjcl 29849	. . . . 5 $/\$ $/\$ $.\/$
11	3, 6, 7, 10	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
12		simp123 1091	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
13	1, 9	atbase 29772	. . . . 5
14	12, 13	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
15	1, 8	latjcl 14434	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$
16	5, 11, 14, 15	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
17		simp2l1 1056	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
18		simp2l2 1057	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
19	1, 8, 9	hlatjcl 29849	. . . . 5 $/\$ $/\$ $.\/$
20	3, 17, 18, 19	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
21		simp2l3 1058	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	1, 9	atbase 29772	. . . . 5
23	21, 22	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
24	1, 8	latjcl 14434	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$
25	5, 20, 23, 24	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
26	1, 8	latjcl 14434	. . 3 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
27	5, 16, 25, 26	syl3anc 1184	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
28		simp11r 1069	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
29		2lplnja.v	. . . 4
30	1, 29	lvolbase 30060	. . 3
31	28, 30	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
32		simp31 993	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
33		simp32 994	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
34	1, 2, 8	latjle12 14446	. . . 4 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
35	5, 16, 25, 31, 34	syl13anc 1186	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
36	32, 33, 35	mpbi2and 888	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
37	1, 2, 8	latlej2 14445	. . . . . . . . . 10 $/\$ $.\/$ $/\$ $.\/$ $.\/$
38	5, 20, 23, 37	syl3anc 1184	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
39	1, 2, 5, 23, 25, 31, 38, 33	lattrd 14442	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
40	1, 2, 8	latjle12 14446	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
41	5, 16, 23, 31, 40	syl13anc 1186	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
42	32, 39, 41	mpbi2and 888	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
43	42	ad2antrr 707	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
44	3	ad2antrr 707	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
45	3, 6, 7	3jca 1134	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $/\$
46	45	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
47	12, 21	jca 519	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$
48	47	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
49		simp13l 1072	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
50	49	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
51		simp13r 1073	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
52	51	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
53		simp33 995	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
54	53	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
55		simplr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
56		simpr 448	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
57	1, 9	atbase 29772	. . . . . . . . . . . . . . . . . . 19
58	17, 57	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
59	1, 9	atbase 29772	. . . . . . . . . . . . . . . . . . 19
60	18, 59	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
61	1, 2, 8	latjle12 14446	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
62	5, 58, 60, 16, 61	syl13anc 1186	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
63	62	ad2antrr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
64	55, 56, 63	mpbi2and 888	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
65	64	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
66		simpr 448	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
67	1, 2, 8	latjle12 14446	. . . . . . . . . . . . . . . 16 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
68	5, 20, 23, 16, 67	syl13anc 1186	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
69	68	ad3antrrr 711	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
70	65, 66, 69	mpbi2and 888	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71		simp2l 983	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $/\$
72		simp12 988	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $/\$
73		simp2rr 1027	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
74		simp2rl 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
75	2, 8, 9	3at 29972	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
76	3, 71, 72, 73, 74, 75	syl32anc 1192	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
77	76	ad3antrrr 711	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
78	70, 77	mpbid 202	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
79	78	eqcomd 2409	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
80	79	ex 424	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
81	80	necon3ad 2603	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
82	54, 81	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
83	2, 8, 9, 29	lvoli2 30063	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
84	46, 48, 50, 52, 82, 83	syl113anc 1196	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
85	28	ad2antrr 707	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
86	2, 29	lvolcmp 30099	. . . . . . 7 $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
87	44, 84, 85, 86	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
88	43, 87	mpbid 202	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
89	1, 2, 8	latjlej2 14450	. . . . . . . 8 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
90	5, 23, 25, 16, 89	syl13anc 1186	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
91	38, 90	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
92	91	ad2antrr 707	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
93	88, 92	eqbrtrrd 4194	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
94	1, 8, 9	hlatjcl 29849	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
95	3, 17, 21, 94	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
96	1, 2, 8	latlej2 14445	. . . . . . . . . . 11 $/\$ $.\/$ $/\$ $.\/$ $.\/$
97	5, 95, 60, 96	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
98	8, 9	hlatj32 29854	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
99	3, 17, 18, 21, 98	syl13anc 1186	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
100	97, 99	breqtrrd 4198	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
101	1, 2, 5, 60, 25, 31, 100, 33	lattrd 14442	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
102	1, 2, 8	latjle12 14446	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
103	5, 16, 60, 31, 102	syl13anc 1186	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
104	32, 101, 103	mpbi2and 888	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
105	104	ad2antrr 707	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
106	3	ad2antrr 707	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
107	45	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
108	12, 18	jca 519	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$
109	108	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
110	49	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
111	51	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
112		simpr 448	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
113	2, 8, 9, 29	lvoli2 30063	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
114	107, 109, 110, 111, 112, 113	syl113anc 1196	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
115	28	ad2antrr 707	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
116	2, 29	lvolcmp 30099	. . . . . . 7 $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
117	106, 114, 115, 116	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
118	105, 117	mpbid 202	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
119	1, 2, 8	latjlej2 14450	. . . . . . . 8 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
120	5, 60, 25, 16, 119	syl13anc 1186	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
121	100, 120	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
122	121	ad2antrr 707	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
123	118, 122	eqbrtrrd 4194	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
124	93, 123	pm2.61dan 767	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
125	1, 8, 9	hlatjcl 29849	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
126	3, 18, 21, 125	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
127	1, 2, 8	latlej1 14444	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$
128	5, 58, 126, 127	syl3anc 1184	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
129	1, 8	latjass 14479	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
130	5, 58, 60, 23, 129	syl13anc 1186	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
131	128, 130	breqtrrd 4198	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
132	1, 2, 5, 58, 25, 31, 131, 33	lattrd 14442	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
133	1, 2, 8	latjle12 14446	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
134	5, 16, 58, 31, 133	syl13anc 1186	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
135	32, 132, 134	mpbi2and 888	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
136	135	adantr 452	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$