poimirlem32 - Mathbox for Brendan Leahy

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

Theorem poimirlem32 33441

Description: Lemma for poimir 33442, combining poimirlem28 33437, poimirlem30 33439, and poimirlem31 33440 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimir.i
poimir.r
poimir.1	↾_t
poimir.2	$/\$ $/\$ $/\$
poimir.3	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
poimirlem32	↾_t

Distinct variable groups:

Proof of Theorem poimirlem32 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . . 7
2	1	adantr 481	. . . . . 6 $/\$
3		oveq1 6657	. . . . . . . . . . . . . 14
4	3	fveq2d 6195	. . . . . . . . . . . . 13
5	4	fveq1d 6193	. . . . . . . . . . . 12
6	5	breq2d 4665	. . . . . . . . . . 11
7		fveq1 6190	. . . . . . . . . . . 12
8	7	neeq1d 2853	. . . . . . . . . . 11
9	6, 8	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
10	9	ralbidv 2986	. . . . . . . . 9 $/\$ $/\$
11	10	rabbidv 3189	. . . . . . . 8 $/\$ $/\$
12	11	uneq2d 3767	. . . . . . 7 $/\$ $/\$
13	12	supeq1d 8352	. . . . . 6 $/\$ $/\$
14	1	nnnn0d 11351	. . . . . . . . . . 11
15		0elfz 12436	. . . . . . . . . . 11
16	14, 15	syl 17	. . . . . . . . . 10
17	16	snssd 4340	. . . . . . . . 9
18		ssrab2 3687	. . . . . . . . . . 11 $/\$
19		1eluzge0 11732	. . . . . . . . . . . 12
20		fzss1 12380	. . . . . . . . . . . 12
21	19, 20	ax-mp 5	. . . . . . . . . . 11
22	18, 21	sstri 3612	. . . . . . . . . 10 $/\$
23	22	a1i 11	. . . . . . . . 9 $/\$
24	17, 23	unssd 3789	. . . . . . . 8 $/\$
25		ltso 10118	. . . . . . . . 9
26		snfi 8038	. . . . . . . . . . 11
27		fzfi 12771	. . . . . . . . . . . 12
28		rabfi 8185	. . . . . . . . . . . 12 $/\$
29	27, 28	ax-mp 5	. . . . . . . . . . 11 $/\$
30		unfi 8227	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	26, 29, 30	mp2an 708	. . . . . . . . . 10 $/\$
32		c0ex 10034	. . . . . . . . . . . 12
33	32	snid 4208	. . . . . . . . . . 11
34		elun1 3780	. . . . . . . . . . 11 $/\$
35		ne0i 3921	. . . . . . . . . . 11 $/\$ $/\$
36	33, 34, 35	mp2b 10	. . . . . . . . . 10 $/\$
37		0red 10041	. . . . . . . . . . . . 13
38	37	snssd 4340	. . . . . . . . . . . 12
39	1, 38	ax-mp 5	. . . . . . . . . . 11
40		elfzelz 12342	. . . . . . . . . . . . . 14
41	40	ssriv 3607	. . . . . . . . . . . . 13
42		zssre 11384	. . . . . . . . . . . . 13
43	41, 42	sstri 3612	. . . . . . . . . . . 12
44	18, 43	sstri 3612	. . . . . . . . . . 11 $/\$
45	39, 44	unssi 3788	. . . . . . . . . 10 $/\$
46	31, 36, 45	3pm3.2i 1239	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
47		fisupcl 8375	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	25, 46, 47	mp2an 708	. . . . . . . 8 $/\$ $/\$
49		ssel 3597	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
50	24, 48, 49	mpisyl 21	. . . . . . 7 $/\$
51	50	ad2antrr 762	. . . . . 6 $/\$ $/\$ $/\$
52		elfznn 12370	. . . . . . . . 9
53		nngt0 11049	. . . . . . . . . . . 12
54	53	adantr 481	. . . . . . . . . . 11 $/\$
55		simpr 477	. . . . . . . . . . . . . 14 $/\$
56	55	ralimi 2952	. . . . . . . . . . . . 13 $/\$
57		elfznn 12370	. . . . . . . . . . . . . 14
58		nnre 11027	. . . . . . . . . . . . . . . . . . . 20
59		nnre 11027	. . . . . . . . . . . . . . . . . . . 20
60		lenlt 10116	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	58, 59, 60	syl2an 494	. . . . . . . . . . . . . . . . . . 19 $/\$
62		elfz1b 12409	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	biimpri 218	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
64	63	3expia 1267	. . . . . . . . . . . . . . . . . . 19 $/\$
65	61, 64	sylbird 250	. . . . . . . . . . . . . . . . . 18 $/\$
66		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
67	66	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . 20
68	67	rspcev 3309	. . . . . . . . . . . . . . . . . . 19 $/\$
69	68	expcom 451	. . . . . . . . . . . . . . . . . 18
70	65, 69	sylan9 689	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71	70	an32s 846	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72		nne 2798	. . . . . . . . . . . . . . . . . 18
73	72	rexbii 3041	. . . . . . . . . . . . . . . . 17
74		rexnal 2995	. . . . . . . . . . . . . . . . 17
75	73, 74	bitr3i 266	. . . . . . . . . . . . . . . 16
76	71, 75	syl6ib 241	. . . . . . . . . . . . . . 15 $/\$ $/\$
77	76	con4d 114	. . . . . . . . . . . . . 14 $/\$ $/\$
78	57, 77	sylan2 491	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	syl5 34	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	79	ralrimiva 2966	. . . . . . . . . . 11 $/\$ $/\$
81		ralunb 3794	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
82		breq1 4656	. . . . . . . . . . . . . 14
83	32, 82	ralsn 4222	. . . . . . . . . . . . 13
84		oveq2 6658	. . . . . . . . . . . . . . 15
85	84	raleqdv 3144	. . . . . . . . . . . . . 14 $/\$ $/\$
86	85	ralrab 3368	. . . . . . . . . . . . 13 $/\$ $/\$
87	83, 86	anbi12i 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	81, 87	bitri 264	. . . . . . . . . . 11 $/\$ $/\$ $/\$
89	54, 80, 88	sylanbrc 698	. . . . . . . . . 10 $/\$ $/\$
90		breq1 4656	. . . . . . . . . . 11 $/\$ $/\$
91	90	rspcva 3307	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
92	48, 89, 91	sylancr 695	. . . . . . . . 9 $/\$ $/\$
93	52, 92	sylan 488	. . . . . . . 8 $/\$ $/\$
94	93	3adant2 1080	. . . . . . 7 $/\$ $/\$ $/\$
95	94	adantl 482	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
96	40	zred 11482	. . . . . . . . . . 11
97	96	3ad2ant1 1082	. . . . . . . . . 10 $/\$ $/\$
98	97	adantl 482	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
99		simpr1 1067	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100		simpll 790	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101		simplr 792	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	zred 11482	. . . . . . . . . . . . . . . . . . . . . 22
104		nndivre 11056	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
105	103, 104	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . 23
107	103, 106	jca 554	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108		nnrp 11842	. . . . . . . . . . . . . . . . . . . . . . 23
109	108	rpregt0d 11878	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
110		divge0 10892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111	107, 109, 110	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
114	103	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
115		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
116	108	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
117	114, 115, 116	ledivmuld 11925	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
118		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	118	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . 25
120	119	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
122	117, 121	bitrd 268	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	113, 122	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124		0re 10040	. . . . . . . . . . . . . . . . . . . . . 22
125		1re 10039	. . . . . . . . . . . . . . . . . . . . . 22
126	124, 125	elicc2i 12239	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	105, 111, 123, 126	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . 20 $/\$
128	127	ancoms 469	. . . . . . . . . . . . . . . . . . 19 $/\$
129		elsni 4194	. . . . . . . . . . . . . . . . . . . . 21
130	129	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
131	130	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
132	128, 131	syl5ibrcom 237	. . . . . . . . . . . . . . . . . 18 $/\$
133	132	impr 649	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
134	101, 133	sylan 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
135		simprr 796	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136		vex 3203	. . . . . . . . . . . . . . . . . 18
137	136	fconst 6091	. . . . . . . . . . . . . . . . 17
138	137	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
140		inidm 3822	. . . . . . . . . . . . . . . 16
141	134, 135, 138, 139, 139, 140	off 6912	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142		poimir.i	. . . . . . . . . . . . . . . . 17
143	142	eleq2i 2693	. . . . . . . . . . . . . . . 16
144		ovex 6678	. . . . . . . . . . . . . . . . 17
145		ovex 6678	. . . . . . . . . . . . . . . . 17
146	144, 145	elmap 7886	. . . . . . . . . . . . . . . 16
147	143, 146	bitri 264	. . . . . . . . . . . . . . 15
148	141, 147	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	148	3adantr3 1222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150		3anass 1042	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
151		ancom 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
152	150, 151	bitri 264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
153		ffn 6045	. . . . . . . . . . . . . . . . . 18
154	153	ad2antrl 764	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
155		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
156	136, 155	mp1i 13	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
157		fzfid 12772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
158		simplrr 801	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	136	fvconst2 6469	. . . . . . . . . . . . . . . . . 18
160	159	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	154, 156, 157, 157, 140, 158, 160	ofval 6906	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
162	161	anasss 679	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
163	152, 162	sylan2b 492	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
164		nnne0 11053	. . . . . . . . . . . . . . . 16
165	118, 164	dividd 10799	. . . . . . . . . . . . . . 15
166	165	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
167	163, 166	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
168		ovex 6678	. . . . . . . . . . . . . 14
169		eleq1 2689	. . . . . . . . . . . . . . . . 17
170		fveq1 6190	. . . . . . . . . . . . . . . . . 18
171	170	eqeq1d 2624	. . . . . . . . . . . . . . . . 17
172	169, 171	3anbi23d 1402	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
173	172	anbi2d 740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		fveq2 6191	. . . . . . . . . . . . . . . . 17
175	174	fveq1d 6193	. . . . . . . . . . . . . . . 16
176	175	breq2d 4665	. . . . . . . . . . . . . . 15
177	173, 176	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		poimir.3	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
179	168, 177, 178	vtocl 3259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180	100, 99, 149, 167, 179	syl13anc 1328	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
181		simpr 477	. . . . . . . . . . . . 13 $/\$
182		simp3 1063	. . . . . . . . . . . . 13 $/\$ $/\$
183		neeq1 2856	. . . . . . . . . . . . . . 15
184	164, 183	syl5ibrcom 237	. . . . . . . . . . . . . 14
185	184	imp 445	. . . . . . . . . . . . 13 $/\$
186	181, 182, 185	syl2an 494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
187		vex 3203	. . . . . . . . . . . . 13
188		fveq2 6191	. . . . . . . . . . . . . . 15
189	188	breq2d 4665	. . . . . . . . . . . . . 14
190	66	neeq1d 2853	. . . . . . . . . . . . . 14
191	189, 190	anbi12d 747	. . . . . . . . . . . . 13 $/\$ $/\$
192	187, 191	ralsn 4222	. . . . . . . . . . . 12 $/\$ $/\$
193	180, 186, 192	sylanbrc 698	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
194	40	zcnd 11483	. . . . . . . . . . . . . . . . . . 19
195		1cnd 10056	. . . . . . . . . . . . . . . . . . 19
196	194, 195	subeq0ad 10402	. . . . . . . . . . . . . . . . . 18
197	196	biimpcd 239	. . . . . . . . . . . . . . . . 17
198		1z 11407	. . . . . . . . . . . . . . . . . . . . 21
199		fzsn 12383	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
201		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
202		sneq 4187	. . . . . . . . . . . . . . . . . . . 20
203	200, 201, 202	3eqtr4a 2682	. . . . . . . . . . . . . . . . . . 19
204	203	raleqdv 3144	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
205	204	biimprd 238	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
206	197, 205	syl6 35	. . . . . . . . . . . . . . . 16 $/\$ $/\$
207		ralun 3795	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
208		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . . 25
209	194, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
210		elfzuz 12338	. . . . . . . . . . . . . . . . . . . . . . . 24
211	209, 210	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23
212		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . 25
213		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25
214		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . 25
215	40, 212, 213, 214	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
216	209, 215	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . 23
217		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
218	211, 216, 217	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
219	209	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24
220		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . 25
221	40, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
222	219, 221	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23
223	222	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . 22
224	218, 223	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21
225	224	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
226	207, 225	syl5ibr 236	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
227	226	expd 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
228	227	com12 32	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
229	228	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
230	206, 229	jaoi 394	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$ $/\$
231	230	imdistand 728	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
232	231	com12 32	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
233		elun 3753	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
234		ovex 6678	. . . . . . . . . . . . . . . 16
235	234	elsn 4192	. . . . . . . . . . . . . . 15
236		oveq2 6658	. . . . . . . . . . . . . . . . 17
237	236	raleqdv 3144	. . . . . . . . . . . . . . . 16 $/\$ $/\$
238	237	elrab 3363	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
239	235, 238	orbi12i 543	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$
240	233, 239	bitri 264	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
241		oveq2 6658	. . . . . . . . . . . . . . 15
242	241	raleqdv 3144	. . . . . . . . . . . . . 14 $/\$ $/\$
243	242	elrab 3363	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
244	232, 240, 243	3imtr4g 285	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
245		elun2 3781	. . . . . . . . . . . 12 $/\$ $/\$
246	244, 245	syl6 35	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
247	99, 193, 246	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		fimaxre2 10969	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
249	45, 31, 248	mp2an 708	. . . . . . . . . . . 12 $/\$
250	45, 36, 249	3pm3.2i 1239	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
251	250	suprubii 10998	. . . . . . . . . 10 $/\$ $/\$
252	247, 251	syl6 35	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253		ltm1 10863	. . . . . . . . . 10
254		peano2rem 10348	. . . . . . . . . . 11
255	45, 48	sselii 3600	. . . . . . . . . . . 12 $/\$
256		ltletr 10129	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	255, 256	mp3an3 1413	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
258	254, 257	mpancom 703	. . . . . . . . . 10 $/\$ $/\$ $/\$
259	253, 258	mpand 711	. . . . . . . . 9 $/\$ $/\$
260	98, 252, 259	sylsyld 61	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261	255	ltnri 10146	. . . . . . . . . 10 $/\$ $/\$
262		breq1 4656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
263	261, 262	mtbii 316	. . . . . . . . 9 $/\$ $/\$
264	263	necon2ai 2823	. . . . . . . 8 $/\$ $/\$
265	260, 264	syl6 35	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
266		eleq1 2689	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
267	48, 266	mpbii 223	. . . . . . . 8 $/\$ $/\$
268	267	necon3bi 2820	. . . . . . 7 $/\$ $/\$
269	265, 268	pm2.61d1 171	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
270	2, 13, 51, 95, 269, 181	poimirlem28 33437	. . . . 5 $/\$ ..^ $/\$
271		nn0ex 11298	. . . . . . . . . . . 12
272		fzo0ssnn0 12548	. . . . . . . . . . . 12 ..^
273		mapss 7900	. . . . . . . . . . . 12 $/\$ ..^ ..^
274	271, 272, 273	mp2an 708	. . . . . . . . . . 11 ..^
275		xpss1 5228	. . . . . . . . . . 11 ..^ ..^
276	274, 275	ax-mp 5	. . . . . . . . . 10 ..^
277	276	sseli 3599	. . . . . . . . 9 ..^
278		xp1st 7198	. . . . . . . . . 10 ..^ ..^
279		elmapi 7879	. . . . . . . . . 10 ..^ ..^
280		frn 6053	. . . . . . . . . 10 ..^ ..^
281	278, 279, 280	3syl 18	. . . . . . . . 9 ..^ ..^
282	277, 281	jca 554	. . . . . . . 8 ..^ $/\$ ..^
283	282	anim1i 592	. . . . . . 7 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
284		anass 681	. . . . . . 7 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
285	283, 284	sylib 208	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
286	285	reximi2 3010	. . . . 5 ..^ $/\$ ..^ $/\$ $/\$
287	270, 286	syl 17	. . . 4 $/\$ ..^ $/\$ $/\$
288	287	ralrimiva 2966	. . 3 ..^ $/\$ $/\$
289		nnex 11026	. . . 4
290	145, 271	ixpconst 7918	. . . . . . 7
291		omelon 8543	. . . . . . . . . 10
292		nn0ennn 12778	. . . . . . . . . . 11
293		nnenom 12779	. . . . . . . . . . 11
294	292, 293	entr2i 8011	. . . . . . . . . 10
295		isnumi 8772	. . . . . . . . . 10 $/\$
296	291, 294, 295	mp2an 708	. . . . . . . . 9
297	296	rgenw 2924	. . . . . . . 8
298		finixpnum 33394	. . . . . . . 8 $/\$
299	27, 297, 298	mp2an 708	. . . . . . 7
300	290, 299	eqeltrri 2698	. . . . . 6
301	145, 145	mapval 7869	. . . . . . . . 9
302		mapfi 8262	. . . . . . . . . 10 $/\$
303	27, 27, 302	mp2an 708	. . . . . . . . 9
304	301, 303	eqeltrri 2698	. . . . . . . 8
305		f1of 6137	. . . . . . . . 9
306	305	ss2abi 3674	. . . . . . . 8
307		ssfi 8180	. . . . . . . 8 $/\$
308	304, 306, 307	mp2an 708	. . . . . . 7
309		finnum 8774	. . . . . . 7
310	308, 309	ax-mp 5	. . . . . 6
311		xpnum 8777	. . . . . 6 $/\$
312	300, 310, 311	mp2an 708	. . . . 5
313		ssrab2 3687	. . . . . . . 8 ..^ $/\$ $/\$
314	313	rgenw 2924	. . . . . . 7 ..^ $/\$ $/\$
315		ss2iun 4536	. . . . . . 7 ..^ $/\$ $/\$ ..^ $/\$ $/\$
316	314, 315	ax-mp 5	. . . . . 6 ..^ $/\$ $/\$
317		1nn 11031	. . . . . . 7
318		ne0i 3921	. . . . . . 7
319		iunconst 4529	. . . . . . 7
320	317, 318, 319	mp2b 10	. . . . . 6
321	316, 320	sseqtri 3637	. . . . 5 ..^ $/\$ $/\$
322		ssnum 8862	. . . . 5 $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$
323	312, 321, 322	mp2an 708	. . . 4 ..^ $/\$ $/\$
324		fveq2 6191	. . . . . . . 8
325	324	rneqd 5353	. . . . . . 7
326	325	sseq1d 3632	. . . . . 6 ..^ ..^
327		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
328	327	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . 21
329	328	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . 20
330	327	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . 21
331	330	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . 20
332	329, 331	uneq12d 3768	. . . . . . . . . . . . . . . . . . 19
333	324, 332	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
334	333	oveq1d 6665	. . . . . . . . . . . . . . . . 17
335	334	fveq2d 6195	. . . . . . . . . . . . . . . 16
336	335	fveq1d 6193	. . . . . . . . . . . . . . 15
337	336	breq2d 4665	. . . . . . . . . . . . . 14
338	333	fveq1d 6193	. . . . . . . . . . . . . . 15
339	338	neeq1d 2853	. . . . . . . . . . . . . 14
340	337, 339	anbi12d 747	. . . . . . . . . . . . 13 $/\$ $/\$
341	340	ralbidv 2986	. . . . . . . . . . . 12 $/\$ $/\$
342	341	rabbidv 3189	. . . . . . . . . . 11 $/\$ $/\$
343	342	uneq2d 3767	. . . . . . . . . 10 $/\$ $/\$
344	343	supeq1d 8352	. . . . . . . . 9 $/\$ $/\$
345	344	eqeq2d 2632	. . . . . . . 8 $/\$ $/\$
346	345	rexbidv 3052	. . . . . . 7 $/\$ $/\$
347	346	ralbidv 2986	. . . . . 6 $/\$ $/\$
348	326, 347	anbi12d 747	. . . . 5 ..^ $/\$ $/\$ ..^ $/\$ $/\$
349	348	ac6num 9301	. . . 4 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
350	289, 323, 349	mp3an12 1414	. . 3 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
351	288, 350	syl 17	. 2 $/\$ ..^ $/\$ $/\$
352	1	ad2antrr 762	. . . 4 $/\$ $/\$ ..^ $/\$ $/\$
353		poimir.r	. . . 4
354		poimir.1	. . . . 5 ↾_t
355	354	ad2antrr 762	. . . 4 $/\$ $/\$ ..^ $/\$ $/\$ ↾_t
356		eqid 2622	. . . 4
357		simplr 792	. . . 4 $/\$ $/\$ ..^ $/\$ $/\$
358		simpl 473	. . . . . . 7 ..^ $/\$ $/\$ ..^
359	358	ralimi 2952	. . . . . 6 ..^ $/\$ $/\$ ..^
360	359	adantl 482	. . . . 5 $/\$ $/\$ ..^ $/\$ $/\$ ..^
361		fveq2 6191	. . . . . . . . 9
362	361	fveq2d 6195	. . . . . . . 8
363	362	rneqd 5353	. . . . . . 7
364		oveq2 6658	. . . . . . 7 ..^ ..^
365	363, 364	sseq12d 3634	. . . . . 6 ..^ ..^
366	365	rspccva 3308	. . . . 5 ..^ $/\$ ..^
367	360, 366	sylan 488	. . . 4 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^
368		simpll 790	. . . . . 6 $/\$ $/\$ ..^ $/\$ $/\$
369		poimir.2	. . . . . 6 $/\$ $/\$ $/\$
370	368, 369	sylan 488	. . . . 5 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
371		eqid 2622	. . . . 5
372		simpr 477	. . . . . . . 8 ..^ $/\$ $/\$ $/\$
373	372	ralimi 2952	. . . . . . 7 ..^ $/\$ $/\$ $/\$
374	373	adantl 482	. . . . . 6 $/\$ $/\$ ..^ $/\$ $/\$ $/\$
375	361	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
376	375	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . 21
377	376	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . 20
378	375	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . 21
379	378	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . 20
380	377, 379	uneq12d 3768	. . . . . . . . . . . . . . . . . . 19
381	362, 380	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
382		sneq 4187	. . . . . . . . . . . . . . . . . . 19
383	382	xpeq2d 5139	. . . . . . . . . . . . . . . . . 18
384	381, 383	oveq12d 6668	. . . . . . . . . . . . . . . . 17
385	384	fveq2d 6195	. . . . . . . . . . . . . . . 16
386	385	fveq1d 6193	. . . . . . . . . . . . . . 15
387	386	breq2d 4665	. . . . . . . . . . . . . 14
388	381	fveq1d 6193	. . . . . . . . . . . . . . 15
389	388	neeq1d 2853	. . . . . . . . . . . . . 14
390	387, 389	anbi12d 747	. . . . . . . . . . . . 13 $/\$ $/\$
391	390	ralbidv 2986	. . . . . . . . . . . 12 $/\$ $/\$
392	391	rabbidv 3189	. . . . . . . . . . 11 $/\$ $/\$
393	392	uneq2d 3767	. . . . . . . . . 10 $/\$ $/\$
394	393	supeq1d 8352	. . . . . . . . 9 $/\$ $/\$
395	394	eqeq2d 2632	. . . . . . . 8 $/\$ $/\$
396	395	rexbidv 3052	. . . . . . 7 $/\$ $/\$
397		eqeq1 2626	. . . . . . . . 9 $/\$ $/\$
398	397	rexbidv 3052	. . . . . . . 8 $/\$ $/\$
399		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23
400	399	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
401	400	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
402		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
403	402	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
404	403	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
405	404	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
406	401, 405	uneq12d 3768	. . . . . . . . . . . . . . . . . . . 20
407	406	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
408	407	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
409	408	fveq2d 6195	. . . . . . . . . . . . . . . . 17
410	409	fveq1d 6193	. . . . . . . . . . . . . . . 16
411	410	breq2d 4665	. . . . . . . . . . . . . . 15
412	407	fveq1d 6193	. . . . . . . . . . . . . . . 16
413	412	neeq1d 2853	. . . . . . . . . . . . . . 15
414	411, 413	anbi12d 747	. . . . . . . . . . . . . 14 $/\$ $/\$
415	414	ralbidv 2986	. . . . . . . . . . . . 13 $/\$ $/\$
416	415	rabbidv 3189	. . . . . . . . . . . 12 $/\$ $/\$
417	416	uneq2d 3767	. . . . . . . . . . 11 $/\$ $/\$
418	417	supeq1d 8352	. . . . . . . . . 10 $/\$ $/\$
419	418	eqeq2d 2632	. . . . . . . . 9 $/\$ $/\$
420	419	cbvrexv 3172	. . . . . . . 8 $/\$ $/\$
421	398, 420	syl6bb 276	. . . . . . 7 $/\$ $/\$
422	396, 421	rspc2v 3322	. . . . . 6 $/\$ $/\$ $/\$
423	374, 422	mpan9 486	. . . . 5 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
424	352, 142, 353, 355, 370, 371, 357, 367, 423	poimirlem31 33440	. . . 4 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
425	352, 142, 353, 355, 356, 357, 367, 424	poimirlem30 33439	. . 3 $/\$ $/\$ ..^ $/\$ $/\$ ↾_t
426	425	anasss 679	. 2 $/\$ $/\$ ..^ $/\$ $/\$ ↾_t
427	351, 426	exlimddv 1863	1 ↾_t

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

cun 3572

wss 3574

c0 3915

csn 4177

cpr 4179

ciun 4520 class class class wbr 4653

wor 5034

cxp 5112

ccnv 5113

cdm 5114

crn 5115

cima 5117

con0 5723

wfn 5883

wf 5884

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

com 7065

c1st 7166

c2nd 7167

cmap 7857

cixp 7908

cen 7952

cfn 7955

csup 8346

ccrd 8761

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465 ↾_t crest 16081

ctg 16098

cpt 16099

ccn 21028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 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-se 5074 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-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-dvds 14984 df-rest 16083 df-topgen 16104 df-pt 16105 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-lp 20940 df-cn 21031 df-cnp 21032 df-t1 21118 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-hmph 21559 df-ii 22680

This theorem is referenced by: poimir 33442

W3C validator