poimirlem20 - Mathbox for Brendan Leahy

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

Theorem poimirlem20 33429

Description: Lemma for poimir 33442 establishing existence for poimirlem21 33430. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

**Assertion**
Ref	Expression
poimirlem20

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem20**
Step	Hyp	Ref	Expression
1		oveq2 6658	. . . . . . . . 9
2	1	eleq1d 2686	. . . . . . . 8 ..^ ..^
3		oveq2 6658	. . . . . . . . 9
4	3	eleq1d 2686	. . . . . . . 8 ..^ ..^
5		fveq2 6191	. . . . . . . . . . . 12
6	5	oveq1d 6665	. . . . . . . . . . 11
7	6	adantl 482	. . . . . . . . . 10 $/\$
8		poimirlem22.2	. . . . . . . . . . . . . . . . . . . 20
9		elrabi 3359	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
10		poimirlem22.s	. . . . . . . . . . . . . . . . . . . . 21 ..^
11	9, 10	eleq2s 2719	. . . . . . . . . . . . . . . . . . . 20 ..^
12	8, 11	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
13		xp1st 7198	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
14	12, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
15		xp1st 7198	. . . . . . . . . . . . . . . . . 18 ..^ ..^
16	14, 15	syl 17	. . . . . . . . . . . . . . . . 17 ..^
17		elmapi 7879	. . . . . . . . . . . . . . . . 17 ..^ ..^
18	16, 17	syl 17	. . . . . . . . . . . . . . . 16 ..^
19		xp2nd 7199	. . . . . . . . . . . . . . . . . . . 20 ..^
20	14, 19	syl 17	. . . . . . . . . . . . . . . . . . 19
21		fvex 6201	. . . . . . . . . . . . . . . . . . . 20
22		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . 20
23	21, 22	elab 3350	. . . . . . . . . . . . . . . . . . 19
24	20, 23	sylib 208	. . . . . . . . . . . . . . . . . 18
25		f1of 6137	. . . . . . . . . . . . . . . . . 18
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17
27		poimir.0	. . . . . . . . . . . . . . . . . 18
28		elfz1end 12371	. . . . . . . . . . . . . . . . . 18
29	27, 28	sylib 208	. . . . . . . . . . . . . . . . 17
30	26, 29	ffvelrnd 6360	. . . . . . . . . . . . . . . 16
31	18, 30	ffvelrnd 6360	. . . . . . . . . . . . . . 15 ..^
32		elfzonn0 12512	. . . . . . . . . . . . . . 15 ..^
33	31, 32	syl 17	. . . . . . . . . . . . . 14
34		fvex 6201	. . . . . . . . . . . . . . . . 17
35		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
36	35	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
37		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
38	37	neeq1d 2853	. . . . . . . . . . . . . . . . . . 19
39	38	rexbidv 3052	. . . . . . . . . . . . . . . . . 18
40	36, 39	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
41		poimirlem22.3	. . . . . . . . . . . . . . . . 17 $/\$
42	34, 40, 41	vtocl 3259	. . . . . . . . . . . . . . . 16 $/\$
43	30, 42	mpdan 702	. . . . . . . . . . . . . . 15
44		fveq1 6190	. . . . . . . . . . . . . . . . . . . . 21
45		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
46	18, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	46	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
48		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
49		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
50	48, 49	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
51		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
53	51, 52	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54	50, 53	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
55		dff1o3 6143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
56	55	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	24, 56	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
60		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
61	60	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
62	61	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
63		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65	64	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
66		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	65, 66	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	59, 67	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
69		fnun 5997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
70	54, 68, 69	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
71		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
72		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
73		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
74	72, 73	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
75	60, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
76	75	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
77	27	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	79	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
82		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
84	83	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
85	80, 84	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
86		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
87	76, 85, 86	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
88	87	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
89		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90		foima 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
91	24, 89, 90	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
92	91	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
93	88, 92	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
94	71, 93	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
95	94	fneq2d 5982	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
96	70, 95	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
97		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . 25
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
99		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . . 24
100		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
101		f1ofn 6138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102	24, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103	102	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
104		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
105	75, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
106	105	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
107		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
108		uzss 11708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
109	81, 107, 108	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
110	109	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
111	27	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
112		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
113	111, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114	79	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
115	113, 114	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
116	115	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
117	110, 116	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
118		eluzfz2 12349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
119	117, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
120		fnfvima 6496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
121	103, 106, 119, 120	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
122		fvun2 6270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
123	50, 53, 122	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
124	68, 121, 123	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
125	51	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126	121, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
127	124, 126	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
128	127	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
129	47, 96, 98, 98, 99, 100, 128	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
130	30, 129	mpidan 704	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
131	33	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	130, 133	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	44, 134	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136	135	adantllr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
138	137	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
139	138	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
140	139	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
142	141	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
144	143	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
145	144	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
146	143	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
147	146	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
148	145, 147	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
149	142, 148	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
150	149	csbeq2dv 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
151	140, 150	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
152	151	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
153	152	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153, 10	elrab2 3366	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
155	154	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . 25
156	8, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
157	61	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
158		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159	111, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
161	160	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
162	27	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
163	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
164		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
165	164	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
166	162	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
167	166	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
168	157, 161, 163, 165, 167	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
169		poimirlem21.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
170	169	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
171	168, 170	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
172	171	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
173	172	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
174		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
175		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
176	175	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
177	176	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
178		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
179	178	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
180	179	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
181	180	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
182	177, 181	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
183	182	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
184	174, 183	csbie 3559	. . . . . . . . . . . . . . . . . . . . . . . . . 26
185	173, 184	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
186	185	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . 24
187	156, 186	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23
188	187	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . 22
189	188	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . 21
190		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
191		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
192	190, 191	elrnmpti 5376	. . . . . . . . . . . . . . . . . . . . 21
193	189, 192	syl6bb 276	. . . . . . . . . . . . . . . . . . . 20
194	193	biimpa 501	. . . . . . . . . . . . . . . . . . 19 $/\$
195	136, 194	r19.29a 3078	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	neeq1d 2853	. . . . . . . . . . . . . . . . 17 $/\$
197	196	biimpd 219	. . . . . . . . . . . . . . . 16 $/\$
198	197	rexlimdva 3031	. . . . . . . . . . . . . . 15
199	43, 198	mpd 15	. . . . . . . . . . . . . 14
200		elnnne0 11306	. . . . . . . . . . . . . 14 $/\$
201	33, 199, 200	sylanbrc 698	. . . . . . . . . . . . 13
202		nnm1nn0 11334	. . . . . . . . . . . . 13
203	201, 202	syl 17	. . . . . . . . . . . 12
204		elfzo0 12508	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$
205	31, 204	sylib 208	. . . . . . . . . . . . 13 $/\$ $/\$
206	205	simp2d 1074	. . . . . . . . . . . 12
207	203	nn0red 11352	. . . . . . . . . . . . 13
208	33	nn0red 11352	. . . . . . . . . . . . 13
209	206	nnred 11035	. . . . . . . . . . . . 13
210	208	ltm1d 10956	. . . . . . . . . . . . 13
211		elfzolt2 12479	. . . . . . . . . . . . . 14 ..^
212	31, 211	syl 17	. . . . . . . . . . . . 13
213	207, 208, 209, 210, 212	lttrd 10198	. . . . . . . . . . . 12
214		elfzo0 12508	. . . . . . . . . . . 12 ..^ $/\$ $/\$
215	203, 206, 213, 214	syl3anbrc 1246	. . . . . . . . . . 11 ..^
216	215	adantr 481	. . . . . . . . . 10 $/\$ ..^
217	7, 216	eqeltrd 2701	. . . . . . . . 9 $/\$ ..^
218	217	adantlr 751	. . . . . . . 8 $/\$ $/\$ ..^
219	18	ffvelrnda 6359	. . . . . . . . . . . . 13 $/\$ ..^
220		elfzonn0 12512	. . . . . . . . . . . . 13 ..^
221	219, 220	syl 17	. . . . . . . . . . . 12 $/\$
222	221	nn0cnd 11353	. . . . . . . . . . 11 $/\$
223	222	subid1d 10381	. . . . . . . . . 10 $/\$
224	223, 219	eqeltrd 2701	. . . . . . . . 9 $/\$ ..^
225	224	adantr 481	. . . . . . . 8 $/\$ $/\$ ..^
226	2, 4, 218, 225	ifbothda 4123	. . . . . . 7 $/\$ ..^
227		eqid 2622	. . . . . . 7
228	226, 227	fmptd 6385	. . . . . 6 ..^
229		ovex 6678	. . . . . . 7 ..^
230	229, 97	elmap 7886	. . . . . 6 ..^ ..^
231	228, 230	sylibr 224	. . . . 5 ..^
232		simpr 477	. . . . . . . . . . . . 13 $/\$
233		1z 11407	. . . . . . . . . . . . . . . 16
234		peano2z 11418	. . . . . . . . . . . . . . . 16
235	233, 234	ax-mp 5	. . . . . . . . . . . . . . 15
236	111, 235	jctil 560	. . . . . . . . . . . . . 14 $/\$
237		elfzelz 12342	. . . . . . . . . . . . . . 15
238	237, 233	jctir 561	. . . . . . . . . . . . . 14 $/\$
239		fzsubel 12377	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
240	236, 238, 239	syl2an 494	. . . . . . . . . . . . 13 $/\$
241	232, 240	mpbid 222	. . . . . . . . . . . 12 $/\$
242		ax-1cn 9994	. . . . . . . . . . . . . 14
243	242, 242	pncan3oi 10297	. . . . . . . . . . . . 13
244	243	oveq1i 6660	. . . . . . . . . . . 12
245	241, 244	syl6eleq 2711	. . . . . . . . . . 11 $/\$
246	245	ralrimiva 2966	. . . . . . . . . 10
247		simpr 477	. . . . . . . . . . . . . 14 $/\$
248	159, 233	jctil 560	. . . . . . . . . . . . . . 15 $/\$
249		elfzelz 12342	. . . . . . . . . . . . . . . 16
250	249, 233	jctir 561	. . . . . . . . . . . . . . 15 $/\$
251		fzaddel 12375	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
252	248, 250, 251	syl2an 494	. . . . . . . . . . . . . 14 $/\$
253	247, 252	mpbid 222	. . . . . . . . . . . . 13 $/\$
254	79	oveq2d 6666	. . . . . . . . . . . . . 14
255	254	adantr 481	. . . . . . . . . . . . 13 $/\$
256	253, 255	eleqtrd 2703	. . . . . . . . . . . 12 $/\$
257	237	zcnd 11483	. . . . . . . . . . . . . . 15
258	249	zcnd 11483	. . . . . . . . . . . . . . 15
259		subadd2 10285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
260	242, 259	mp3an2 1412	. . . . . . . . . . . . . . . 16 $/\$
261		eqcom 2629	. . . . . . . . . . . . . . . 16
262		eqcom 2629	. . . . . . . . . . . . . . . 16
263	260, 261, 262	3bitr4g 303	. . . . . . . . . . . . . . 15 $/\$
264	257, 258, 263	syl2anr 495	. . . . . . . . . . . . . 14 $/\$
265	264	ralrimiva 2966	. . . . . . . . . . . . 13
266	265	adantl 482	. . . . . . . . . . . 12 $/\$
267		reu6i 3397	. . . . . . . . . . . 12 $/\$
268	256, 266, 267	syl2anc 693	. . . . . . . . . . 11 $/\$
269	268	ralrimiva 2966	. . . . . . . . . 10
270		eqid 2622	. . . . . . . . . . 11
271	270	f1ompt 6382	. . . . . . . . . 10 $/\$
272	246, 269, 271	sylanbrc 698	. . . . . . . . 9
273		f1osng 6177	. . . . . . . . . 10 $/\$
274	48, 27, 273	sylancr 695	. . . . . . . . 9
275	160, 162	ltnled 10184	. . . . . . . . . . . 12
276	166, 275	mpbid 222	. . . . . . . . . . 11
277		elfzle2 12345	. . . . . . . . . . 11
278	276, 277	nsyl 135	. . . . . . . . . 10
279		disjsn 4246	. . . . . . . . . 10
280	278, 279	sylibr 224	. . . . . . . . 9
281		1re 10039	. . . . . . . . . . . . . 14
282	281	ltp1i 10927	. . . . . . . . . . . . 13
283	235	zrei 11383	. . . . . . . . . . . . . 14
284	281, 283	ltnlei 10158	. . . . . . . . . . . . 13
285	282, 284	mpbi 220	. . . . . . . . . . . 12
286		elfzle1 12344	. . . . . . . . . . . 12
287	285, 286	mto 188	. . . . . . . . . . 11
288		disjsn 4246	. . . . . . . . . . 11
289	287, 288	mpbir 221	. . . . . . . . . 10
290		f1oun 6156	. . . . . . . . . 10 $/\$ $/\$ $/\$
291	289, 290	mpanr1 719	. . . . . . . . 9 $/\$ $/\$
292	272, 274, 280, 291	syl21anc 1325	. . . . . . . 8
293		eleq1 2689	. . . . . . . . . . . . . . 15
294	287, 293	mtbiri 317	. . . . . . . . . . . . . 14
295	294	necon2ai 2823	. . . . . . . . . . . . 13
296		ifnefalse 4098	. . . . . . . . . . . . 13
297	295, 296	syl 17	. . . . . . . . . . . 12
298	297	mpteq2ia 4740	. . . . . . . . . . 11
299	298	uneq1i 3763	. . . . . . . . . 10
300	48	a1i 11	. . . . . . . . . . 11
301		ssv 3625	. . . . . . . . . . . 12
302	301, 27	sseldi 3601	. . . . . . . . . . 11
303	27, 73	syl6eleq 2711	. . . . . . . . . . . . 13
304		fzpred 12389	. . . . . . . . . . . . 13
305	303, 304	syl 17	. . . . . . . . . . . 12
306		uncom 3757	. . . . . . . . . . . 12
307	305, 306	syl6req 2673	. . . . . . . . . . 11
308		iftrue 4092	. . . . . . . . . . . 12
309	308	adantl 482	. . . . . . . . . . 11 $/\$
310	300, 302, 307, 309	fmptapd 6437	. . . . . . . . . 10
311	299, 310	syl5eqr 2670	. . . . . . . . 9
312	79, 303	eqeltrd 2701	. . . . . . . . . . 11
313		uzid 11702	. . . . . . . . . . . . 13
314		peano2uz 11741	. . . . . . . . . . . . 13
315	159, 313, 314	3syl 18	. . . . . . . . . . . 12
316	79, 315	eqeltrrd 2702	. . . . . . . . . . 11
317		fzsplit2 12366	. . . . . . . . . . 11 $/\$
318	312, 316, 317	syl2anc 693	. . . . . . . . . 10
319	79	oveq1d 6665	. . . . . . . . . . . 12
320		fzsn 12383	. . . . . . . . . . . . 13
321	111, 320	syl 17	. . . . . . . . . . . 12
322	319, 321	eqtrd 2656	. . . . . . . . . . 11
323	322	uneq2d 3767	. . . . . . . . . 10
324	318, 323	eqtr2d 2657	. . . . . . . . 9
325	311, 307, 324	f1oeq123d 6133	. . . . . . . 8
326	292, 325	mpbid 222	. . . . . . 7
327		f1oco 6159	. . . . . . 7 $/\$
328	24, 326, 327	syl2anc 693	. . . . . 6
329	97	mptex 6486	. . . . . . . 8
330	21, 329	coex 7118	. . . . . . 7
331		f1oeq1 6127	. . . . . . 7
332	330, 331	elab 3350	. . . . . 6
333	328, 332	sylibr 224	. . . . 5
334		opelxpi 5148	. . . . 5 ..^ $/\$ ..^
335	231, 333, 334	syl2anc 693	. . . 4 ..^
336	27	nnnn0d 11351	. . . . 5
337		0elfz 12436	. . . . 5
338	336, 337	syl 17	. . . 4
339		opelxpi 5148	. . . 4 ..^ $/\$ ..^
340	335, 338, 339	syl2anc 693	. . 3 ..^
341		poimirlem22.1	. . . . 5
342	27, 10, 341, 8, 41, 169	poimirlem19 33428	. . . 4
343		elfzle1 12344	. . . . . . . . 9
344		0re 10040	. . . . . . . . . 10
345		lenlt 10116	. . . . . . . . . 10 $/\$
346	344, 61, 345	sylancr 695	. . . . . . . . 9
347	343, 346	mpbid 222	. . . . . . . 8
348	347	iffalsed 4097	. . . . . . 7
349	348	csbeq1d 3540	. . . . . 6
350		ovex 6678	. . . . . . 7
351		oveq2 6658	. . . . . . . . . . 11
352	351	imaeq2d 5466	. . . . . . . . . 10
353	352	xpeq1d 5138	. . . . . . . . 9
354		oveq1 6657	. . . . . . . . . . . 12
355	354	oveq1d 6665	. . . . . . . . . . 11
356	355	imaeq2d 5466	. . . . . . . . . 10
357	356	xpeq1d 5138	. . . . . . . . 9
358	353, 357	uneq12d 3768	. . . . . . . 8
359	358	oveq2d 6666	. . . . . . 7
360	350, 359	csbie 3559	. . . . . 6
361	349, 360	syl6eq 2672	. . . . 5
362	361	mpteq2ia 4740	. . . 4
363	342, 362	syl6eqr 2674	. . 3
364		opex 4932	. . . . . . . . . . 11
365	364, 51	op2ndd 7179	. . . . . . . . . 10
366	365	breq2d 4665	. . . . . . . . 9
367	366	ifbid 4108	. . . . . . . 8
368	367	csbeq1d 3540	. . . . . . 7
369	364, 51	op1std 7178	. . . . . . . . . 10
370	97	mptex 6486	. . . . . . . . . . 11
371	370, 330	op1std 7178	. . . . . . . . . 10
372	369, 371	syl 17	. . . . . . . . 9
373	370, 330	op2ndd 7179	. . . . . . . . . . . . 13
374	369, 373	syl 17	. . . . . . . . . . . 12
375	374	imaeq1d 5465	. . . . . . . . . . 11
376	375	xpeq1d 5138	. . . . . . . . . 10
377	374	imaeq1d 5465	. . . . . . . . . . 11
378	377	xpeq1d 5138	. . . . . . . . . 10
379	376, 378	uneq12d 3768	. . . . . . . . 9
380	372, 379	oveq12d 6668	. . . . . . . 8
381	380	csbeq2dv 3992	. . . . . . 7
382	368, 381	eqtrd 2656	. . . . . 6
383	382	mpteq2dv 4745	. . . . 5
384	383	eqeq2d 2632	. . . 4
385	384, 10	elrab2 3366	. . 3 ..^ $/\$
386	340, 363, 385	sylanbrc 698	. 2
387	364, 51	op2ndd 7179	. . . . . 6
388	387	eqcoms 2630	. . . . 5
389	27	nnne0d 11065	. . . . . . 7
390	389	necomd 2849	. . . . . 6
391		neeq1 2856	. . . . . 6
392	390, 391	syl5ibrcom 237	. . . . 5
393	388, 392	syl5 34	. . . 4
394	393	necon2d 2817	. . 3
395	169, 394	mpd 15	. 2
396		neeq1 2856	. . 3
397	396	rspcev 3309	. 2 $/\$
398	386, 395, 397	syl2anc 693	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

wreu 2914

crab 2916

cvv 3200

csb 3533

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cop 4183 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

crn 5115

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

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-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-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-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-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466

This theorem is referenced by: poimirlem21 33430

W3C validator