poimirlem22 - Mathbox for Brendan Leahy

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

Theorem poimirlem22 33431

Description: Lemma for poimir 33442, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem22.2
poimirlem22.3	$/\$
poimirlem22.4	$/\$

**Assertion**
Ref	Expression
poimirlem22

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem22**
Step	Hyp	Ref	Expression
1		poimir.0	. . . . 5
2	1	adantr 481	. . . 4 $/\$
3		poimirlem22.s	. . . 4 ..^
4		poimirlem22.1	. . . . 5
5	4	adantr 481	. . . 4 $/\$
6		poimirlem22.2	. . . . 5
7	6	adantr 481	. . . 4 $/\$
8		simpr 477	. . . 4 $/\$
9	2, 3, 5, 7, 8	poimirlem15 33424	. . 3 $/\$ $\$
10		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
11	10	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23
12	11	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . 22
13	12	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . 21
14		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
15	14	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
16	14	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	16	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
19	16	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
21	18, 20	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . 23
22	15, 21	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22
23	22	csbeq2dv 3992	. . . . . . . . . . . . . . . . . . . . 21
24	13, 23	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
25	24	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . 19
26	25	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18
27	26, 3	elrab2 3366	. . . . . . . . . . . . . . . . 17 ..^ $/\$
28	27	simprbi 480	. . . . . . . . . . . . . . . 16
29	6, 28	syl 17	. . . . . . . . . . . . . . 15
30	29	adantr 481	. . . . . . . . . . . . . 14 $/\$
31		elrabi 3359	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
32	31, 3	eleq2s 2719	. . . . . . . . . . . . . . . . . . . 20 ..^
33	6, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
34		xp1st 7198	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
36		xp1st 7198	. . . . . . . . . . . . . . . . . 18 ..^ ..^
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ..^
38		elmapi 7879	. . . . . . . . . . . . . . . . 17 ..^ ..^
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ..^
40		elfzoelz 12470	. . . . . . . . . . . . . . . . 17 ..^
41	40	ssriv 3607	. . . . . . . . . . . . . . . 16 ..^
42		fss 6056	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
43	39, 41, 42	sylancl 694	. . . . . . . . . . . . . . 15
44	43	adantr 481	. . . . . . . . . . . . . 14 $/\$
45		xp2nd 7199	. . . . . . . . . . . . . . . . 17 ..^
46	35, 45	syl 17	. . . . . . . . . . . . . . . 16
47		fvex 6201	. . . . . . . . . . . . . . . . 17
48		f1oeq1 6127	. . . . . . . . . . . . . . . . 17
49	47, 48	elab 3350	. . . . . . . . . . . . . . . 16
50	46, 49	sylib 208	. . . . . . . . . . . . . . 15
51	50	adantr 481	. . . . . . . . . . . . . 14 $/\$
52	2, 30, 44, 51, 8	poimirlem1 33410	. . . . . . . . . . . . 13 $/\$
53	52	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
54	1	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
55		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23
57	56	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . 22
58	57	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . 21
59		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
60	59	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
61	59	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	61	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	62	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
64	61	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	64	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
66	63, 65	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . 23
67	60, 66	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22
68	67	csbeq2dv 3992	. . . . . . . . . . . . . . . . . . . . 21
69	58, 68	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
70	69	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . 19
71	70	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18
72	71, 3	elrab2 3366	. . . . . . . . . . . . . . . . 17 ..^ $/\$
73	72	simprbi 480	. . . . . . . . . . . . . . . 16
74	73	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		elrabi 3359	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
76	75, 3	eleq2s 2719	. . . . . . . . . . . . . . . . . . . 20 ..^
77		xp1st 7198	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
79		xp1st 7198	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
81		elmapi 7879	. . . . . . . . . . . . . . . . . 18 ..^ ..^
82	80, 81	syl 17	. . . . . . . . . . . . . . . . 17 ..^
83		fss 6056	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
84	82, 41, 83	sylancl 694	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86		xp2nd 7199	. . . . . . . . . . . . . . . . . 18 ..^
87	78, 86	syl 17	. . . . . . . . . . . . . . . . 17
88		fvex 6201	. . . . . . . . . . . . . . . . . 18
89		f1oeq1 6127	. . . . . . . . . . . . . . . . . 18
90	88, 89	elab 3350	. . . . . . . . . . . . . . . . 17
91	87, 90	sylib 208	. . . . . . . . . . . . . . . 16
92	91	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93		simpllr 799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94		xp2nd 7199	. . . . . . . . . . . . . . . . . 18 ..^
95	76, 94	syl 17	. . . . . . . . . . . . . . . . 17
96	95	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97		eldifsn 4317	. . . . . . . . . . . . . . . . 17 $\$ $/\$
98	97	biimpri 218	. . . . . . . . . . . . . . . 16 $/\$ $\$
99	96, 98	sylan 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
100	54, 74, 85, 92, 93, 99	poimirlem2 33411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100	ex 450	. . . . . . . . . . . . 13 $/\$ $/\$
102	101	necon1bd 2812	. . . . . . . . . . . 12 $/\$ $/\$
103	53, 102	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
104		eleq1 2689	. . . . . . . . . . . . . . . 16
105	104	biimparc 504	. . . . . . . . . . . . . . 15 $/\$
106	105	anim2i 593	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	106	anassrs 680	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	73	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
109		breq1 4656	. . . . . . . . . . . . . . . . . 18
110		id 22	. . . . . . . . . . . . . . . . . 18
111	109, 110	ifbieq1d 4109	. . . . . . . . . . . . . . . . 17
112		elfznn 12370	. . . . . . . . . . . . . . . . . . . 20
113	112	nngt0d 11064	. . . . . . . . . . . . . . . . . . 19
114	113	iftrued 4094	. . . . . . . . . . . . . . . . . 18
115	114	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	111, 115	sylan9eqr 2678	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117	116	csbeq1d 3540	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
118		c0ex 10034	. . . . . . . . . . . . . . . . . 18
119		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . 24
120		fz10 12362	. . . . . . . . . . . . . . . . . . . . . . . 24
121	119, 120	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
123	122	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
124		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25
125		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . . . 25
126	124, 125	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
127	126	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
129	128	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
130	123, 129	uneq12d 3768	. . . . . . . . . . . . . . . . . . . 20
131		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	xpeq1i 5135	. . . . . . . . . . . . . . . . . . . . . . 23
133		0xp 5199	. . . . . . . . . . . . . . . . . . . . . . 23
134	132, 133	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22
135	134	uneq1i 3763	. . . . . . . . . . . . . . . . . . . . 21
136		uncom 3757	. . . . . . . . . . . . . . . . . . . . 21
137		un0 3967	. . . . . . . . . . . . . . . . . . . . 21
138	135, 136, 137	3eqtri 2648	. . . . . . . . . . . . . . . . . . . 20
139	130, 138	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19
140	139	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
141	118, 140	csbie 3559	. . . . . . . . . . . . . . . . 17
142		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . 22
143	91, 142	syl 17	. . . . . . . . . . . . . . . . . . . . 21
144		foima 6120	. . . . . . . . . . . . . . . . . . . . 21
145	143, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20
146	145	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
147	146	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
148		ovexd 6680	. . . . . . . . . . . . . . . . . . 19
149		ffn 6045	. . . . . . . . . . . . . . . . . . . 20 ..^
150	82, 149	syl 17	. . . . . . . . . . . . . . . . . . 19
151		fnconstg 6093	. . . . . . . . . . . . . . . . . . . 20
152	118, 151	mp1i 13	. . . . . . . . . . . . . . . . . . 19
153		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 $/\$
154	118	fvconst2 6469	. . . . . . . . . . . . . . . . . . . 20
155	154	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
156	82	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
157		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . . 22 ..^
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
159	158	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . 20 $/\$
160	159	addid1d 10236	. . . . . . . . . . . . . . . . . . 19 $/\$
161	148, 150, 152, 150, 153, 155, 160	offveq 6918	. . . . . . . . . . . . . . . . . 18
162	147, 161	eqtrd 2656	. . . . . . . . . . . . . . . . 17
163	141, 162	syl5eq 2668	. . . . . . . . . . . . . . . 16
164	163	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
165	117, 164	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166		nnm1nn0 11334	. . . . . . . . . . . . . . . . 17
167	1, 166	syl 17	. . . . . . . . . . . . . . . 16
168		0elfz 12436	. . . . . . . . . . . . . . . 16
169	167, 168	syl 17	. . . . . . . . . . . . . . 15
170	169	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
171		fvexd 6203	. . . . . . . . . . . . . 14 $/\$ $/\$
172	108, 165, 170, 171	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ $/\$
173	107, 172	sylan 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
174	173	an32s 846	. . . . . . . . . . 11 $/\$ $/\$ $/\$
175	103, 174	mpdan 702	. . . . . . . . . 10 $/\$ $/\$
176		fveq2 6191	. . . . . . . . . . . . . . . 16
177	176	eleq1d 2686	. . . . . . . . . . . . . . 15
178	177	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ $/\$
179		fveq2 6191	. . . . . . . . . . . . . . . 16
180	179	fveq2d 6195	. . . . . . . . . . . . . . 15
181	180	eqeq2d 2632	. . . . . . . . . . . . . 14
182	178, 181	imbi12d 334	. . . . . . . . . . . . 13 $/\$ $/\$
183	172	expcom 451	. . . . . . . . . . . . 13 $/\$
184	182, 183	vtoclga 3272	. . . . . . . . . . . 12 $/\$
185	7, 184	mpcom 38	. . . . . . . . . . 11 $/\$
186	185	adantr 481	. . . . . . . . . 10 $/\$ $/\$
187	175, 186	eqtr3d 2658	. . . . . . . . 9 $/\$ $/\$
188	187	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$
189	1	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $/\$
190	6	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $/\$
191		simpllr 799	. . . . . . . . 9 $/\$ $/\$ $/\$
192		simplr 792	. . . . . . . . 9 $/\$ $/\$ $/\$
193	35	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^
194		xpopth 7207	. . . . . . . . . . . . . 14 ..^ $/\$ ..^ $/\$
195	78, 193, 194	syl2anr 495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
196	33	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^
197		xpopth 7207	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$
198	197	biimpd 219	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$
199	76, 196, 198	syl2anr 495	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
200	103, 199	mpan2d 710	. . . . . . . . . . . . 13 $/\$ $/\$
201	195, 200	sylbid 230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
202	187, 201	mpand 711	. . . . . . . . . . 11 $/\$ $/\$
203	202	necon3d 2815	. . . . . . . . . 10 $/\$ $/\$
204	203	imp 445	. . . . . . . . 9 $/\$ $/\$ $/\$
205	189, 3, 190, 191, 192, 204	poimirlem9 33418	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
206	103	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$
207	188, 205, 206	jca31 557	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
208	207	ex 450	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
209		simplr 792	. . . . . . . 8 $/\$ $\$ $/\$ $\$
210		elfznn 12370	. . . . . . . . . . . . . 14
211	210	nnred 11035	. . . . . . . . . . . . 13
212	211	ltp1d 10954	. . . . . . . . . . . . 13
213	211, 212	ltned 10173	. . . . . . . . . . . 12
214	213	adantl 482	. . . . . . . . . . 11 $/\$
215		fveq1 6190	. . . . . . . . . . . . 13 $\$ $\$
216		id 22	. . . . . . . . . . . . . . . . . . . . . 22
217		ltp1 10861	. . . . . . . . . . . . . . . . . . . . . 22
218	216, 217	ltned 10173	. . . . . . . . . . . . . . . . . . . . 21
219		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
220		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
221	219, 220, 220, 219	fpr 6421	. . . . . . . . . . . . . . . . . . . . 21
222	218, 221	syl 17	. . . . . . . . . . . . . . . . . . . 20
223		f1oi 6174	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
224		f1of 6137	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$ $\$ $\$
225	223, 224	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
226		disjdif 4040	. . . . . . . . . . . . . . . . . . . . 21 $\$
227		fun 6066	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
228	226, 227	mpan2 707	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
229	222, 225, 228	sylancl 694	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
230	219	prid1 4297	. . . . . . . . . . . . . . . . . . . 20
231		elun1 3780	. . . . . . . . . . . . . . . . . . . 20 $\$
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
233		fvco3 6275	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $/\$ $\$ $\$ $\$
234	229, 232, 233	sylancl 694	. . . . . . . . . . . . . . . . . 18 $\$ $\$
235		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 22
236	222, 235	syl 17	. . . . . . . . . . . . . . . . . . . . 21
237		fnresi 6008	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
238	226, 230	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
239		fvun1 6269	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
240	237, 238, 239	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . 21 $\$
241	236, 240	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$
242	219, 220	fvpr1 6456	. . . . . . . . . . . . . . . . . . . . 21
243	218, 242	syl 17	. . . . . . . . . . . . . . . . . . . 20
244	241, 243	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $\$
245	244	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $\$
246	234, 245	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $\$
247	211, 246	syl 17	. . . . . . . . . . . . . . . 16 $\$
248	247	eqeq2d 2632	. . . . . . . . . . . . . . 15 $\$
249	248	adantl 482	. . . . . . . . . . . . . 14 $/\$ $\$
250		f1of1 6136	. . . . . . . . . . . . . . . . 17
251	50, 250	syl 17	. . . . . . . . . . . . . . . 16
252	251	adantr 481	. . . . . . . . . . . . . . 15 $/\$
253	1	nncnd 11036	. . . . . . . . . . . . . . . . . . 19
254		npcan1 10455	. . . . . . . . . . . . . . . . . . 19
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . 18
256	167	nn0zd 11480	. . . . . . . . . . . . . . . . . . . 20
257		uzid 11702	. . . . . . . . . . . . . . . . . . . 20
258	256, 257	syl 17	. . . . . . . . . . . . . . . . . . 19
259		peano2uz 11741	. . . . . . . . . . . . . . . . . . 19
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . 18
261	255, 260	eqeltrrd 2702	. . . . . . . . . . . . . . . . 17
262		fzss2 12381	. . . . . . . . . . . . . . . . 17
263	261, 262	syl 17	. . . . . . . . . . . . . . . 16
264	263	sselda 3603	. . . . . . . . . . . . . . 15 $/\$
265		fzp1elp1 12394	. . . . . . . . . . . . . . . . 17
266	265	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
267	255	oveq2d 6666	. . . . . . . . . . . . . . . . 17
268	267	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
269	266, 268	eleqtrd 2703	. . . . . . . . . . . . . . 15 $/\$
270		f1veqaeq 6514	. . . . . . . . . . . . . . 15 $/\$ $/\$
271	252, 264, 269, 270	syl12anc 1324	. . . . . . . . . . . . . 14 $/\$
272	249, 271	sylbid 230	. . . . . . . . . . . . 13 $/\$ $\$
273	215, 272	syl5 34	. . . . . . . . . . . 12 $/\$ $\$
274	273	necon3d 2815	. . . . . . . . . . 11 $/\$ $\$
275	214, 274	mpd 15	. . . . . . . . . 10 $/\$ $\$
276	179	fveq2d 6195	. . . . . . . . . . 11
277	276	neeq1d 2853	. . . . . . . . . 10 $\$ $\$
278	275, 277	syl5ibrcom 237	. . . . . . . . 9 $/\$ $\$
279	278	necon2d 2817	. . . . . . . 8 $/\$ $\$
280	209, 279	syl5 34	. . . . . . 7 $/\$ $/\$ $\$ $/\$
281	280	adantr 481	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
282	208, 281	impbid 202	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$
283		eqop 7208	. . . . . . . 8 ..^ $\$ $\$ $/\$
284		eqop 7208	. . . . . . . . . 10 ..^ $\$ $/\$ $\$
285	77, 284	syl 17	. . . . . . . . 9 ..^ $\$ $/\$ $\$
286	285	anbi1d 741	. . . . . . . 8 ..^ $\$ $/\$ $/\$ $\$ $/\$
287	283, 286	bitrd 268	. . . . . . 7 ..^ $\$ $/\$ $\$ $/\$
288	76, 287	syl 17	. . . . . 6 $\$ $/\$ $\$ $/\$
289	288	adantl 482	. . . . 5 $/\$ $/\$ $\$ $/\$ $\$ $/\$
290	282, 289	bitr4d 271	. . . 4 $/\$ $/\$ $\$
291	290	ralrimiva 2966	. . 3 $/\$ $\$
292		reu6i 3397	. . 3 $\$ $/\$ $\$
293	9, 291, 292	syl2anc 693	. 2 $/\$
294		xp2nd 7199	. . . . . . 7 ..^
295	33, 294	syl 17	. . . . . 6
296	295	biantrurd 529	. . . . 5 $/\$
297	1	nnnn0d 11351	. . . . . . . . . . . 12
298		nn0uz 11722	. . . . . . . . . . . 12
299	297, 298	syl6eleq 2711	. . . . . . . . . . 11
300		fzpred 12389	. . . . . . . . . . 11
301	299, 300	syl 17	. . . . . . . . . 10
302	125	oveq1i 6660	. . . . . . . . . . 11
303	302	uneq2i 3764	. . . . . . . . . 10
304	301, 303	syl6eq 2672	. . . . . . . . 9
305	304	difeq1d 3727	. . . . . . . 8 $\$ $\$
306		difundir 3880	. . . . . . . . . 10 $\$ $\$ $\$
307		0lt1 10550	. . . . . . . . . . . . . 14
308		0re 10040	. . . . . . . . . . . . . . 15
309		1re 10039	. . . . . . . . . . . . . . 15
310	308, 309	ltnlei 10158	. . . . . . . . . . . . . 14
311	307, 310	mpbi 220	. . . . . . . . . . . . 13
312		elfzle1 12344	. . . . . . . . . . . . 13
313	311, 312	mto 188	. . . . . . . . . . . 12
314		incom 3805	. . . . . . . . . . . . . 14
315	314	eqeq1i 2627	. . . . . . . . . . . . 13
316		disjsn 4246	. . . . . . . . . . . . 13
317		disj3 4021	. . . . . . . . . . . . 13 $\$
318	315, 316, 317	3bitr3i 290	. . . . . . . . . . . 12 $\$
319	313, 318	mpbi 220	. . . . . . . . . . 11 $\$
320	319	uneq1i 3763	. . . . . . . . . 10 $\$ $\$ $\$
321	306, 320	eqtr4i 2647	. . . . . . . . 9 $\$ $\$
322		difundir 3880	. . . . . . . . . . . 12 $\$ $\$ $\$
323		difid 3948	. . . . . . . . . . . . 13 $\$
324	323	uneq1i 3763	. . . . . . . . . . . 12 $\$ $\$ $\$
325		uncom 3757	. . . . . . . . . . . . 13 $\$ $\$
326		un0 3967	. . . . . . . . . . . . 13 $\$ $\$
327	325, 326	eqtri 2644	. . . . . . . . . . . 12 $\$ $\$
328	322, 324, 327	3eqtri 2648	. . . . . . . . . . 11 $\$ $\$
329		nnuz 11723	. . . . . . . . . . . . . . . 16
330	1, 329	syl6eleq 2711	. . . . . . . . . . . . . . 15
331	255, 330	eqeltrd 2701	. . . . . . . . . . . . . 14
332		fzsplit2 12366	. . . . . . . . . . . . . 14 $/\$
333	331, 261, 332	syl2anc 693	. . . . . . . . . . . . 13
334	255	oveq1d 6665	. . . . . . . . . . . . . . 15
335	1	nnzd 11481	. . . . . . . . . . . . . . . 16
336		fzsn 12383	. . . . . . . . . . . . . . . 16
337	335, 336	syl 17	. . . . . . . . . . . . . . 15
338	334, 337	eqtrd 2656	. . . . . . . . . . . . . 14
339	338	uneq2d 3767	. . . . . . . . . . . . 13
340	333, 339	eqtrd 2656	. . . . . . . . . . . 12
341	340	difeq1d 3727	. . . . . . . . . . 11 $\$ $\$
342	1	nnred 11035	. . . . . . . . . . . . . . 15
343	342	ltm1d 10956	. . . . . . . . . . . . . 14
344	167	nn0red 11352	. . . . . . . . . . . . . . 15
345	344, 342	ltnled 10184	. . . . . . . . . . . . . 14
346	343, 345	mpbid 222	. . . . . . . . . . . . 13
347		elfzle2 12345	. . . . . . . . . . . . 13
348	346, 347	nsyl 135	. . . . . . . . . . . 12
349		incom 3805	. . . . . . . . . . . . . 14
350	349	eqeq1i 2627	. . . . . . . . . . . . 13
351		disjsn 4246	. . . . . . . . . . . . 13
352		disj3 4021	. . . . . . . . . . . . 13 $\$
353	350, 351, 352	3bitr3i 290	. . . . . . . . . . . 12 $\$
354	348, 353	sylib 208	. . . . . . . . . . 11 $\$
355	328, 341, 354	3eqtr4a 2682	. . . . . . . . . 10 $\$
356	355	uneq2d 3767	. . . . . . . . 9 $\$
357	321, 356	syl5eq 2668	. . . . . . . 8 $\$
358	305, 357	eqtrd 2656	. . . . . . 7 $\$
359	358	eleq2d 2687	. . . . . 6 $\$
360		eldif 3584	. . . . . 6 $\$ $/\$
361		elun 3753	. . . . . . 7 $\/$
362	219	elsn 4192	. . . . . . . 8
363	219	elsn 4192	. . . . . . . 8
364	362, 363	orbi12i 543	. . . . . . 7 $\/$ $\/$
365	361, 364	bitri 264	. . . . . 6 $\/$
366	359, 360, 365	3bitr3g 302	. . . . 5 $/\$ $\/$
367	296, 366	bitrd 268	. . . 4 $\/$
368	367	biimpa 501	. . 3 $/\$ $\/$
369	1	adantr 481	. . . . 5 $/\$
370	4	adantr 481	. . . . 5 $/\$
371	6	adantr 481	. . . . 5 $/\$
372		poimirlem22.4	. . . . . 6 $/\$
373	372	adantlr 751	. . . . 5 $/\$ $/\$
374		simpr 477	. . . . 5 $/\$
375	369, 3, 370, 371, 373, 374	poimirlem18 33427	. . . 4 $/\$
376	1	adantr 481	. . . . 5 $/\$
377	4	adantr 481	. . . . 5 $/\$
378	6	adantr 481	. . . . 5 $/\$
379		poimirlem22.3	. . . . . 6 $/\$
380	379	adantlr 751	. . . . 5 $/\$ $/\$
381		simpr 477	. . . . 5 $/\$
382	376, 3, 377, 378, 380, 381	poimirlem21 33430	. . . 4 $/\$
383	375, 382	jaodan 826	. . 3 $/\$ $\/$
384	368, 383	syldan 487	. 2 $/\$
385	293, 384	pm2.61dan 832	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

wreu 2914

wrmo 2915

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179

cop 4183 class class class wbr 4653

cmpt 4729

cid 5023

cxp 5112

crn 5115

cres 5116

cima 5117

ccom 5118

wfn 5883

wf 5884

wf1 5885

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cz 11377

cuz 11687

cfz 12326 ..^cfzo 12465

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

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 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-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 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-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-fac 13061 df-bc 13090 df-hash 13118

This theorem is referenced by: poimirlem27 33436

W3C validator