poimirlem29 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem29		Structured version Visualization version Unicode version

Theorem poimirlem29 31981

Description: Lemma for poimir 31985 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimir.i
poimir.r
poimir.1	↾_t
poimirlem30.x
poimirlem30.2
poimirlem30.3	$/\$ ..^
poimirlem30.4	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
poimirlem29	↾_t

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem poimirlem29 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.r	. . . . . . . . . . . 12
2		fzfi 12192	. . . . . . . . . . . . 13
3		retop 21794	. . . . . . . . . . . . . 14
4	3	fconst6 5778	. . . . . . . . . . . . 13
5		pttop 20609	. . . . . . . . . . . . 13 $/\$
6	2, 4, 5	mp2an 679	. . . . . . . . . . . 12
7	1, 6	eqeltri 2527	. . . . . . . . . . 11
8		poimir.i	. . . . . . . . . . . 12
9		ovex 6323	. . . . . . . . . . . 12
10	8, 9	eqeltri 2527	. . . . . . . . . . 11
11		elrest 15338	. . . . . . . . . . 11 $/\$ ↾_t
12	7, 10, 11	mp2an 679	. . . . . . . . . 10 ↾_t
13		eqid 2453	. . . . . . . . . . . . . 14
14	1, 13	ptrecube 31952	. . . . . . . . . . . . 13 $/\$
15	14	ex 436	. . . . . . . . . . . 12
16		inss1 3654	. . . . . . . . . . . . . . 15
17		sseq1 3455	. . . . . . . . . . . . . . 15
18	16, 17	mpbiri 237	. . . . . . . . . . . . . 14
19	18	sseld 3433	. . . . . . . . . . . . 13
20		ssrin 3659	. . . . . . . . . . . . . . 15
21		sseq2 3456	. . . . . . . . . . . . . . 15
22	20, 21	syl5ibr 225	. . . . . . . . . . . . . 14
23	22	reximdv 2863	. . . . . . . . . . . . 13
24	19, 23	imim12d 77	. . . . . . . . . . . 12
25	15, 24	syl5com 31	. . . . . . . . . . 11
26	25	rexlimiv 2875	. . . . . . . . . 10
27	12, 26	sylbi 199	. . . . . . . . 9 ↾_t
28	27	imp 431	. . . . . . . 8 ↾_t $/\$
29	28	adantl 468	. . . . . . 7 $/\$ ↾_t $/\$
30		resttop 20188	. . . . . . . . . . 11 $/\$ ↾_t
31	7, 10, 30	mp2an 679	. . . . . . . . . 10 ↾_t
32		reex 9635	. . . . . . . . . . . . . 14
33		unitssre 11786	. . . . . . . . . . . . . 14
34		mapss 7519	. . . . . . . . . . . . . 14 $/\$
35	32, 33, 34	mp2an 679	. . . . . . . . . . . . 13
36	8, 35	eqsstri 3464	. . . . . . . . . . . 12
37		ovex 6323	. . . . . . . . . . . . . 14
38		uniretop 21795	. . . . . . . . . . . . . . 15
39	1, 38	ptuniconst 20625	. . . . . . . . . . . . . 14 $/\$
40	37, 3, 39	mp2an 679	. . . . . . . . . . . . 13
41	40	restuni 20190	. . . . . . . . . . . 12 $/\$ ↾_t
42	7, 36, 41	mp2an 679	. . . . . . . . . . 11 ↾_t
43	42	eltopss 19949	. . . . . . . . . 10 ↾_t $/\$ ↾_t
44	31, 43	mpan 677	. . . . . . . . 9 ↾_t
45	44	sselda 3434	. . . . . . . 8 ↾_t $/\$
46		2rp 11314	. . . . . . . . . . . . . . . . 17
47		rpdivcl 11332	. . . . . . . . . . . . . . . . 17 $/\$
48	46, 47	mpan 677	. . . . . . . . . . . . . . . 16
49	48	rpred 11348	. . . . . . . . . . . . . . 15
50		ceicl 12077	. . . . . . . . . . . . . . 15
51	49, 50	syl 17	. . . . . . . . . . . . . 14
52		0red 9649	. . . . . . . . . . . . . . 15
53	51	zred 11047	. . . . . . . . . . . . . . 15
54	48	rpgt0d 11351	. . . . . . . . . . . . . . 15
55		ceige 12079	. . . . . . . . . . . . . . . 16
56	49, 55	syl 17	. . . . . . . . . . . . . . 15
57	52, 49, 53, 54, 56	ltletrd 9800	. . . . . . . . . . . . . 14
58		elnnz 10954	. . . . . . . . . . . . . 14 $/\$
59	51, 57, 58	sylanbrc 671	. . . . . . . . . . . . 13
60		fveq2 5870	. . . . . . . . . . . . . . 15
61		oveq2 6303	. . . . . . . . . . . . . . . . . 18
62	61	oveq2d 6311	. . . . . . . . . . . . . . . . 17
63	62	eleq2d 2516	. . . . . . . . . . . . . . . 16
64	63	ralbidv 2829	. . . . . . . . . . . . . . 15
65	60, 64	rexeqbidv 3004	. . . . . . . . . . . . . 14
66	65	rspcv 3148	. . . . . . . . . . . . 13
67	59, 66	syl 17	. . . . . . . . . . . 12
68	67	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
69		uznnssnn 11213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	59, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	70	sseld 3433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
72	71	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
73	72	imdistani 697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	59	nnrpd 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	48, 74	lerecd 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	56, 75	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		rpcn 11317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78		rpne0 11324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79		2cn 10687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80		2ne0 10709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
81		recdiv 10320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
82	79, 80, 81	mpanl12 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
83	77, 78, 82	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
84	76, 83	breqtrd 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85	84	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
86		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
87	86, 8	eleq2s 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
88	87	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
89	88	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
90	33, 89	sseldi 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
91		simp-4l 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
92		simplr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
93	91, 92	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
94		poimirlem30.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	94	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
96		xp1st 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
98	95, 96, 97	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
99	98	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
100	99	nn0red 10933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
101		simplr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
102	100, 101	nndivred 10665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
103	93, 102	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 103	resubcld 10054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	recnd 9674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	abscld 13510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
107	59	nnrecred 10662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	107	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
109		rphalfcl 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110	109	rpred 11348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111	110	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
112		ltletr 9730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
113	106, 108, 111, 112	syl3anc 1269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	85, 113	mpan2d 681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
115	73, 114	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
117	70	sselda 3434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	116, 117	anim12i 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
119	118	anassrs 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
120		1re 9647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
121		snssi 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		0re 9648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
124		snssi 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	122, 125	unssi 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127		1ex 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
128	127	fconst 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
129		c0ex 9642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
130	129	fconst 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131	128, 130	pm3.2i 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
132		xp2nd 6829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
133	95, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
134		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135		f1oeq1 5810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
136	134, 135	elab 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
137	133, 136	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
138		dff1o3 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
139	138	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
140		imain 5664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
141	137, 139, 140	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
142		elfznn0 11894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
143	142	nn0red 10933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
144	143	ltp1d 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
145		fzdisj 11833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
147	146	imaeq2d 5171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
148		ima0 5186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149	147, 148	syl6eq 2503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150	141, 149	sylan9req 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
151		fun 5751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
152	131, 150, 151	sylancr 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
153		imaundi 5251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
154		nn0p1nn 10916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
155	142, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
156		nnuz 11201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
157	155, 156	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
158		elfzuz3 11804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
159		fzsplit2 11831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
160	157, 158, 159	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
161	160	imaeq2d 5171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
162		f1ofo 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
163		foima 5803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
164	137, 162, 163	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
165	161, 164	sylan9req 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
166	165	ancoms 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
167	153, 166	syl5eqr 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
168	167	feq2d 5720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
169	152, 168	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
170	169	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
171	126, 170	sseldi 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
172		simpllr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	171, 172	nndivred 10665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
174	173	recnd 9674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
175	174	absnegd 13523	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
176	119, 175	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
177	119, 170	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
178		elun 3576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\/$
179	177, 178	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
180		nnrecre 10653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
181		nnrp 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
182	181	rpreccld 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
183	182	rpge0d 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	180, 183	absidd 13496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	117, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
186	117	nnrecred 10662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
187	107	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
188	110	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
189		eluzle 11178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
190	189	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
191	59	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
192	191	nnrpd 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
193	117	nnrpd 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
194	192, 193	lerecd 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
195	190, 194	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
196	84	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
197	186, 187, 188, 195, 196	letrd 9797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
198	185, 197	eqbrtrd 4426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
199		elsni 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200	199	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
201	200	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
202	201	breq1d 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203	198, 202	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
204	109	rpge0d 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
205		nncn 10624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
206		nnne0 10649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
207	205, 206	div0d 10389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
208	207	abs00bd 13366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
209	208	breq1d 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210	209	biimparc 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
211	204, 210	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
212	117, 211	syldan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
213		elsni 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
214	213	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
215	214	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	215	breq1d 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	212, 216	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
218	203, 217	jaod 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$
219	218	adantll 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\/$
220	219	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
221	179, 220	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
222	176, 221	eqbrtrd 4426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
223	73, 106	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
224		simpll 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
225	224	anim1i 572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
226	173	renegcld 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
227	225, 226	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
228	227	recnd 9674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	abscld 13510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
230	73, 229	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
231	110, 110	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
232	231	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		ltleadd 10104	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
234	223, 230, 232, 233	syl21anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
235	222, 234	mpan2d 681	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
236	105, 228	abstrid 13530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
237	104, 227	readdcld 9675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
238	237	recnd 9674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
239	238	abscld 13510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
240	106, 229	readdcld 9675	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
241	110, 110	readdcld 9675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
242	241	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
243		lelttr 9729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
244	239, 240, 242, 243	syl3anc 1269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	236, 244	mpand 682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
246	73, 245	sylanl1 656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$