poimirlem29 - Mathbox for Brendan Leahy

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

Theorem poimirlem29 31883

Description: Lemma for poimir 31887 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 12185	. . . . . . . . . . . . 13
3		retop 21769	. . . . . . . . . . . . . 14
4	3	fconst6 5787	. . . . . . . . . . . . 13
5		pttop 20584	. . . . . . . . . . . . 13 $/\$
6	2, 4, 5	mp2an 676	. . . . . . . . . . . 12
7	1, 6	eqeltri 2506	. . . . . . . . . . 11
8		poimir.i	. . . . . . . . . . . 12
9		ovex 6330	. . . . . . . . . . . 12
10	8, 9	eqeltri 2506	. . . . . . . . . . 11
11		elrest 15314	. . . . . . . . . . 11 $/\$ ↾_t
12	7, 10, 11	mp2an 676	. . . . . . . . . 10 ↾_t
13		eqid 2422	. . . . . . . . . . . . . 14
14	1, 13	ptrecube 31854	. . . . . . . . . . . . 13 $/\$
15	14	ex 435	. . . . . . . . . . . 12
16		inss1 3682	. . . . . . . . . . . . . . 15
17		sseq1 3485	. . . . . . . . . . . . . . 15
18	16, 17	mpbiri 236	. . . . . . . . . . . . . 14
19	18	sseld 3463	. . . . . . . . . . . . 13
20		ssrin 3687	. . . . . . . . . . . . . . 15
21		sseq2 3486	. . . . . . . . . . . . . . 15
22	20, 21	syl5ibr 224	. . . . . . . . . . . . . 14
23	22	reximdv 2899	. . . . . . . . . . . . 13
24	19, 23	imim12d 77	. . . . . . . . . . . 12
25	15, 24	syl5com 31	. . . . . . . . . . 11
26	25	rexlimiv 2911	. . . . . . . . . 10
27	12, 26	sylbi 198	. . . . . . . . 9 ↾_t
28	27	imp 430	. . . . . . . 8 ↾_t $/\$
29	28	adantl 467	. . . . . . 7 $/\$ ↾_t $/\$
30		resttop 20163	. . . . . . . . . . 11 $/\$ ↾_t
31	7, 10, 30	mp2an 676	. . . . . . . . . 10 ↾_t
32		reex 9631	. . . . . . . . . . . . . 14
33		unitssre 11780	. . . . . . . . . . . . . 14
34		mapss 7519	. . . . . . . . . . . . . 14 $/\$
35	32, 33, 34	mp2an 676	. . . . . . . . . . . . 13
36	8, 35	eqsstri 3494	. . . . . . . . . . . 12
37		ovex 6330	. . . . . . . . . . . . . 14
38		uniretop 21770	. . . . . . . . . . . . . . 15
39	1, 38	ptuniconst 20600	. . . . . . . . . . . . . 14 $/\$
40	37, 3, 39	mp2an 676	. . . . . . . . . . . . 13
41	40	restuni 20165	. . . . . . . . . . . 12 $/\$ ↾_t
42	7, 36, 41	mp2an 676	. . . . . . . . . . 11 ↾_t
43	42	eltopss 19924	. . . . . . . . . 10 ↾_t $/\$ ↾_t
44	31, 43	mpan 674	. . . . . . . . 9 ↾_t
45	44	sselda 3464	. . . . . . . 8 ↾_t $/\$
46		2rp 11308	. . . . . . . . . . . . . . . . 17
47		rpdivcl 11326	. . . . . . . . . . . . . . . . 17 $/\$
48	46, 47	mpan 674	. . . . . . . . . . . . . . . 16
49	48	rpred 11342	. . . . . . . . . . . . . . 15
50		ceicl 12070	. . . . . . . . . . . . . . 15
51	49, 50	syl 17	. . . . . . . . . . . . . 14
52		0red 9645	. . . . . . . . . . . . . . 15
53	51	zred 11041	. . . . . . . . . . . . . . 15
54	48	rpgt0d 11345	. . . . . . . . . . . . . . 15
55		ceige 12072	. . . . . . . . . . . . . . . 16
56	49, 55	syl 17	. . . . . . . . . . . . . . 15
57	52, 49, 53, 54, 56	ltletrd 9796	. . . . . . . . . . . . . 14
58		elnnz 10948	. . . . . . . . . . . . . 14 $/\$
59	51, 57, 58	sylanbrc 668	. . . . . . . . . . . . 13
60		fveq2 5878	. . . . . . . . . . . . . . 15
61		oveq2 6310	. . . . . . . . . . . . . . . . . 18
62	61	oveq2d 6318	. . . . . . . . . . . . . . . . 17
63	62	eleq2d 2492	. . . . . . . . . . . . . . . 16
64	63	ralbidv 2864	. . . . . . . . . . . . . . 15
65	60, 64	rexeqbidv 3040	. . . . . . . . . . . . . 14
66	65	rspcv 3178	. . . . . . . . . . . . 13
67	59, 66	syl 17	. . . . . . . . . . . 12
68	67	adantl 467	. . . . . . . . . . 11 $/\$ $/\$
69		uznnssnn 11207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	59, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	70	sseld 3463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
72	71	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
73	72	imdistani 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	59	nnrpd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	48, 74	lerecd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	56, 75	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		rpcn 11311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78		rpne0 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79		2cn 10681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80		2ne0 10703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
81		recdiv 10314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
82	79, 80, 81	mpanl12 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
83	77, 78, 82	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
84	76, 83	breqtrd 4445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85	84	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
86		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
87	86, 8	eleq2s 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
88	87	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
89	88	ffvelrnda 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
90	33, 89	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
91		simp-4l 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
92		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
93	91, 92	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
94		poimirlem30.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	94	ffvelrnda 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
96		xp1st 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
98	95, 96, 97	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
99	98	ffvelrnda 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
100	99	nn0red 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
101		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
102	100, 101	nndivred 10659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
103	93, 102	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 103	resubcld 10048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	recnd 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	abscld 13486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
107	59	nnrecred 10656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	107	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
109		rphalfcl 11328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110	109	rpred 11342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111	110	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
112		ltletr 9726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
113	106, 108, 111, 112	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	85, 113	mpan2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
115	73, 114	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
117	70	sselda 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	116, 117	anim12i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
119	118	anassrs 652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
120		1re 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
121		snssi 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		0re 9644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
124		snssi 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	122, 125	unssi 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127		1ex 9639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
128	127	fconst 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
129		c0ex 9638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
130	129	fconst 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131	128, 130	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
132		xp2nd 6835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
133	95, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
134		fvex 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135		f1oeq1 5819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
136	134, 135	elab 3218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
137	133, 136	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
138		dff1o3 5834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
139	138	simprbi 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
140		imain 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
141	137, 139, 140	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
142		elfznn0 11888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
143	142	nn0red 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
144	143	ltp1d 10538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
145		fzdisj 11827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
147	146	imaeq2d 5184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
148		ima0 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149	147, 148	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150	141, 149	sylan9req 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
151		fun 5760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
152	131, 150, 151	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
153		imaundi 5264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
154		nn0p1nn 10910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
155	142, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
156		nnuz 11195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
157	155, 156	syl6eleq 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
158		elfzuz3 11798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
159		fzsplit2 11825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
160	157, 158, 159	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
161	160	imaeq2d 5184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
162		f1ofo 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
163		foima 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
164	137, 162, 163	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
165	161, 164	sylan9req 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
166	165	ancoms 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
167	153, 166	syl5eqr 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
168	167	feq2d 5730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
169	152, 168	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
170	169	ffvelrnda 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
171	126, 170	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
172		simpllr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	171, 172	nndivred 10659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
174	173	recnd 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
175	174	absnegd 13499	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
176	119, 175	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
177	119, 170	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
178		elun 3606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\/$
179	177, 178	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
180		nnrecre 10647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
181		nnrp 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
182	181	rpreccld 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
183	182	rpge0d 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	180, 183	absidd 13473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	117, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
186	117	nnrecred 10656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
187	107	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
188	110	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
189		eluzle 11172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
190	189	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
191	59	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
192	191	nnrpd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
193	117	nnrpd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
194	192, 193	lerecd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
195	190, 194	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
196	84	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
197	186, 187, 188, 195, 196	letrd 9793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
198	185, 197	eqbrtrd 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
199		elsni 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200	199	oveq1d 6317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
201	200	fveq2d 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
202	201	breq1d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203	198, 202	syl5ibrcom 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
204	109	rpge0d 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
205		nncn 10618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
206		nnne0 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
207	205, 206	div0d 10383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
208	207	abs00bd 13343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
209	208	breq1d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210	209	biimparc 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
211	204, 210	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
212	117, 211	syldan 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
213		elsni 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
214	213	oveq1d 6317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
215	214	fveq2d 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	215	breq1d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	212, 216	syl5ibrcom 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
218	203, 217	jaod 381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$
219	218	adantll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\/$
220	219	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
221	179, 220	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
222	176, 221	eqbrtrd 4441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
223	73, 106	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
224		simpll 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
225	224	anim1i 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
226	173	renegcld 10047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
227	225, 226	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
228	227	recnd 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	abscld 13486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
230	73, 229	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
231	110, 110	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
232	231	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		ltleadd 10098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
234	223, 230, 232, 233	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
235	222, 234	mpan2d 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
236	105, 228	abstrid 13506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
237	104, 227	readdcld 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
238	237	recnd 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
239	238	abscld 13486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
240	106, 229	readdcld 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
241	110, 110	readdcld 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
242	241	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
243		lelttr 9725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
244	239, 240, 242, 243	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	236, 244	mpand 679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
246	73, 245	sylanl1 654	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$