poimirlem17 - Mathbox for Brendan Leahy

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

Theorem poimirlem17 33426

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

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

**Assertion**
Ref	Expression
poimirlem17

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

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

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wal 1481

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-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-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: poimirlem18 33427

W3C validator