poimirlem31 - Mathbox for Brendan Leahy

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

Theorem poimirlem31 33440

Description: Lemma for poimir 33442, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 33439 and poimirlem28 33437. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimir.i
poimir.r
poimir.1	↾_t
poimir.2	$/\$ $/\$ $/\$
poimirlem31.p
poimirlem31.3
poimirlem31.4	$/\$ ..^
poimirlem31.5	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
poimirlem31	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem poimirlem31 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpri 4197	. . . 4 $\/$
2		simprr 796	. . . . . . 7 $/\$ $/\$
3		1eluzge0 11732	. . . . . . . . . . 11
4		fzss1 12380	. . . . . . . . . . 11
5	3, 4	ax-mp 5	. . . . . . . . . 10
6	5	sseli 3599	. . . . . . . . 9
7	6	anim2i 593	. . . . . . . 8 $/\$ $/\$
8		eleq1 2689	. . . . . . . . . . . . 13
9	8	anbi2d 740	. . . . . . . . . . . 12 $/\$ $/\$
10	9	anbi2d 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
11		eqeq1 2626	. . . . . . . . . . . 12 $/\$ $/\$
12	11	rexbidv 3052	. . . . . . . . . . 11 $/\$ $/\$
13	10, 12	imbi12d 334	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		poimirlem31.5	. . . . . . . . . 10 $/\$ $/\$ $/\$
15	13, 14	chvarv 2263	. . . . . . . . 9 $/\$ $/\$ $/\$
16		elfzle1 12344	. . . . . . . . . . . . 13
17		1re 10039	. . . . . . . . . . . . . 14
18		elfzelz 12342	. . . . . . . . . . . . . . 15
19	18	zred 11482	. . . . . . . . . . . . . 14
20		lenlt 10116	. . . . . . . . . . . . . 14 $/\$
21	17, 19, 20	sylancr 695	. . . . . . . . . . . . 13
22	16, 21	mpbid 222	. . . . . . . . . . . 12
23		elsni 4194	. . . . . . . . . . . . 13
24		0lt1 10550	. . . . . . . . . . . . 13
25	23, 24	syl6eqbr 4692	. . . . . . . . . . . 12
26	22, 25	nsyl 135	. . . . . . . . . . 11
27		ltso 10118	. . . . . . . . . . . . . . 15
28		snfi 8038	. . . . . . . . . . . . . . . . 17
29		fzfi 12771	. . . . . . . . . . . . . . . . . 18
30		rabfi 8185	. . . . . . . . . . . . . . . . . 18 $/\$
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$
32		unfi 8227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33	28, 31, 32	mp2an 708	. . . . . . . . . . . . . . . 16 $/\$
34		c0ex 10034	. . . . . . . . . . . . . . . . . 18
35	34	snid 4208	. . . . . . . . . . . . . . . . 17
36		elun1 3780	. . . . . . . . . . . . . . . . 17 $/\$
37		ne0i 3921	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	35, 36, 37	mp2b 10	. . . . . . . . . . . . . . . 16 $/\$
39		0re 10040	. . . . . . . . . . . . . . . . . 18
40		snssi 4339	. . . . . . . . . . . . . . . . . 18
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17
42		ssrab2 3687	. . . . . . . . . . . . . . . . . 18 $/\$
43	18	ssriv 3607	. . . . . . . . . . . . . . . . . . 19
44		zssre 11384	. . . . . . . . . . . . . . . . . . 19
45	43, 44	sstri 3612	. . . . . . . . . . . . . . . . . 18
46	42, 45	sstri 3612	. . . . . . . . . . . . . . . . 17 $/\$
47	41, 46	unssi 3788	. . . . . . . . . . . . . . . 16 $/\$
48	33, 38, 47	3pm3.2i 1239	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
49		fisupcl 8375	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	27, 48, 49	mp2an 708	. . . . . . . . . . . . . 14 $/\$ $/\$
51		eleq1 2689	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
52	50, 51	mpbiri 248	. . . . . . . . . . . . 13 $/\$ $/\$
53		elun 3753	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$
54	52, 53	sylib 208	. . . . . . . . . . . 12 $/\$ $\/$ $/\$
55		oveq2 6658	. . . . . . . . . . . . . . . 16
56	55	raleqdv 3144	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	elrab 3363	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
58		elfzuz 12338	. . . . . . . . . . . . . . . 16
59		eluzfz2 12349	. . . . . . . . . . . . . . . 16
60	58, 59	syl 17	. . . . . . . . . . . . . . 15
61		simpl 473	. . . . . . . . . . . . . . . 16 $/\$
62	61	ralimi 2952	. . . . . . . . . . . . . . 15 $/\$
63		fveq2 6191	. . . . . . . . . . . . . . . . 17
64	63	breq2d 4665	. . . . . . . . . . . . . . . 16
65	64	rspcva 3307	. . . . . . . . . . . . . . 15 $/\$
66	60, 62, 65	syl2an 494	. . . . . . . . . . . . . 14 $/\$ $/\$
67	57, 66	sylbi 207	. . . . . . . . . . . . 13 $/\$
68	67	orim2i 540	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
69	54, 68	syl 17	. . . . . . . . . . 11 $/\$ $\/$
70		orel1 397	. . . . . . . . . . 11 $\/$
71	26, 69, 70	syl2im 40	. . . . . . . . . 10 $/\$
72	71	reximdv 3016	. . . . . . . . 9 $/\$
73	15, 72	syl5 34	. . . . . . . 8 $/\$ $/\$
74	7, 73	sylan2i 687	. . . . . . 7 $/\$ $/\$
75	2, 74	mpcom 38	. . . . . 6 $/\$ $/\$
76		breq 4655	. . . . . . 7
77	76	rexbidv 3052	. . . . . 6
78	75, 77	syl5ibrcom 237	. . . . 5 $/\$ $/\$
79		poimir.0	. . . . . . . . . . . . . . . 16
80	79	nnzd 11481	. . . . . . . . . . . . . . 15
81		elfzm1b 12418	. . . . . . . . . . . . . . 15 $/\$
82	18, 80, 81	syl2anr 495	. . . . . . . . . . . . . 14 $/\$
83	82	biimpd 219	. . . . . . . . . . . . 13 $/\$
84	83	ex 450	. . . . . . . . . . . 12
85	84	pm2.43d 53	. . . . . . . . . . 11
86	79	nncnd 11036	. . . . . . . . . . . . . . 15
87		npcan1 10455	. . . . . . . . . . . . . . 15
88	86, 87	syl 17	. . . . . . . . . . . . . 14
89		nnm1nn0 11334	. . . . . . . . . . . . . . . . 17
90	79, 89	syl 17	. . . . . . . . . . . . . . . 16
91	90	nn0zd 11480	. . . . . . . . . . . . . . 15
92		uzid 11702	. . . . . . . . . . . . . . 15
93		peano2uz 11741	. . . . . . . . . . . . . . 15
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . 14
95	88, 94	eqeltrrd 2702	. . . . . . . . . . . . 13
96		fzss2 12381	. . . . . . . . . . . . 13
97	95, 96	syl 17	. . . . . . . . . . . 12
98	97	sseld 3602	. . . . . . . . . . 11
99	85, 98	syld 47	. . . . . . . . . 10
100	99	anim2d 589	. . . . . . . . 9 $/\$ $/\$
101	100	imp 445	. . . . . . . 8 $/\$ $/\$ $/\$
102		ovex 6678	. . . . . . . . 9
103		eleq1 2689	. . . . . . . . . . . 12
104	103	anbi2d 740	. . . . . . . . . . 11 $/\$ $/\$
105	104	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
106		eqeq1 2626	. . . . . . . . . . 11 $/\$ $/\$
107	106	rexbidv 3052	. . . . . . . . . 10 $/\$ $/\$
108	105, 107	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	102, 108, 14	vtocl 3259	. . . . . . . 8 $/\$ $/\$ $/\$
110	101, 109	syldan 487	. . . . . . 7 $/\$ $/\$ $/\$
111		eleq1 2689	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
112	50, 111	mpbiri 248	. . . . . . . . . . . . . . 15 $/\$ $/\$
113		elun 3753	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
114	102	elsn 4192	. . . . . . . . . . . . . . . . 17
115		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
116	115	raleqdv 3144	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
117	116	elrab 3363	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	114, 117	orbi12i 543	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $\/$ $/\$ $/\$
119	113, 118	bitri 264	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $/\$
120	112, 119	sylib 208	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$
121	120	a1i 11	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
122		ltm1 10863	. . . . . . . . . . . . . . . . . 18
123		peano2rem 10348	. . . . . . . . . . . . . . . . . . 19
124		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 $/\$
125	123, 124	mpancom 703	. . . . . . . . . . . . . . . . . 18
126	122, 125	mpbid 222	. . . . . . . . . . . . . . . . 17
127	19, 126	syl 17	. . . . . . . . . . . . . . . 16
128		breq2 4657	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	128	notbid 308	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	127, 129	syl5ibcom 235	. . . . . . . . . . . . . . 15 $/\$ $/\$
131		elun2 3781	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132		fimaxre2 10969	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
133	47, 33, 132	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	47, 38, 133	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
135	134	suprubii 10998	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
136	131, 135	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
137	136	con3i 150	. . . . . . . . . . . . . . . 16 $/\$ $/\$
138		ianor 509	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
139	138, 57	xchnxbir 323	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
140	137, 139	sylib 208	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$
141	130, 140	syl6 35	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
142		pm2.63 829	. . . . . . . . . . . . . . 15 $\/$ $/\$ $\/$ $/\$ $/\$
143	142	orcs 409	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
144	141, 143	syld 47	. . . . . . . . . . . . 13 $/\$ $/\$
145	121, 144	jcad 555	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
146		andir 912	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
147		1p0e1 11133	. . . . . . . . . . . . . . . . . 18
148	18	zcnd 11483	. . . . . . . . . . . . . . . . . . . 20
149		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . 21
150		0cn 10032	. . . . . . . . . . . . . . . . . . . . 21
151		subadd 10284	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
152	149, 150, 151	mp3an23 1416	. . . . . . . . . . . . . . . . . . . 20
153	148, 152	syl 17	. . . . . . . . . . . . . . . . . . 19
154	153	biimpa 501	. . . . . . . . . . . . . . . . . 18 $/\$
155	147, 154	syl5reqr 2671	. . . . . . . . . . . . . . . . 17 $/\$
156		1z 11407	. . . . . . . . . . . . . . . . . . . . . 22
157		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . 22
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
159		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
160		sneq 4187	. . . . . . . . . . . . . . . . . . . . 21
161	158, 159, 160	3eqtr4a 2682	. . . . . . . . . . . . . . . . . . . 20
162	161	raleqdv 3144	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	162	notbid 308	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	163	biimpd 219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
165	155, 164	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
166	165	expimpd 629	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167		ralun 3795	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
168		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . . 25
169	148, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
170	169, 58	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23
171		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . 25
172		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25
173		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . 25
174	18, 171, 172, 173	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
175	169, 174	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . 23
176		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
177	170, 175, 176	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
178	169	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24
179		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . 25
180	18, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
181	178, 180	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . 22
183	177, 182	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21
184	183	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
185	167, 184	syl5ibr 236	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
186	185	expdimp 453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
187	186	con3d 148	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
188	187	adantrl 752	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	expimpd 629	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
190	166, 189	jaod 395	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
191	146, 190	syl5bi 232	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
192		fveq2 6191	. . . . . . . . . . . . . . . . . 18
193	192	neeq1d 2853	. . . . . . . . . . . . . . . . 17
194	64, 193	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$
195	194	ralsng 4218	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	195	notbid 308	. . . . . . . . . . . . . 14 $/\$ $/\$
197		ianor 509	. . . . . . . . . . . . . . 15 $/\$ $\/$
198		nne 2798	. . . . . . . . . . . . . . . 16
199	198	orbi2i 541	. . . . . . . . . . . . . . 15 $\/$ $\/$
200	197, 199	bitri 264	. . . . . . . . . . . . . 14 $/\$ $\/$
201	196, 200	syl6bb 276	. . . . . . . . . . . . 13 $/\$ $\/$
202	191, 201	sylibd 229	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
203	145, 202	syld 47	. . . . . . . . . . 11 $/\$ $\/$
204	203	ad2antlr 763	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\/$
205		poimir.1	. . . . . . . . . . . . . . . . . . 19 ↾_t
206		poimir.r	. . . . . . . . . . . . . . . . . . . . . 22
207		retop 22565	. . . . . . . . . . . . . . . . . . . . . . . 24
208	207	fconst6 6095	. . . . . . . . . . . . . . . . . . . . . . 23
209		pttop 21385	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	29, 208, 209	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
211	206, 210	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . 21
212		poimir.i	. . . . . . . . . . . . . . . . . . . . . 22
213		reex 10027	. . . . . . . . . . . . . . . . . . . . . . 23
214		unitssre 12319	. . . . . . . . . . . . . . . . . . . . . . 23
215		mapss 7900	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
216	213, 214, 215	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
217	212, 216	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . 21
218		uniretop 22566	. . . . . . . . . . . . . . . . . . . . . . . 24
219	206, 218	ptuniconst 21401	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
220	29, 207, 219	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
221	220	restuni 20966	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ↾_t
222	211, 217, 221	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 ↾_t
223	222, 220	cnf 21050	. . . . . . . . . . . . . . . . . . 19 ↾_t
224	205, 223	syl 17	. . . . . . . . . . . . . . . . . 18
225	224	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
226		simplr 792	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
227		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
228	227	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
230		nnre 11027	. . . . . . . . . . . . . . . . . . . . . . . . . 26
231	230	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
232		nnne0 11053	. . . . . . . . . . . . . . . . . . . . . . . . . 26
233	232	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
234	229, 231, 233	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
235		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	228, 235	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
237		nnrp 11842	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237	rpregt0d 11878	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
239		divge0 10892	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
240	236, 238, 239	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
241		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . 26
242	241	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
243		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	237	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
245	229, 243, 244	ledivmuld 11925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
246		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
247	246	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
248	247	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
249	248	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
250	245, 249	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
251	242, 250	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
252	39, 17	elicc2i 12239	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
253	234, 240, 251, 252	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
254	253	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
255		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . 24
256	255	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23
257	256	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22
258	254, 257	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . 21 $/\$
259	258	impr 649	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
260	226, 259	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
261		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
262		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
263		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264	263	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
265	264	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26
266	262, 265	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
267		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
268	267	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
269	268	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
270		elfzofz 12485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
271	269, 270	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
272		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
273	272	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
274	273	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26
275	271, 274	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
276	266, 275	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $\/$
277	261, 276	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
278	277	imp 445	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
279	278	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ ..^ $/\$
280		poimirlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25
281	280	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
282		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . 24
283		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . . 24
284	281, 282, 283	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
285		poimirlem31.4	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^
286		df-f 5892	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$ ..^
287	284, 285, 286	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
288	287	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
289		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . 25
290	289	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24
291	34	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24
292	290, 291	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
293		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
294	281, 293	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
295		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
296		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
297	295, 296	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . 26
298	294, 297	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
299		dff1o3 6143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
300	299	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . 25
301		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . 25
302	298, 300, 301	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
303		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
304	303	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
305	304	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
306		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
307	305, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
308	307	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . 25
309		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . 25
310	308, 309	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
311	302, 310	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
312		fun 6066	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
313	292, 311, 312	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
314		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . 24
315		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
316	303, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
317		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
318	316, 317	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
319		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
320		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	318, 319, 320	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
322	321	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
323		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
324		foima 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
325	298, 323, 324	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
326	322, 325	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
327	326	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
328	314, 327	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
329	328	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
330	313, 329	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
331		fzfid 12772	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
332		inidm 3822	. . . . . . . . . . . . . . . . . . . . 21
333	279, 288, 330, 331, 331, 332	off 6912	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
334		poimirlem31.p	. . . . . . . . . . . . . . . . . . . . 21
335	334	feq1i 6036	. . . . . . . . . . . . . . . . . . . 20
336	333, 335	sylibr 224	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
337		vex 3203	. . . . . . . . . . . . . . . . . . . . 21
338	337	fconst 6091	. . . . . . . . . . . . . . . . . . . 20
339	338	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
340	260, 336, 339, 331, 331, 332	off 6912	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
341	212	eleq2i 2693	. . . . . . . . . . . . . . . . . . 19
342		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
343		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
344	342, 343	elmap 7886	. . . . . . . . . . . . . . . . . . 19
345	341, 344	bitri 264	. . . . . . . . . . . . . . . . . 18
346	340, 345	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
347	225, 346	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ $/\$
348		elmapi 7879	. . . . . . . . . . . . . . . 16
349	347, 348	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
350	349	ffvelrnda 6359	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
351	350	an32s 846	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
352		0red 10041	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
353	351, 352	ltnled 10184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
354		ltle 10126	. . . . . . . . . . . . 13 $/\$
355	351, 39, 354	sylancl 694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
356	353, 355	sylbird 250	. . . . . . . . . . 11 $/\$ $/\$ $/\$
357	246, 232	div0d 10800	. . . . . . . . . . . . . . 15
358		oveq1 6657	. . . . . . . . . . . . . . . 16
359	358	eqeq1d 2624	. . . . . . . . . . . . . . 15
360	357, 359	syl5ibrcom 237	. . . . . . . . . . . . . 14
361	360	ad3antlr 767	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
362		ffn 6045	. . . . . . . . . . . . . . . . 17
363	336, 362	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
364		fnconstg 6093	. . . . . . . . . . . . . . . . 17
365	337, 364	mp1i 13	. . . . . . . . . . . . . . . 16 $/\$ $/\$
366		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
367	337	fvconst2 6469	. . . . . . . . . . . . . . . . 17
368	367	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
369	363, 365, 331, 331, 332, 366, 368	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
370	369	an32s 846	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
371	370	eqeq1d 2624	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
372	361, 371	sylibrd 249	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
373		simplll 798	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
374		simplr 792	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
375	346	adantlr 751	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
376		ovex 6678	. . . . . . . . . . . . . 14
377		eleq1 2689	. . . . . . . . . . . . . . . . 17
378		fveq1 6190	. . . . . . . . . . . . . . . . . . 19
379	378	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18
380		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
381	380	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
382	381	breq1d 4663	. . . . . . . . . . . . . . . . . 18
383	379, 382	imbi12d 334	. . . . . . . . . . . . . . . . 17
384	377, 383	imbi12d 334	. . . . . . . . . . . . . . . 16
385	384	imbi2d 330	. . . . . . . . . . . . . . 15
386	385	imbi2d 330	. . . . . . . . . . . . . 14
387		poimir.2	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
388	387	3exp2 1285	. . . . . . . . . . . . . 14
389	376, 386, 388	vtocl 3259	. . . . . . . . . . . . 13
390	373, 374, 375, 389	syl3c 66	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
391	372, 390	syld 47	. . . . . . . . . . 11 $/\$ $/\$ $/\$
392	356, 391	jaod 395	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
393	204, 392	syld 47	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
394	393	reximdva 3017	. . . . . . . 8 $/\$ $/\$ $/\$
395	394	anasss 679	. . . . . . 7 $/\$ $/\$ $/\$
396	110, 395	mpd 15	. . . . . 6 $/\$ $/\$
397		breq 4655	. . . . . . . 8
398		fvex 6201	. . . . . . . . 9
399	34, 398	brcnv 5305	. . . . . . . 8
400	397, 399	syl6bb 276	. . . . . . 7
401	400	rexbidv 3052	. . . . . 6
402	396, 401	syl5ibrcom 237	. . . . 5 $/\$ $/\$
403	78, 402	jaod 395	. . . 4 $/\$ $/\$ $\/$
404	1, 403	syl5 34	. . 3 $/\$ $/\$
405	404	exp32 631	. 2
406	405	3imp2 1282	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cpr 4179

cuni 4436 class class class wbr 4653

wor 5034

cxp 5112

ccnv 5113

crn 5115

cima 5117

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

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465 ↾_t crest 16081

ctg 16098

cpt 16099

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-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-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466 df-rest 16083 df-topgen 16104 df-pt 16105 df-top 20699 df-topon 20716 df-bases 20750 df-cn 21031

This theorem is referenced by: poimirlem32 33441

W3C validator