poimirlem16 - Mathbox for Brendan Leahy

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

Theorem poimirlem16 33425

Description: Lemma for poimir 33442 establishing the vertices of the simplex of poimirlem17 33426. (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
poimirlem16

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem16**
Step	Hyp	Ref	Expression
1		poimirlem22.2	. . 3
2		fveq2 6191	. . . . . . . . . . 11
3	2	breq2d 4665	. . . . . . . . . 10
4	3	ifbid 4108	. . . . . . . . 9
5	4	csbeq1d 3540	. . . . . . . 8
6		fveq2 6191	. . . . . . . . . . 11
7	6	fveq2d 6195	. . . . . . . . . 10
8	6	fveq2d 6195	. . . . . . . . . . . . 13
9	8	imaeq1d 5465	. . . . . . . . . . . 12
10	9	xpeq1d 5138	. . . . . . . . . . 11
11	8	imaeq1d 5465	. . . . . . . . . . . 12
12	11	xpeq1d 5138	. . . . . . . . . . 11
13	10, 12	uneq12d 3768	. . . . . . . . . 10
14	7, 13	oveq12d 6668	. . . . . . . . 9
15	14	csbeq2dv 3992	. . . . . . . 8
16	5, 15	eqtrd 2656	. . . . . . 7
17	16	mpteq2dv 4745	. . . . . 6
18	17	eqeq2d 2632	. . . . 5
19		poimirlem22.s	. . . . 5 ..^
20	18, 19	elrab2 3366	. . . 4 ..^ $/\$
21	20	simprbi 480	. . 3
22	1, 21	syl 17	. 2
23		elrabi 3359	. . . . . . . . . . . 12 ..^ ..^
24	23, 19	eleq2s 2719	. . . . . . . . . . 11 ..^
25	1, 24	syl 17	. . . . . . . . . 10 ..^
26		xp1st 7198	. . . . . . . . . 10 ..^ ..^
27	25, 26	syl 17	. . . . . . . . 9 ..^
28		xp1st 7198	. . . . . . . . 9 ..^ ..^
29	27, 28	syl 17	. . . . . . . 8 ..^
30		elmapfn 7880	. . . . . . . 8 ..^
31	29, 30	syl 17	. . . . . . 7
32	31	adantr 481	. . . . . 6 $/\$
33		1ex 10035	. . . . . . . . . 10
34		fnconstg 6093	. . . . . . . . . 10
35	33, 34	ax-mp 5	. . . . . . . . 9
36		c0ex 10034	. . . . . . . . . 10
37		fnconstg 6093	. . . . . . . . . 10
38	36, 37	ax-mp 5	. . . . . . . . 9
39	35, 38	pm3.2i 471	. . . . . . . 8 $/\$
40		xp2nd 7199	. . . . . . . . . . . . 13 ..^
41	27, 40	syl 17	. . . . . . . . . . . 12
42		fvex 6201	. . . . . . . . . . . . 13
43		f1oeq1 6127	. . . . . . . . . . . . 13
44	42, 43	elab 3350	. . . . . . . . . . . 12
45	41, 44	sylib 208	. . . . . . . . . . 11
46		dff1o3 6143	. . . . . . . . . . . 12 $/\$
47	46	simprbi 480	. . . . . . . . . . 11
48	45, 47	syl 17	. . . . . . . . . 10
49		imain 5974	. . . . . . . . . 10
50	48, 49	syl 17	. . . . . . . . 9
51		elfznn0 12433	. . . . . . . . . . . . . . 15
52		nn0p1nn 11332	. . . . . . . . . . . . . . 15
53	51, 52	syl 17	. . . . . . . . . . . . . 14
54	53	nnred 11035	. . . . . . . . . . . . 13
55	54	ltp1d 10954	. . . . . . . . . . . 12
56		fzdisj 12368	. . . . . . . . . . . 12
57	55, 56	syl 17	. . . . . . . . . . 11
58	57	imaeq2d 5466	. . . . . . . . . 10
59		ima0 5481	. . . . . . . . . 10
60	58, 59	syl6eq 2672	. . . . . . . . 9
61	50, 60	sylan9req 2677	. . . . . . . 8 $/\$
62		fnun 5997	. . . . . . . 8 $/\$ $/\$
63	39, 61, 62	sylancr 695	. . . . . . 7 $/\$
64		imaundi 5545	. . . . . . . . 9
65		nnuz 11723	. . . . . . . . . . . . . . 15
66	53, 65	syl6eleq 2711	. . . . . . . . . . . . . 14
67		peano2uz 11741	. . . . . . . . . . . . . 14
68	66, 67	syl 17	. . . . . . . . . . . . 13
69	68	adantl 482	. . . . . . . . . . . 12 $/\$
70		poimir.0	. . . . . . . . . . . . . . . 16
71	70	nncnd 11036	. . . . . . . . . . . . . . 15
72		npcan1 10455	. . . . . . . . . . . . . . 15
73	71, 72	syl 17	. . . . . . . . . . . . . 14
74	73	adantr 481	. . . . . . . . . . . . 13 $/\$
75		elfzuz3 12339	. . . . . . . . . . . . . . 15
76		eluzp1p1 11713	. . . . . . . . . . . . . . 15
77	75, 76	syl 17	. . . . . . . . . . . . . 14
78	77	adantl 482	. . . . . . . . . . . . 13 $/\$
79	74, 78	eqeltrrd 2702	. . . . . . . . . . . 12 $/\$
80		fzsplit2 12366	. . . . . . . . . . . 12 $/\$
81	69, 79, 80	syl2anc 693	. . . . . . . . . . 11 $/\$
82	81	imaeq2d 5466	. . . . . . . . . 10 $/\$
83		f1ofo 6144	. . . . . . . . . . . 12
84		foima 6120	. . . . . . . . . . . 12
85	45, 83, 84	3syl 18	. . . . . . . . . . 11
86	85	adantr 481	. . . . . . . . . 10 $/\$
87	82, 86	eqtr3d 2658	. . . . . . . . 9 $/\$
88	64, 87	syl5eqr 2670	. . . . . . . 8 $/\$
89	88	fneq2d 5982	. . . . . . 7 $/\$
90	63, 89	mpbid 222	. . . . . 6 $/\$
91		ovexd 6680	. . . . . 6 $/\$
92		inidm 3822	. . . . . 6
93		eqidd 2623	. . . . . 6 $/\$ $/\$
94		eqidd 2623	. . . . . 6 $/\$ $/\$
95	32, 90, 91, 91, 92, 93, 94	offval 6904	. . . . 5 $/\$
96		oveq1 6657	. . . . . . . . . 10
97	96	eqeq2d 2632	. . . . . . . . 9
98		oveq1 6657	. . . . . . . . . 10
99	98	eqeq2d 2632	. . . . . . . . 9
100		1p0e1 11133	. . . . . . . . . . . . . 14
101	100	eqcomi 2631	. . . . . . . . . . . . 13
102		f1ofn 6138	. . . . . . . . . . . . . . . . . 18
103	45, 102	syl 17	. . . . . . . . . . . . . . . . 17
104	103	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
105		fzss2 12381	. . . . . . . . . . . . . . . . 17
106	79, 105	syl 17	. . . . . . . . . . . . . . . 16 $/\$
107		eluzfz1 12348	. . . . . . . . . . . . . . . . . 18
108	66, 107	syl 17	. . . . . . . . . . . . . . . . 17
109	108	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
110		fnfvima 6496	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	104, 106, 109, 110	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$
112		fvun1 6269	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
113	35, 38, 112	mp3an12 1414	. . . . . . . . . . . . . . 15 $/\$
114	61, 111, 113	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
115	33	fvconst2 6469	. . . . . . . . . . . . . . 15
116	111, 115	syl 17	. . . . . . . . . . . . . 14 $/\$
117	114, 116	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
118		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
119	70	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122		1z 11407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
123	121, 122	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
124		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	124, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
126		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	123, 125, 126	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
128	118, 127	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
129	73	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
131	128, 130	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
132	131	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . 23
133		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
134		peano2z 11418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135	122, 134	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	119, 135	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
137		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138	137, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
139		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
140	136, 138, 139	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
141	133, 140	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
142		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	142, 142	pncan3oi 10297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	143	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145	141, 144	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
146	137	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147		elfznn 12370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148	147	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149		subadd2 10285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
150	142, 149	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
151	150	bicomd 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
152		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
154	151, 152, 153	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
155	146, 148, 154	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
156	155	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . . . . 26
157	156	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
158		reu6i 3397	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
159	145, 157, 158	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . 23
161		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
162	161	f1ompt 6382	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
163	132, 160, 162	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . 22
164		f1osng 6177	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
165	70, 33, 164	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22
166	70	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . . . 26
167	166	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	121	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26
169	168, 166	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . 25
170	167, 169	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24
171		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . 23
173		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . 23
174	172, 173	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22
175		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
176	175	ltp1i 10927	. . . . . . . . . . . . . . . . . . . . . . . . . 26
177	175, 175	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
178	175, 177	ltnlei 10158	. . . . . . . . . . . . . . . . . . . . . . . . . 26
179	176, 178	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25
180		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	179, 180	mto 188	. . . . . . . . . . . . . . . . . . . . . . . 24
182		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . . 24
183	181, 182	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . 23
184		f1oun 6156	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185	183, 184	mpanr2 720	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
186	163, 165, 174, 185	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . 21
187		ssv 3625	. . . . . . . . . . . . . . . . . . . . . . . . 25
188	187, 70	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24
189	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
190	70, 65	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
191	73, 190	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26
192		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
193		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194	121, 192, 193	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
195	73, 194	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . 26
196		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
197	191, 195, 196	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25
198	73	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
199		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	119, 199	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	198, 200	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	201	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . . 25
203	197, 202	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . 24
204		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . 25
205	204	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
206	188, 189, 203, 205	fmptapd 6437	. . . . . . . . . . . . . . . . . . . . . . 23
207		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
208	207	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
209	172, 208	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
210	209	necon2ad 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
211	210	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
212		ifnefalse 4098	. . . . . . . . . . . . . . . . . . . . . . . . . 26
213	211, 212	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
214	213	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . 24
215	214	uneq1d 3766	. . . . . . . . . . . . . . . . . . . . . . 23
216	206, 215	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22
217	197, 202	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
218		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25
219		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . 25
220	122, 218, 219	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . 24
221		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
222	220, 190, 221	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . 23
223		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . . 26
224	122, 223	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
225	224	uneq1i 3763	. . . . . . . . . . . . . . . . . . . . . . . 24
226	225	equncomi 3759	. . . . . . . . . . . . . . . . . . . . . . 23
227	222, 226	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22
228	216, 217, 227	f1oeq123d 6133	. . . . . . . . . . . . . . . . . . . . 21
229	186, 228	mpbird 247	. . . . . . . . . . . . . . . . . . . 20
230		f1oco 6159	. . . . . . . . . . . . . . . . . . . 20 $/\$
231	45, 229, 230	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
232		dff1o3 6143	. . . . . . . . . . . . . . . . . . . 20 $/\$
233	232	simprbi 480	. . . . . . . . . . . . . . . . . . 19
234	231, 233	syl 17	. . . . . . . . . . . . . . . . . 18
235		imain 5974	. . . . . . . . . . . . . . . . . 18
236	234, 235	syl 17	. . . . . . . . . . . . . . . . 17
237	51	nn0red 11352	. . . . . . . . . . . . . . . . . . . . 21
238	237	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20
239		fzdisj 12368	. . . . . . . . . . . . . . . . . . . 20
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . . 19
241	240	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
242		ima0 5481	. . . . . . . . . . . . . . . . . 18
243	241, 242	syl6eq 2672	. . . . . . . . . . . . . . . . 17
244	236, 243	sylan9req 2677	. . . . . . . . . . . . . . . 16 $/\$
245		imassrn 5477	. . . . . . . . . . . . . . . . . . . 20
246		f1of 6137	. . . . . . . . . . . . . . . . . . . . 21
247		frn 6053	. . . . . . . . . . . . . . . . . . . . 21
248	229, 246, 247	3syl 18	. . . . . . . . . . . . . . . . . . . 20
249	245, 248	syl5ss 3614	. . . . . . . . . . . . . . . . . . 19
250	249	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
251		elfz1end 12371	. . . . . . . . . . . . . . . . . . . . . 22
252	70, 251	sylib 208	. . . . . . . . . . . . . . . . . . . . 21
253		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
254	204, 253, 33	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21
255	252, 254	syl 17	. . . . . . . . . . . . . . . . . . . 20
256	255	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
257		f1ofn 6138	. . . . . . . . . . . . . . . . . . . . . 22
258	229, 257	syl 17	. . . . . . . . . . . . . . . . . . . . 21
259	258	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
260		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . 22
261	66, 260	syl 17	. . . . . . . . . . . . . . . . . . . . 21
262	261	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
263		eluzfz2 12349	. . . . . . . . . . . . . . . . . . . . 21
264	79, 263	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
265		fnfvima 6496	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
266	259, 262, 264, 265	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 $/\$
267	256, 266	eqeltrrd 2702	. . . . . . . . . . . . . . . . . 18 $/\$
268		fnfvima 6496	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
269	104, 250, 267, 268	syl3anc 1326	. . . . . . . . . . . . . . . . 17 $/\$
270		imaco 5640	. . . . . . . . . . . . . . . . 17
271	269, 270	syl6eleqr 2712	. . . . . . . . . . . . . . . 16 $/\$
272		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
273	33, 272	ax-mp 5	. . . . . . . . . . . . . . . . 17
274		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
275	36, 274	ax-mp 5	. . . . . . . . . . . . . . . . 17
276		fvun2 6270	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
277	273, 275, 276	mp3an12 1414	. . . . . . . . . . . . . . . 16 $/\$
278	244, 271, 277	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
279	36	fvconst2 6469	. . . . . . . . . . . . . . . 16
280	271, 279	syl 17	. . . . . . . . . . . . . . 15 $/\$
281	278, 280	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$
282	281	oveq2d 6666	. . . . . . . . . . . . 13 $/\$
283	101, 117, 282	3eqtr4a 2682	. . . . . . . . . . . 12 $/\$
284		fveq2 6191	. . . . . . . . . . . . 13
285		fveq2 6191	. . . . . . . . . . . . . 14
286	285	oveq2d 6666	. . . . . . . . . . . . 13
287	284, 286	eqeq12d 2637	. . . . . . . . . . . 12
288	283, 287	syl5ibrcom 237	. . . . . . . . . . 11 $/\$
289	288	imp 445	. . . . . . . . . 10 $/\$ $/\$
290	289	adantlr 751	. . . . . . . . 9 $/\$ $/\$ $/\$
291		eldifsn 4317	. . . . . . . . . . . . . 14 $\$ $/\$
292		df-ne 2795	. . . . . . . . . . . . . . 15
293	292	anbi2i 730	. . . . . . . . . . . . . 14 $/\$ $/\$
294	291, 293	bitri 264	. . . . . . . . . . . . 13 $\$ $/\$
295		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
296	33, 295	ax-mp 5	. . . . . . . . . . . . . . . . 17
297	296, 38	pm3.2i 471	. . . . . . . . . . . . . . . 16 $/\$
298		imain 5974	. . . . . . . . . . . . . . . . . 18
299	48, 298	syl 17	. . . . . . . . . . . . . . . . 17
300		fzdisj 12368	. . . . . . . . . . . . . . . . . . . 20
301	55, 300	syl 17	. . . . . . . . . . . . . . . . . . 19
302	301	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
303	302, 59	syl6eq 2672	. . . . . . . . . . . . . . . . 17
304	299, 303	sylan9req 2677	. . . . . . . . . . . . . . . 16 $/\$
305		fnun 5997	. . . . . . . . . . . . . . . 16 $/\$ $/\$
306	297, 304, 305	sylancr 695	. . . . . . . . . . . . . . 15 $/\$
307		imaundi 5545	. . . . . . . . . . . . . . . . 17
308		fzpred 12389	. . . . . . . . . . . . . . . . . . . . . . . . 25
309	190, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
310		uncom 3757	. . . . . . . . . . . . . . . . . . . . . . . 24
311	309, 310	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
312	311	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
313		difun2 4048	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
314		disj3 4021	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
315	183, 314	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
316	313, 315	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . 22 $\$
317	312, 316	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 $\$
318	317	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
319		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . . . 23
320	66, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
321	320	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
322		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . 21 $/\$
323	321, 79, 322	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$
324	318, 323	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
325	324	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
326		imadif 5973	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
327	48, 326	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
328		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . . . 24
329	190, 328	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
330		fnsnfv 6258	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
331	103, 329, 330	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
332	331	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
333	85, 332	difeq12d 3729	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
334	327, 333	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
335	334	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
336	325, 335	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 $/\$ $\$
337	307, 336	syl5eqr 2670	. . . . . . . . . . . . . . . 16 $/\$ $\$
338	337	fneq2d 5982	. . . . . . . . . . . . . . 15 $/\$ $\$
339	306, 338	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $\$
340		incom 3805	. . . . . . . . . . . . . . . 16 $\$ $\$
341		disjdif 4040	. . . . . . . . . . . . . . . 16 $\$
342	340, 341	eqtri 2644	. . . . . . . . . . . . . . 15 $\$
343		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
344	33, 343	ax-mp 5	. . . . . . . . . . . . . . . . 17
345		fvun1 6269	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $/\$ $\$
346	344, 345	mp3an2 1412	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
347		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
348	36, 347	ax-mp 5	. . . . . . . . . . . . . . . . 17
349		fvun1 6269	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $/\$ $\$
350	348, 349	mp3an2 1412	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
351	346, 350	eqtr4d 2659	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
352	342, 351	mpanr1 719	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
353	339, 352	sylan 488	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
354	294, 353	sylan2br 493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
355	354	anassrs 680	. . . . . . . . . . 11 $/\$ $/\$ $/\$
356		fzpred 12389	. . . . . . . . . . . . . . . . . . . . 21
357	66, 356	syl 17	. . . . . . . . . . . . . . . . . . . 20
358	357	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
359	358	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
360	331	uneq1d 3766	. . . . . . . . . . . . . . . . . . . 20
361		uncom 3757	. . . . . . . . . . . . . . . . . . . 20
362		imaundi 5545	. . . . . . . . . . . . . . . . . . . 20
363	360, 361, 362	3eqtr4g 2681	. . . . . . . . . . . . . . . . . . 19
364	363	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
365	359, 364	eqtr4d 2659	. . . . . . . . . . . . . . . . 17 $/\$
366	365	xpeq1d 5138	. . . . . . . . . . . . . . . 16 $/\$
367		xpundir 5172	. . . . . . . . . . . . . . . 16
368	366, 367	syl6eq 2672	. . . . . . . . . . . . . . 15 $/\$
369	368	uneq1d 3766	. . . . . . . . . . . . . 14 $/\$
370		un23 3772	. . . . . . . . . . . . . 14
371	369, 370	syl6eq 2672	. . . . . . . . . . . . 13 $/\$
372	371	fveq1d 6193	. . . . . . . . . . . 12 $/\$
373	372	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
374		imaco 5640	. . . . . . . . . . . . . . . . 17
375		df-ima 5127	. . . . . . . . . . . . . . . . . . . 20
376		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
377	75, 376	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
378	377	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
379	74, 378	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
380		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . 24
381	379, 380	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
382	381	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
383	172	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
384		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
385	75, 384	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
386	385	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
387	386	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
388	383, 387	mtod 189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
389		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
390	389	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
391	388, 390	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
392	391	necon2ad 2809	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
393	392	imp 445	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
394	393, 212	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
395	394	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
396	382, 395	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
397	396	rneqd 5353	. . . . . . . . . . . . . . . . . . . 20 $/\$
398	375, 397	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $/\$
399		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22
400		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
401	400	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . 22
402	399, 401	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
403		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
404	403	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
405		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
406	122	jctl 564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
408	407, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
409		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
410	406, 408, 409	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
411	405, 410	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
413	411, 412	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
414	413	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . . 23
415		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
416	415	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
417		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
418	416, 417	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
419	418	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
420	419	ibir 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
421	420	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
422		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
423	415, 422	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
424	423, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
425		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
426	406, 424, 425	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
427	421, 426	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
428	416	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	417	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . 26
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
431		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
432	431	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . 26
433	432	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
434	427, 430, 433	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
435	434	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23
436	414, 435	impbid 202	. . . . . . . . . . . . . . . . . . . . . 22
437	404, 436	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
438	402, 437	syl5bb 272	. . . . . . . . . . . . . . . . . . . 20 $/\$
439	438	eqrdv 2620	. . . . . . . . . . . . . . . . . . 19 $/\$
440	398, 439	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$
441	440	imaeq2d 5466	. . . . . . . . . . . . . . . . 17 $/\$
442	374, 441	syl5eq 2668	. . . . . . . . . . . . . . . 16 $/\$
443	442	xpeq1d 5138	. . . . . . . . . . . . . . 15 $/\$
444		imaundi 5545	. . . . . . . . . . . . . . . . . . 19
445		imaco 5640	. . . . . . . . . . . . . . . . . . . 20
446		imaco 5640	. . . . . . . . . . . . . . . . . . . 20
447	445, 446	uneq12i 3765	. . . . . . . . . . . . . . . . . . 19
448	444, 447	eqtri 2644	. . . . . . . . . . . . . . . . . 18
449	195	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
450		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
451	78, 449, 450	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$
452	201	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . 22
453	452	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
454	451, 453	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$
455		uncom 3757	. . . . . . . . . . . . . . . . . . . 20
456	454, 455	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 $/\$
457	456	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 $/\$
458	255	sneqd 4189	. . . . . . . . . . . . . . . . . . . . . . 23
459		fnsnfv 6258	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
460	258, 252, 459	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
461	458, 460	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22
462	461	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
463	331, 462	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
464	463	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
465		df-ima 5127	. . . . . . . . . . . . . . . . . . . . . 22
466		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
467	66, 466	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
468		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
469	195, 468	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
470	467, 469	sylan9ssr 3617	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
471	470	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
472		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
473	170, 472	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
474		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
475	474	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
476	473, 475	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
477	476	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
478	477	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
479	478	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
480	479	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . 25
481	480	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
482	471, 481	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
483	482	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
484	465, 483	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . 21 $/\$
485		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
486	485	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
487	486, 417	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
488	487	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
489	488	ibir 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
490	489	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
491	53	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
492	121, 491	anim12ci 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
493	485, 422	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
494	493, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
495		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
496	492, 494, 495	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
497	490, 496	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
498	486, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
499	498	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
500	432	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
501	497, 499, 500	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
502	501	ex 450	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
503		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
504		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
505	504, 122	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
506		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
507	492, 505, 506	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
508	503, 507	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
509		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
510	508, 509	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
511	510	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
512	502, 511	impbid 202	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
513		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25
514	513	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . . . 24
515	399, 514	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
516	512, 515	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
517	516	eqrdv 2620	. . . . . . . . . . . . . . . . . . . . 21 $/\$
518	73	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22
519	518	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
520	484, 517, 519	3eqtr2rd 2663	. . . . . . . . . . . . . . . . . . . 20 $/\$
521	520	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19 $/\$
522	464, 521	uneq12d 3768	. . . . . . . . . . . . . . . . . 18 $/\$
523	448, 457, 522	3eqtr4a 2682	. . . . . . . . . . . . . . . . 17 $/\$
524	523	xpeq1d 5138	. . . . . . . . . . . . . . . 16 $/\$
525		xpundir 5172	. . . . . . . . . . . . . . . 16
526	524, 525	syl6eq 2672	. . . . . . . . . . . . . . 15 $/\$
527	443, 526	uneq12d 3768	. . . . . . . . . . . . . 14 $/\$
528		unass 3770	. . . . . . . . . . . . . . 15
529		un23 3772	. . . . . . . . . . . . . . 15
530	528, 529	eqtr3i 2646	. . . . . . . . . . . . . 14
531	527, 530	syl6eq 2672	. . . . . . . . . . . . 13 $/\$
532	531	fveq1d 6193	. . . . . . . . . . . 12 $/\$
533	532	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
534	355, 373, 533	3eqtr4d 2666	. . . . . . . . . 10 $/\$ $/\$ $/\$
535		snssi 4339	. . . . . . . . . . . . . . 15
536	142, 535	ax-mp 5	. . . . . . . . . . . . . 14
537		0cn 10032	. . . . . . . . . . . . . . 15
538		snssi 4339	. . . . . . . . . . . . . . 15
539	537, 538	ax-mp 5	. . . . . . . . . . . . . 14
540	536, 539	unssi 3788	. . . . . . . . . . . . 13
541	33	fconst 6091	. . . . . . . . . . . . . . . . 17
542	36	fconst 6091	. . . . . . . . . . . . . . . . 17
543	541, 542	pm3.2i 471	. . . . . . . . . . . . . . . 16 $/\$
544		fun 6066	. . . . . . . . . . . . . . . 16 $/\$ $/\$
545	543, 244, 544	sylancr 695	. . . . . . . . . . . . . . 15 $/\$
546		imaundi 5545	. . . . . . . . . . . . . . . . 17
547	66	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
548		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . 20 $/\$
549	547, 379, 548	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$
550	549	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 $/\$
551		f1ofo 6144	. . . . . . . . . . . . . . . . . . . 20
552		foima 6120	. . . . . . . . . . . . . . . . . . . 20
553	231, 551, 552	3syl 18	. . . . . . . . . . . . . . . . . . 19
554	553	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
555	550, 554	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 $/\$
556	546, 555	syl5eqr 2670	. . . . . . . . . . . . . . . 16 $/\$
557	556	feq2d 6031	. . . . . . . . . . . . . . 15 $/\$
558	545, 557	mpbid 222	. . . . . . . . . . . . . 14 $/\$
559	558	ffvelrnda 6359	. . . . . . . . . . . . 13 $/\$ $/\$
560	540, 559	sseldi 3601	. . . . . . . . . . . 12 $/\$ $/\$
561	560	addid2d 10237	. . . . . . . . . . 11 $/\$ $/\$
562	561	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$
563	534, 562	eqtr4d 2659	. . . . . . . . 9 $/\$ $/\$ $/\$
564	97, 99, 290, 563	ifbothda 4123	. . . . . . . 8 $/\$ $/\$
565	564	oveq2d 6666	. . . . . . 7 $/\$ $/\$
566		elmapi 7879	. . . . . . . . . . . . 13 ..^ ..^
567	29, 566	syl 17	. . . . . . . . . . . 12 ..^
568	567	ffvelrnda 6359	. . . . . . . . . . 11 $/\$ ..^
569		elfzonn0 12512	. . . . . . . . . . 11 ..^
570	568, 569	syl 17	. . . . . . . . . 10 $/\$
571	570	nn0cnd 11353	. . . . . . . . 9 $/\$
572	571	adantlr 751	. . . . . . . 8 $/\$ $/\$
573	142, 537	keepel 4155	. . . . . . . . 9
574	573	a1i 11	. . . . . . . 8 $/\$ $/\$
575	572, 574, 560	addassd 10062	. . . . . . 7 $/\$ $/\$
576	565, 575	eqtr4d 2659	. . . . . 6 $/\$ $/\$
577	576	mpteq2dva 4744	. . . . 5 $/\$
578	95, 577	eqtrd 2656	. . . 4 $/\$
579		poimirlem18.4	. . . . . . . . . 10
580	579	adantr 481	. . . . . . . . 9 $/\$
581		elfzle1 12344	. . . . . . . . . 10
582	581	adantl 482	. . . . . . . . 9 $/\$
583	580, 582	eqbrtrd 4675	. . . . . . . 8 $/\$
584		0re 10040	. . . . . . . . . 10
585	579, 584	syl6eqel 2709	. . . . . . . . 9
586		lenlt 10116	. . . . . . . . 9 $/\$
587	585, 237, 586	syl2an 494	. . . . . . . 8 $/\$
588	583, 587	mpbid 222	. . . . . . 7 $/\$
589	588	iffalsed 4097	. . . . . 6 $/\$
590	589	csbeq1d 3540	. . . . 5 $/\$
591		ovex 6678	. . . . . 6
592		oveq2 6658	. . . . . . . . . 10
593	592	imaeq2d 5466	. . . . . . . . 9
594	593	xpeq1d 5138	. . . . . . . 8
595		oveq1 6657	. . . . . . . . . . 11
596	595	oveq1d 6665	. . . . . . . . . 10
597	596	imaeq2d 5466	. . . . . . . . 9
598	597	xpeq1d 5138	. . . . . . . 8
599	594, 598	uneq12d 3768	. . . . . . 7
600	599	oveq2d 6666	. . . . . 6
601	591, 600	csbie 3559	. . . . 5
602	590, 601	syl6eq 2672	. . . 4 $/\$
603		ovexd 6680	. . . . 5 $/\$ $/\$
604		fvexd 6203	. . . . 5 $/\$ $/\$
605		eqidd 2623	. . . . 5 $/\$
606		ffn 6045	. . . . . . 7
607	558, 606	syl 17	. . . . . 6 $/\$
608		nfcv 2764	. . . . . . . . . . 11
609		nfmpt1 4747	. . . . . . . . . . 11
610	608, 609	nfco 5287	. . . . . . . . . 10
611		nfcv 2764	. . . . . . . . . 10
612	610, 611	nfima 5474	. . . . . . . . 9
613		nfcv 2764	. . . . . . . . 9
614	612, 613	nfxp 5142	. . . . . . . 8
615		nfcv 2764	. . . . . . . . . 10
616	610, 615	nfima 5474	. . . . . . . . 9
617		nfcv 2764	. . . . . . . . 9
618	616, 617	nfxp 5142	. . . . . . . 8
619	614, 618	nfun 3769	. . . . . . 7
620	619	dffn5f 6252	. . . . . 6
621	607, 620	sylib 208	. . . . 5 $/\$
622	91, 603, 604, 605, 621	offval2 6914	. . . 4 $/\$
623	578, 602, 622	3eqtr4rd 2667	. . 3 $/\$
624	623	mpteq2dva 4744	. 2
625	22, 624	eqtr4d 2659	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

wreu 2914

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

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

cres 5116

cima 5117

ccom 5118

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

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: poimirlem17 33426

W3C validator