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 31965

Description: Lemma for poimir 31966, combining poimirlem28 31961, poimirlem30 31963, and poimirlem31 31964 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 467	. . . . . 6 $/\$
3		oveq1 6295	. . . . . . . . . . . . . 14
4	3	fveq2d 5867	. . . . . . . . . . . . 13
5	4	fveq1d 5865	. . . . . . . . . . . 12
6	5	breq2d 4413	. . . . . . . . . . 11
7		fveq1 5862	. . . . . . . . . . . 12
8	7	neeq1d 2682	. . . . . . . . . . 11
9	6, 8	anbi12d 716	. . . . . . . . . 10 $/\$ $/\$
10	9	ralbidv 2826	. . . . . . . . 9 $/\$ $/\$
11	10	rabbidv 3035	. . . . . . . 8 $/\$ $/\$
12	11	uneq2d 3587	. . . . . . 7 $/\$ $/\$
13	12	supeq1d 7957	. . . . . 6 $/\$ $/\$
14	1	nnnn0d 10922	. . . . . . . . . . 11
15		0elfz 11886	. . . . . . . . . . 11
16	14, 15	syl 17	. . . . . . . . . 10
17	16	snssd 4116	. . . . . . . . 9
18		ssrab2 3513	. . . . . . . . . . 11 $/\$
19		1eluzge0 11199	. . . . . . . . . . . 12
20		fzss1 11834	. . . . . . . . . . . 12
21	19, 20	ax-mp 5	. . . . . . . . . . 11
22	18, 21	sstri 3440	. . . . . . . . . 10 $/\$
23	22	a1i 11	. . . . . . . . 9 $/\$
24	17, 23	unssd 3609	. . . . . . . 8 $/\$
25		ltso 9711	. . . . . . . . 9
26		snfi 7647	. . . . . . . . . . 11
27		fzfi 12182	. . . . . . . . . . . 12
28		rabfi 7793	. . . . . . . . . . . 12 $/\$
29	27, 28	ax-mp 5	. . . . . . . . . . 11 $/\$
30		unfi 7835	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	26, 29, 30	mp2an 677	. . . . . . . . . 10 $/\$
32		c0ex 9634	. . . . . . . . . . . 12
33	32	snid 3995	. . . . . . . . . . 11
34		elun1 3600	. . . . . . . . . . 11 $/\$
35		ne0i 3736	. . . . . . . . . . 11 $/\$ $/\$
36	33, 34, 35	mp2b 10	. . . . . . . . . 10 $/\$
37		0red 9641	. . . . . . . . . . . . 13
38	37	snssd 4116	. . . . . . . . . . . 12
39	1, 38	ax-mp 5	. . . . . . . . . . 11
40		elfzelz 11797	. . . . . . . . . . . . . 14
41	40	ssriv 3435	. . . . . . . . . . . . 13
42		zssre 10941	. . . . . . . . . . . . 13
43	41, 42	sstri 3440	. . . . . . . . . . . 12
44	18, 43	sstri 3440	. . . . . . . . . . 11 $/\$
45	39, 44	unssi 3608	. . . . . . . . . 10 $/\$
46	31, 36, 45	3pm3.2i 1185	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
47		fisupcl 7982	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	25, 46, 47	mp2an 677	. . . . . . . 8 $/\$ $/\$
49		ssel 3425	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
50	24, 48, 49	mpisyl 21	. . . . . . 7 $/\$
51	50	ad2antrr 731	. . . . . 6 $/\$ $/\$ $/\$
52		elfznn 11825	. . . . . . . . 9
53		nngt0 10635	. . . . . . . . . . . 12
54	53	adantr 467	. . . . . . . . . . 11 $/\$
55		simpr 463	. . . . . . . . . . . . . 14 $/\$
56	55	ralimi 2780	. . . . . . . . . . . . 13 $/\$
57		elfznn 11825	. . . . . . . . . . . . . 14
58		nnre 10613	. . . . . . . . . . . . . . . . . . . 20
59		nnre 10613	. . . . . . . . . . . . . . . . . . . 20
60		lenlt 9709	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	58, 59, 60	syl2an 480	. . . . . . . . . . . . . . . . . . 19 $/\$
62		elfz1b 11861	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	biimpri 210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
64	63	3expia 1209	. . . . . . . . . . . . . . . . . . 19 $/\$
65	61, 64	sylbird 239	. . . . . . . . . . . . . . . . . 18 $/\$
66		fveq2 5863	. . . . . . . . . . . . . . . . . . . . 21
67	66	eqeq1d 2452	. . . . . . . . . . . . . . . . . . . 20
68	67	rspcev 3149	. . . . . . . . . . . . . . . . . . 19 $/\$
69	68	expcom 437	. . . . . . . . . . . . . . . . . 18
70	65, 69	sylan9 662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71	70	an32s 812	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72		nne 2627	. . . . . . . . . . . . . . . . . 18
73	72	rexbii 2888	. . . . . . . . . . . . . . . . 17
74		rexnal 2835	. . . . . . . . . . . . . . . . 17
75	73, 74	bitr3i 255	. . . . . . . . . . . . . . . 16
76	71, 75	syl6ib 230	. . . . . . . . . . . . . . 15 $/\$ $/\$
77	76	con4d 109	. . . . . . . . . . . . . 14 $/\$ $/\$
78	57, 77	sylan2 477	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	syl5 33	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	79	ralrimiva 2801	. . . . . . . . . . 11 $/\$ $/\$
81		ralunb 3614	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
82		breq1 4404	. . . . . . . . . . . . . 14
83	32, 82	ralsn 4009	. . . . . . . . . . . . 13
84		oveq2 6296	. . . . . . . . . . . . . . 15
85	84	raleqdv 2992	. . . . . . . . . . . . . 14 $/\$ $/\$
86	85	ralrab 3199	. . . . . . . . . . . . 13 $/\$ $/\$
87	83, 86	anbi12i 702	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	81, 87	bitri 253	. . . . . . . . . . 11 $/\$ $/\$ $/\$
89	54, 80, 88	sylanbrc 669	. . . . . . . . . 10 $/\$ $/\$
90		breq1 4404	. . . . . . . . . . 11 $/\$ $/\$
91	90	rspcva 3147	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
92	48, 89, 91	sylancr 668	. . . . . . . . 9 $/\$ $/\$
93	52, 92	sylan 474	. . . . . . . 8 $/\$ $/\$
94	93	3adant2 1026	. . . . . . 7 $/\$ $/\$ $/\$
95	94	adantl 468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
96	40	zred 11037	. . . . . . . . . . 11
97	96	3ad2ant1 1028	. . . . . . . . . 10 $/\$ $/\$
98	97	adantl 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
99		simpr1 1013	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100		simpll 759	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101		simplr 761	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102		elfzelz 11797	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	zred 11037	. . . . . . . . . . . . . . . . . . . . . 22
104		nndivre 10642	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
105	103, 104	sylan 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106		elfzle1 11799	. . . . . . . . . . . . . . . . . . . . . . 23
107	103, 106	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108		nnrp 11308	. . . . . . . . . . . . . . . . . . . . . . 23
109	108	rpregt0d 11344	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
110		divge0 10471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111	107, 109, 110	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112		elfzle2 11800	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
114	103	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
115		1red 9655	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
116	108	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
117	114, 115, 116	ledivmuld 11388	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
118		nncn 10614	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	118	mulid1d 9657	. . . . . . . . . . . . . . . . . . . . . . . . 25
120	119	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
122	117, 121	bitrd 257	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	113, 122	mpbird 236	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124		0re 9640	. . . . . . . . . . . . . . . . . . . . . 22
125		1re 9639	. . . . . . . . . . . . . . . . . . . . . 22
126	124, 125	elicc2i 11697	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	105, 111, 123, 126	syl3anbrc 1191	. . . . . . . . . . . . . . . . . . . 20 $/\$
128	127	ancoms 455	. . . . . . . . . . . . . . . . . . 19 $/\$
129		elsni 3992	. . . . . . . . . . . . . . . . . . . . 21
130	129	oveq2d 6304	. . . . . . . . . . . . . . . . . . . 20
131	130	eleq1d 2512	. . . . . . . . . . . . . . . . . . 19
132	128, 131	syl5ibrcom 226	. . . . . . . . . . . . . . . . . 18 $/\$
133	132	impr 624	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
134	101, 133	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
135		simprr 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136		vex 3047	. . . . . . . . . . . . . . . . . 18
137	136	fconst 5767	. . . . . . . . . . . . . . . . 17
138	137	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139		fzfid 12183	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
140		inidm 3640	. . . . . . . . . . . . . . . 16
141	134, 135, 138, 139, 139, 140	off 6543	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142		poimir.i	. . . . . . . . . . . . . . . . 17
143	142	eleq2i 2520	. . . . . . . . . . . . . . . 16
144		ovex 6316	. . . . . . . . . . . . . . . . 17
145		ovex 6316	. . . . . . . . . . . . . . . . 17
146	144, 145	elmap 7497	. . . . . . . . . . . . . . . 16
147	143, 146	bitri 253	. . . . . . . . . . . . . . 15
148	141, 147	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	148	3adantr3 1168	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150		3anass 988	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
151		ancom 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
152	150, 151	bitri 253	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
153		ffn 5726	. . . . . . . . . . . . . . . . . 18
154	153	ad2antrl 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
155		fnconstg 5769	. . . . . . . . . . . . . . . . . 18
156	136, 155	mp1i 13	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
157		fzfid 12183	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
158		simplrr 770	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	136	fvconst2 6118	. . . . . . . . . . . . . . . . . 18
160	159	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	154, 156, 157, 157, 140, 158, 160	ofval 6537	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
162	161	anasss 652	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
163	152, 162	sylan2b 478	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
164		nnne0 10639	. . . . . . . . . . . . . . . 16
165	118, 164	dividd 10378	. . . . . . . . . . . . . . 15
166	165	ad2antlr 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
167	163, 166	eqtrd 2484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
168		ovex 6316	. . . . . . . . . . . . . 14
169		eleq1 2516	. . . . . . . . . . . . . . . . 17
170		fveq1 5862	. . . . . . . . . . . . . . . . . 18
171	170	eqeq1d 2452	. . . . . . . . . . . . . . . . 17
172	169, 171	3anbi23d 1341	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
173	172	anbi2d 709	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		fveq2 5863	. . . . . . . . . . . . . . . . 17
175	174	fveq1d 5865	. . . . . . . . . . . . . . . 16
176	175	breq2d 4413	. . . . . . . . . . . . . . 15
177	173, 176	imbi12d 322	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		poimir.3	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
179	168, 177, 178	vtocl 3099	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180	100, 99, 149, 167, 179	syl13anc 1269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
181		simpr 463	. . . . . . . . . . . . 13 $/\$
182		simp3 1009	. . . . . . . . . . . . 13 $/\$ $/\$
183		neeq1 2685	. . . . . . . . . . . . . . 15
184	164, 183	syl5ibrcom 226	. . . . . . . . . . . . . 14
185	184	imp 431	. . . . . . . . . . . . 13 $/\$
186	181, 182, 185	syl2an 480	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
187		vex 3047	. . . . . . . . . . . . 13
188		fveq2 5863	. . . . . . . . . . . . . . 15
189	188	breq2d 4413	. . . . . . . . . . . . . 14
190	66	neeq1d 2682	. . . . . . . . . . . . . 14
191	189, 190	anbi12d 716	. . . . . . . . . . . . 13 $/\$ $/\$
192	187, 191	ralsn 4009	. . . . . . . . . . . 12 $/\$ $/\$
193	180, 186, 192	sylanbrc 669	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
194	40	zcnd 11038	. . . . . . . . . . . . . . . . . . 19
195		1cnd 9656	. . . . . . . . . . . . . . . . . . 19
196	194, 195	subeq0ad 9993	. . . . . . . . . . . . . . . . . 18
197	196	biimpcd 228	. . . . . . . . . . . . . . . . 17
198		1z 10964	. . . . . . . . . . . . . . . . . . . . 21
199		fzsn 11837	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
201		oveq2 6296	. . . . . . . . . . . . . . . . . . . 20
202		sneq 3977	. . . . . . . . . . . . . . . . . . . 20
203	200, 201, 202	3eqtr4a 2510	. . . . . . . . . . . . . . . . . . 19
204	203	raleqdv 2992	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
205	204	biimprd 227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
206	197, 205	syl6 34	. . . . . . . . . . . . . . . 16 $/\$ $/\$
207		ralun 3615	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
208		npcan1 10041	. . . . . . . . . . . . . . . . . . . . . . . . 25
209	194, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
210		elfzuz 11793	. . . . . . . . . . . . . . . . . . . . . . . 24
211	209, 210	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . . . . 23
212		peano2zm 10977	. . . . . . . . . . . . . . . . . . . . . . . . 25
213		uzid 11170	. . . . . . . . . . . . . . . . . . . . . . . . 25
214		peano2uz 11209	. . . . . . . . . . . . . . . . . . . . . . . . 25
215	40, 212, 213, 214	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
216	209, 215	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . . . . 23
217		fzsplit2 11821	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
218	211, 216, 217	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . 22
219	209	oveq1d 6303	. . . . . . . . . . . . . . . . . . . . . . . 24
220		fzsn 11837	. . . . . . . . . . . . . . . . . . . . . . . . 25
221	40, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
222	219, 221	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . 23
223	222	uneq2d 3587	. . . . . . . . . . . . . . . . . . . . . 22
224	218, 223	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . 21
225	224	raleqdv 2992	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
226	207, 225	syl5ibr 225	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
227	226	expd 438	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
228	227	com12 32	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
229	228	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
230	206, 229	jaoi 381	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$ $/\$
231	230	imdistand 697	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
232	231	com12 32	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
233		elun 3573	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
234		ovex 6316	. . . . . . . . . . . . . . . 16
235	234	elsnc 3991	. . . . . . . . . . . . . . 15
236		oveq2 6296	. . . . . . . . . . . . . . . . 17
237	236	raleqdv 2992	. . . . . . . . . . . . . . . 16 $/\$ $/\$
238	237	elrab 3195	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
239	235, 238	orbi12i 524	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$
240	233, 239	bitri 253	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
241		oveq2 6296	. . . . . . . . . . . . . . 15
242	241	raleqdv 2992	. . . . . . . . . . . . . 14 $/\$ $/\$
243	242	elrab 3195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
244	232, 240, 243	3imtr4g 274	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
245		elun2 3601	. . . . . . . . . . . 12 $/\$ $/\$
246	244, 245	syl6 34	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
247	99, 193, 246	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		fimaxre2 10549	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
249	45, 31, 248	mp2an 677	. . . . . . . . . . . 12 $/\$
250	45, 36, 249	3pm3.2i 1185	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
251	250	suprubii 10579	. . . . . . . . . 10 $/\$ $/\$
252	247, 251	syl6 34	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253		ltm1 10442	. . . . . . . . . 10
254		peano2rem 9938	. . . . . . . . . . 11
255	45, 48	sselii 3428	. . . . . . . . . . . 12 $/\$
256		ltletr 9722	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	255, 256	mp3an3 1352	. . . . . . . . . . 11 $/\$ $/\$ $/\$