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 32033

Description: Lemma for poimir 32037 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 12223	. . . . . . . . . . . . 13
3		retop 21860	. . . . . . . . . . . . . 14
4	3	fconst6 5786	. . . . . . . . . . . . 13
5		pttop 20674	. . . . . . . . . . . . 13 $/\$
6	2, 4, 5	mp2an 686	. . . . . . . . . . . 12
7	1, 6	eqeltri 2545	. . . . . . . . . . 11
8		poimir.i	. . . . . . . . . . . 12
9		ovex 6336	. . . . . . . . . . . 12
10	8, 9	eqeltri 2545	. . . . . . . . . . 11
11		elrest 15404	. . . . . . . . . . 11 $/\$ ↾_t
12	7, 10, 11	mp2an 686	. . . . . . . . . 10 ↾_t
13		eqid 2471	. . . . . . . . . . . . . 14
14	1, 13	ptrecube 32004	. . . . . . . . . . . . 13 $/\$
15	14	ex 441	. . . . . . . . . . . 12
16		inss1 3643	. . . . . . . . . . . . . . 15
17		sseq1 3439	. . . . . . . . . . . . . . 15
18	16, 17	mpbiri 241	. . . . . . . . . . . . . 14
19	18	sseld 3417	. . . . . . . . . . . . 13
20		ssrin 3648	. . . . . . . . . . . . . . 15
21		sseq2 3440	. . . . . . . . . . . . . . 15
22	20, 21	syl5ibr 229	. . . . . . . . . . . . . 14
23	22	reximdv 2857	. . . . . . . . . . . . 13
24	19, 23	imim12d 76	. . . . . . . . . . . 12
25	15, 24	syl5com 30	. . . . . . . . . . 11
26	25	rexlimiv 2867	. . . . . . . . . 10
27	12, 26	sylbi 200	. . . . . . . . 9 ↾_t
28	27	imp 436	. . . . . . . 8 ↾_t $/\$
29	28	adantl 473	. . . . . . 7 $/\$ ↾_t $/\$
30		resttop 20253	. . . . . . . . . . 11 $/\$ ↾_t
31	7, 10, 30	mp2an 686	. . . . . . . . . 10 ↾_t
32		reex 9648	. . . . . . . . . . . . . 14
33		unitssre 11805	. . . . . . . . . . . . . 14
34		mapss 7532	. . . . . . . . . . . . . 14 $/\$
35	32, 33, 34	mp2an 686	. . . . . . . . . . . . 13
36	8, 35	eqsstri 3448	. . . . . . . . . . . 12
37		ovex 6336	. . . . . . . . . . . . . 14
38		uniretop 21861	. . . . . . . . . . . . . . 15
39	1, 38	ptuniconst 20690	. . . . . . . . . . . . . 14 $/\$
40	37, 3, 39	mp2an 686	. . . . . . . . . . . . 13
41	40	restuni 20255	. . . . . . . . . . . 12 $/\$ ↾_t
42	7, 36, 41	mp2an 686	. . . . . . . . . . 11 ↾_t
43	42	eltopss 20014	. . . . . . . . . 10 ↾_t $/\$ ↾_t
44	31, 43	mpan 684	. . . . . . . . 9 ↾_t
45	44	sselda 3418	. . . . . . . 8 ↾_t $/\$
46		2rp 11330	. . . . . . . . . . . . . . . . 17
47		rpdivcl 11348	. . . . . . . . . . . . . . . . 17 $/\$
48	46, 47	mpan 684	. . . . . . . . . . . . . . . 16
49	48	rpred 11364	. . . . . . . . . . . . . . 15
50		ceicl 12103	. . . . . . . . . . . . . . 15
51	49, 50	syl 17	. . . . . . . . . . . . . 14
52		0red 9662	. . . . . . . . . . . . . . 15
53	51	zred 11063	. . . . . . . . . . . . . . 15
54	48	rpgt0d 11367	. . . . . . . . . . . . . . 15
55		ceige 12105	. . . . . . . . . . . . . . . 16
56	49, 55	syl 17	. . . . . . . . . . . . . . 15
57	52, 49, 53, 54, 56	ltletrd 9812	. . . . . . . . . . . . . 14
58		elnnz 10971	. . . . . . . . . . . . . 14 $/\$
59	51, 57, 58	sylanbrc 677	. . . . . . . . . . . . 13
60		fveq2 5879	. . . . . . . . . . . . . . 15
61		oveq2 6316	. . . . . . . . . . . . . . . . . 18
62	61	oveq2d 6324	. . . . . . . . . . . . . . . . 17
63	62	eleq2d 2534	. . . . . . . . . . . . . . . 16
64	63	ralbidv 2829	. . . . . . . . . . . . . . 15
65	60, 64	rexeqbidv 2988	. . . . . . . . . . . . . 14
66	65	rspcv 3132	. . . . . . . . . . . . 13
67	59, 66	syl 17	. . . . . . . . . . . 12
68	67	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
69		uznnssnn 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	59, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	70	sseld 3417	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
72	71	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
73	72	imdistani 704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	59	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	48, 74	lerecd 11383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	56, 75	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		rpcn 11333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78		rpne0 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79		2cn 10702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80		2ne0 10724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
81		recdiv 10335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
82	79, 80, 81	mpanl12 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
83	77, 78, 82	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
84	76, 83	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85	84	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
86		elmapi 7511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
87	86, 8	eleq2s 2567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
88	87	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
89	88	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
90	33, 89	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
91		simp-4l 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
92		simplr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
93	91, 92	jca 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
94		poimirlem30.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	94	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
96		xp1st 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97		elmapi 7511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
98	95, 96, 97	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
99	98	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
100	99	nn0red 10950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
101		simplr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
102	100, 101	nndivred 10680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
103	93, 102	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 103	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	abscld 13575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
107	59	nnrecred 10677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	107	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
109		rphalfcl 11350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110	109	rpred 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111	110	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
112		ltletr 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
113	106, 108, 111, 112	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	85, 113	mpan2d 688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
115	73, 114	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
117	70	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	116, 117	anim12i 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
119	118	anassrs 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
120		1re 9660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
121		snssi 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		0re 9661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
124		snssi 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	122, 125	unssi 3600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127		1ex 9656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
128	127	fconst 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
129		c0ex 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
130	129	fconst 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131	128, 130	pm3.2i 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
132		xp2nd 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
133	95, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
134		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135		f1oeq1 5818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
136	134, 135	elab 3173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
137	133, 136	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
138		dff1o3 5834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
139	138	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
140		imain 5669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
141	137, 139, 140	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
142		elfznn0 11913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
143	142	nn0red 10950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
144	143	ltp1d 10559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
145		fzdisj 11852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
147	146	imaeq2d 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
148		ima0 5189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149	147, 148	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150	141, 149	sylan9req 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
151		fun 5758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
152	131, 150, 151	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
153		imaundi 5254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
154		nn0p1nn 10933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
155	142, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
156		nnuz 11218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
157	155, 156	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
158		elfzuz3 11823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
159		fzsplit2 11850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
160	157, 158, 159	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
161	160	imaeq2d 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
162		f1ofo 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
163		foima 5811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
164	137, 162, 163	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
165	161, 164	sylan9req 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
166	165	ancoms 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
167	153, 166	syl5eqr 2519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
168	167	feq2d 5725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
169	152, 168	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
170	169	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
171	126, 170	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
172		simpllr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	171, 172	nndivred 10680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
174	173	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
175	174	absnegd 13588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
176	119, 175	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
177	119, 170	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
178		elun 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\/$
179	177, 178	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
180		nnrecre 10668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
181		nnrp 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
182	181	rpreccld 11374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
183	182	rpge0d 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	180, 183	absidd 13561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	117, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
186	117	nnrecred 10677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
187	107	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
188	110	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
189		eluzle 11195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
190	189	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
191	59	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
192	191	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
193	117	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
194	192, 193	lerecd 11383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
195	190, 194	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
196	84	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
197	186, 187, 188, 195, 196	letrd 9809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
198	185, 197	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
199		elsni 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200	199	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
201	200	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
202	201	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203	198, 202	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
204	109	rpge0d 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
205		nncn 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
206		nnne0 10664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
207	205, 206	div0d 10404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
208	207	abs00bd 13431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
209	208	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210	209	biimparc 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
211	204, 210	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
212	117, 211	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
213		elsni 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
214	213	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
215	214	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	215	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	212, 216	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
218	203, 217	jaod 387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$
219	218	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\/$
220	219	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
221	179, 220	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
222	176, 221	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
223	73, 106	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
224		simpll 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
225	224	anim1i 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
226	173	renegcld 10067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
227	225, 226	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
228	227	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	abscld 13575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
230	73, 229	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
231	110, 110	jca 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
232	231	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		ltleadd 10118	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
234	223, 230, 232, 233	syl21anc 1291	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
235	222, 234	mpan2d 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
236	105, 228	abstrid 13595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
237	104, 227	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
238	237	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
239	238	abscld 13575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
240	106, 229	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
241	110, 110	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
242	241	ad4antlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
243		lelttr 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
244	239, 240, 242, 243	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	236, 244	mpand 689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
246	73, 245	sylanl1 662	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$