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 33438

Description: Lemma for poimir 33442 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 12771	. . . . . . . . . . . . 13
3		retop 22565	. . . . . . . . . . . . . 14
4	3	fconst6 6095	. . . . . . . . . . . . 13
5		pttop 21385	. . . . . . . . . . . . 13 $/\$
6	2, 4, 5	mp2an 708	. . . . . . . . . . . 12
7	1, 6	eqeltri 2697	. . . . . . . . . . 11
8		poimir.i	. . . . . . . . . . . 12
9		ovex 6678	. . . . . . . . . . . 12
10	8, 9	eqeltri 2697	. . . . . . . . . . 11
11		elrest 16088	. . . . . . . . . . 11 $/\$ ↾_t
12	7, 10, 11	mp2an 708	. . . . . . . . . 10 ↾_t
13		eqid 2622	. . . . . . . . . . . . . 14
14	1, 13	ptrecube 33409	. . . . . . . . . . . . 13 $/\$
15	14	ex 450	. . . . . . . . . . . 12
16		inss1 3833	. . . . . . . . . . . . . . 15
17		sseq1 3626	. . . . . . . . . . . . . . 15
18	16, 17	mpbiri 248	. . . . . . . . . . . . . 14
19	18	sseld 3602	. . . . . . . . . . . . 13
20		ssrin 3838	. . . . . . . . . . . . . . 15
21		sseq2 3627	. . . . . . . . . . . . . . 15
22	20, 21	syl5ibr 236	. . . . . . . . . . . . . 14
23	22	reximdv 3016	. . . . . . . . . . . . 13
24	19, 23	imim12d 81	. . . . . . . . . . . 12
25	15, 24	syl5com 31	. . . . . . . . . . 11
26	25	rexlimiv 3027	. . . . . . . . . 10
27	12, 26	sylbi 207	. . . . . . . . 9 ↾_t
28	27	imp 445	. . . . . . . 8 ↾_t $/\$
29	28	adantl 482	. . . . . . 7 $/\$ ↾_t $/\$
30		resttop 20964	. . . . . . . . . . 11 $/\$ ↾_t
31	7, 10, 30	mp2an 708	. . . . . . . . . 10 ↾_t
32		reex 10027	. . . . . . . . . . . . . 14
33		unitssre 12319	. . . . . . . . . . . . . 14
34		mapss 7900	. . . . . . . . . . . . . 14 $/\$
35	32, 33, 34	mp2an 708	. . . . . . . . . . . . 13
36	8, 35	eqsstri 3635	. . . . . . . . . . . 12
37		ovex 6678	. . . . . . . . . . . . . 14
38		uniretop 22566	. . . . . . . . . . . . . . 15
39	1, 38	ptuniconst 21401	. . . . . . . . . . . . . 14 $/\$
40	37, 3, 39	mp2an 708	. . . . . . . . . . . . 13
41	40	restuni 20966	. . . . . . . . . . . 12 $/\$ ↾_t
42	7, 36, 41	mp2an 708	. . . . . . . . . . 11 ↾_t
43	42	eltopss 20712	. . . . . . . . . 10 ↾_t $/\$ ↾_t
44	31, 43	mpan 706	. . . . . . . . 9 ↾_t
45	44	sselda 3603	. . . . . . . 8 ↾_t $/\$
46		2rp 11837	. . . . . . . . . . . . . . . . 17
47		rpdivcl 11856	. . . . . . . . . . . . . . . . 17 $/\$
48	46, 47	mpan 706	. . . . . . . . . . . . . . . 16
49	48	rpred 11872	. . . . . . . . . . . . . . 15
50		ceicl 12642	. . . . . . . . . . . . . . 15
51	49, 50	syl 17	. . . . . . . . . . . . . 14
52		0red 10041	. . . . . . . . . . . . . . 15
53	51	zred 11482	. . . . . . . . . . . . . . 15
54	48	rpgt0d 11875	. . . . . . . . . . . . . . 15
55		ceige 12644	. . . . . . . . . . . . . . . 16
56	49, 55	syl 17	. . . . . . . . . . . . . . 15
57	52, 49, 53, 54, 56	ltletrd 10197	. . . . . . . . . . . . . 14
58		elnnz 11387	. . . . . . . . . . . . . 14 $/\$
59	51, 57, 58	sylanbrc 698	. . . . . . . . . . . . 13
60		fveq2 6191	. . . . . . . . . . . . . . 15
61		oveq2 6658	. . . . . . . . . . . . . . . . . 18
62	61	oveq2d 6666	. . . . . . . . . . . . . . . . 17
63	62	eleq2d 2687	. . . . . . . . . . . . . . . 16
64	63	ralbidv 2986	. . . . . . . . . . . . . . 15
65	60, 64	rexeqbidv 3153	. . . . . . . . . . . . . 14
66	65	rspcv 3305	. . . . . . . . . . . . 13
67	59, 66	syl 17	. . . . . . . . . . . 12
68	67	adantl 482	. . . . . . . . . . 11 $/\$ $/\$
69		uznnssnn 11735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	59, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	70	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
72	71	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
73	72	imdistani 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	59	nnrpd 11870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	48, 74	lerecd 11891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	56, 75	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78		rpne0 11848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
81		recdiv 10731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
82	79, 80, 81	mpanl12 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
83	77, 78, 82	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
84	76, 83	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85	84	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
86		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
87	86, 8	eleq2s 2719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
88	87	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
89	88	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
90	33, 89	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
91		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
92		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
93	91, 92	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
94		poimirlem30.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	94	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
96		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
98	95, 96, 97	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
99	98	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
100	99	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
101		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
102	100, 101	nndivred 11069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
103	93, 102	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 103	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
107	59	nnrecred 11066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	107	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
109		rphalfcl 11858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110	109	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111	110	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
112		ltletr 10129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
113	106, 108, 111, 112	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	85, 113	mpan2d 710	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
115	73, 114	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
117	70	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	116, 117	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
119	118	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
120		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
121		snssi 4339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		0re 10040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
124		snssi 4339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	122, 125	unssi 3788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
128	127	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
129		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
130	129	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131	128, 130	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
132		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
133	95, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
134		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
136	134, 135	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
137	133, 136	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
138		dff1o3 6143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
139	138	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
140		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
141	137, 139, 140	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
142		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
143	142	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
144	143	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
145		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
147	146	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
148		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149	147, 148	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150	141, 149	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
151		fun 6066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
152	131, 150, 151	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
153		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
154		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
155	142, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
156		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
157	155, 156	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
158		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
159		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
160	157, 158, 159	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
161	160	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
162		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
163		foima 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
164	137, 162, 163	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
165	161, 164	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
166	165	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
167	153, 166	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
168	167	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
169	152, 168	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
170	169	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
171	126, 170	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
172		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	171, 172	nndivred 11069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
174	173	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
175	174	absnegd 14188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
176	119, 175	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
177	119, 170	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
178		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\/$
179	177, 178	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
180		nnrecre 11057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
181		nnrp 11842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
182	181	rpreccld 11882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
183	182	rpge0d 11876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	180, 183	absidd 14161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	117, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
186	117	nnrecred 11066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
187	107	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
188	110	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
189		eluzle 11700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
190	189	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
191	59	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
192	191	nnrpd 11870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
193	117	nnrpd 11870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
194	192, 193	lerecd 11891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
195	190, 194	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
196	84	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
197	186, 187, 188, 195, 196	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
198	185, 197	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
199		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200	199	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
201	200	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
202	201	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203	198, 202	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
204	109	rpge0d 11876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
205		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
206		nnne0 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
207	205, 206	div0d 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
208	207	abs00bd 14031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
209	208	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210	209	biimparc 504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
211	204, 210	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
212	117, 211	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
213		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
214	213	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
215	214	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	215	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	212, 216	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
218	203, 217	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$
219	218	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\/$
220	219	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
221	179, 220	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
222	176, 221	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
223	73, 106	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
224		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
225	224	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
226	173	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
227	225, 226	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
228	227	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
230	73, 229	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
231	110, 110	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
232	231	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		ltleadd 10511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
234	223, 230, 232, 233	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
235	222, 234	mpan2d 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
236	105, 228	abstrid 14195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
237	104, 227	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
238	237	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
239	238	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
240	106, 229	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
241	110, 110	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
242	241	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
243		lelttr 10128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
244	239, 240, 242, 243	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	236, 244	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
246	73, 245	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
247	115, 235, 246	3syld 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
248	100	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
249	248, 171	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
250	249, 172	nndivred 11069	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
251	119, 250	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
252	247, 251	jctild 566	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253	252	adantld 483	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
255	87	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
256	255	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
257	33, 256	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
258	74	rpreccld 11882	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
259	258	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . 26
260	259	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
261	13	rexmet 22594	. . . . . . . . . . . . . . . . . . . . . . . . . 26
262		elbl 22193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
263	261, 262	mp3an1 1411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
264	257, 260, 263	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
265		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
266	95, 96, 265	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
267		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
268		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
269	267, 268	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
270		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
271		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
272		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
273	267	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
274	273	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
275	266, 269, 270, 270, 271, 272, 274	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
276	275	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
277	224, 276	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
278	224, 102	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
279	13	remetdval 22592	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
280	257, 278, 279	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
281	277, 280	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
282	281	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
283	282	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
284	264, 283	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
285	254, 284	sylan 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
286		rpxr 11840	. . . . . . . . . . . . . . . . . . . . . . . . . 26
287	286	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
288		elbl 22193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
289	261, 288	mp3an1 1411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290	90, 287, 289	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
291		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\/$
292		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
293		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
294	293	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
295	294	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
296	292, 295	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
297		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ..^
298	297	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
299	298	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
300		elfzofz 12485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
301	299, 300	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
302		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
303	302	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
304	303	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
305	301, 304	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
306	296, 305	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $\/$
307	291, 306	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
308	307	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$
309	308	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ ..^ $/\$
310		dffn3 6054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
311	266, 310	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
312		poimirlem30.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ ..^
313	311, 312	fssd 6057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^
314	313	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^
315		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
316	309, 314, 169, 315, 315, 271	off 6912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
317		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
318	316, 317	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
319	267, 268	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
320	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
321		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
322	169, 321	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
323		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
324		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
325	320, 322, 315, 315, 271, 323, 324	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
326	273	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
327	318, 319, 315, 315, 271, 325, 326	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
328	327	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
329	225, 328	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
330	327	adantl3r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
331	330	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
332	87	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
333	332	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
334	33, 333	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
335	250	adantl3r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
336	13	remetdval 22592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
337	334, 335, 336	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
338	248	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
339	171	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
340	205	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
341	206	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
342	338, 339, 340, 341	divdird 10839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
343	102	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
344	343	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
345	344, 174	subnegd 10399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
346	342, 345	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
347	346	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
348	347	adantl3r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
349	334	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
350	102	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
351	350	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
352	351	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
353	174	adantl3r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
354	353	negcld 10379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
355	349, 352, 354	subsubd 10420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
356	348, 355	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
357	356	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
358	331, 337, 357	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
359	358	adantl3r 786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
360	77	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
361	360	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
362	361	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
363	359, 362	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
364	329, 363	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
365	290, 364	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
366	73, 365	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
367	253, 285, 366	3imtr4d 283	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
368	367	ralimdva 2962	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
369		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
370		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
371	370	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
372		nndivre 11056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
373	371, 372	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
374		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
375	371, 374	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
376	181	rpregt0d 11878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
377		divge0 10892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
378	375, 376, 377	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
379		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
380	379	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
381	371	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
382		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
383	181	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
384	381, 382, 383	ledivmuld 11925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
385	205	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
386	385	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
387	386	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
388	384, 387	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
389	380, 388	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
390	123, 120	elicc2i 12239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
391	373, 378, 389, 390	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
392	391	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
393		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
394	393	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
395	394	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26
396	392, 395	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
397	396	impr 649	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
398	369, 397	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
399	267	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24
400	399	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
401	398, 316, 400, 315, 315, 271	off 6912	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
402		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 22
403	401, 402	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
404	119, 403	sylan 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
405	368, 404	jctild 566	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
406	8	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . 22
407		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
408	407, 37	elmap 7886	. . . . . . . . . . . . . . . . . . . . . 22
409	406, 408	bitri 264	. . . . . . . . . . . . . . . . . . . . 21
410	401, 409	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
411	119, 410	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
412	405, 411	jctird 567	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
413		elin 3796	. . . . . . . . . . . . . . . . . . 19 $/\$
414		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21
415	414	elixp 7915	. . . . . . . . . . . . . . . . . . . 20 $/\$
416	415	anbi1i 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
417	413, 416	bitri 264	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
418	412, 417	syl6ibr 242	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
419		ssel 3597	. . . . . . . . . . . . . . . . . 18
420	419	com12 32	. . . . . . . . . . . . . . . . 17
421	418, 420	syl6 35	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
422	421	impd 447	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
423	422	ralrimdva 2969	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
424	423	expd 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
425		poimirlem30.4	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
426	425	3exp2 1285	. . . . . . . . . . . . . . . . . . 19
427	426	imp43 621	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
428		r19.29 3072	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
429		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
430	429	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . 24
431		poimirlem30.x	. . . . . . . . . . . . . . . . . . . . . . . 24
432	430, 431	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . 23
433	432	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . 22
434	433	rspcev 3309	. . . . . . . . . . . . . . . . . . . . 21 $/\$
435	434	rexlimivw 3029	. . . . . . . . . . . . . . . . . . . 20 $/\$
436	428, 435	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$
437	436	expcom 451	. . . . . . . . . . . . . . . . . 18
438	427, 437	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
439	438	ralrimdvva 2974	. . . . . . . . . . . . . . . 16 $/\$
440	117, 439	sylan2 491	. . . . . . . . . . . . . . 15 $/\$ $/\$
441	440	anassrs 680	. . . . . . . . . . . . . 14 $/\$ $/\$
442	441	adantllr 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
443	424, 442	syl6d 75	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
444	443	rexlimdva 3031	. . . . . . . . . . 11 $/\$ $/\$
445	68, 444	syld 47	. . . . . . . . . 10 $/\$ $/\$
446	445	com23 86	. . . . . . . . 9 $/\$ $/\$
447	446	impr 649	. . . . . . . 8 $/\$ $/\$ $/\$
448	45, 447	sylanl2 683	. . . . . . 7 $/\$ ↾_t $/\$ $/\$ $/\$
449	29, 448	rexlimddv 3035	. . . . . 6 $/\$ ↾_t $/\$
450	449	expr 643	. . . . 5 $/\$ ↾_t
451	450	com23 86	. . . 4 $/\$ ↾_t
452		r19.21v 2960	. . . 4
453	451, 452	syl6ibr 242	. . 3 $/\$ ↾_t
454	453	ralrimdva 2969	. 2 ↾_t
455		ralcom 3098	. 2 ↾_t ↾_t
456	454, 455	syl6ib 241	1 ↾_t

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

cvv 3200

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cpr 4179

cuni 4436 class class class wbr 4653

cxp 5112

ccnv 5113

crn 5115

cres 5116

cima 5117

ccom 5118

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cixp 7908

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465

cfl 12591

cabs 13974 ↾_t crest 16081

ctg 16098

cpt 16099

cxmt 19731

cbl 19733

ctop 20698

ccn 21028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-rest 16083 df-topgen 16104 df-pt 16105 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750

This theorem is referenced by: poimirlem30 33439

W3C validator