poimirlem32 - Mathbox for Brendan Leahy

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

Theorem poimirlem32 31880

Description: Lemma for poimir 31881, combining poimirlem28 31876, poimirlem30 31878, and poimirlem31 31879 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 466	. . . . . 6 $/\$
3		oveq1 6304	. . . . . . . . . . . . . 14
4	3	fveq2d 5877	. . . . . . . . . . . . 13
5	4	fveq1d 5875	. . . . . . . . . . . 12
6	5	breq2d 4429	. . . . . . . . . . 11
7		fveq1 5872	. . . . . . . . . . . 12
8	7	neeq1d 2699	. . . . . . . . . . 11
9	6, 8	anbi12d 715	. . . . . . . . . 10 $/\$ $/\$
10	9	ralbidv 2862	. . . . . . . . 9 $/\$ $/\$
11	10	rabbidv 3070	. . . . . . . 8 $/\$ $/\$
12	11	uneq2d 3617	. . . . . . 7 $/\$ $/\$
13	12	supeq1d 7958	. . . . . 6 $/\$ $/\$
14	1	nnnn0d 10921	. . . . . . . . . . 11
15		0elfz 11883	. . . . . . . . . . 11
16	14, 15	syl 17	. . . . . . . . . 10
17	16	snssd 4139	. . . . . . . . 9
18		ssrab2 3543	. . . . . . . . . . 11 $/\$
19		1eluzge0 11198	. . . . . . . . . . . 12
20		fzss1 11831	. . . . . . . . . . . 12
21	19, 20	ax-mp 5	. . . . . . . . . . 11
22	18, 21	sstri 3470	. . . . . . . . . 10 $/\$
23	22	a1i 11	. . . . . . . . 9 $/\$
24	17, 23	unssd 3639	. . . . . . . 8 $/\$
25		ltso 9710	. . . . . . . . 9
26		snfi 7649	. . . . . . . . . . 11
27		fzfi 12178	. . . . . . . . . . . 12
28		rabfi 7794	. . . . . . . . . . . 12 $/\$
29	27, 28	ax-mp 5	. . . . . . . . . . 11 $/\$
30		unfi 7836	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	26, 29, 30	mp2an 676	. . . . . . . . . 10 $/\$
32		c0ex 9633	. . . . . . . . . . . 12
33	32	snid 4021	. . . . . . . . . . 11
34		elun1 3630	. . . . . . . . . . 11 $/\$
35		ne0i 3764	. . . . . . . . . . 11 $/\$ $/\$
36	33, 34, 35	mp2b 10	. . . . . . . . . 10 $/\$
37		0red 9640	. . . . . . . . . . . . 13
38	37	snssd 4139	. . . . . . . . . . . 12
39	1, 38	ax-mp 5	. . . . . . . . . . 11
40		elfzelz 11794	. . . . . . . . . . . . . 14
41	40	ssriv 3465	. . . . . . . . . . . . 13
42		zssre 10940	. . . . . . . . . . . . 13
43	41, 42	sstri 3470	. . . . . . . . . . . 12
44	18, 43	sstri 3470	. . . . . . . . . . 11 $/\$
45	39, 44	unssi 3638	. . . . . . . . . 10 $/\$
46	31, 36, 45	3pm3.2i 1183	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
47		fisupcl 7983	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	25, 46, 47	mp2an 676	. . . . . . . 8 $/\$ $/\$
49		ssel 3455	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
50	24, 48, 49	mpisyl 22	. . . . . . 7 $/\$
51	50	ad2antrr 730	. . . . . 6 $/\$ $/\$ $/\$
52		elfznn 11822	. . . . . . . . 9
53		nngt0 10634	. . . . . . . . . . . 12
54	53	adantr 466	. . . . . . . . . . 11 $/\$
55		simpr 462	. . . . . . . . . . . . . 14 $/\$
56	55	ralimi 2816	. . . . . . . . . . . . 13 $/\$
57		elfznn 11822	. . . . . . . . . . . . . 14
58		nnre 10612	. . . . . . . . . . . . . . . . . . . 20
59		nnre 10612	. . . . . . . . . . . . . . . . . . . 20
60		lenlt 9708	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	58, 59, 60	syl2an 479	. . . . . . . . . . . . . . . . . . 19 $/\$
62		elfz1b 11858	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	biimpri 209	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
64	63	3expia 1207	. . . . . . . . . . . . . . . . . . 19 $/\$
65	61, 64	sylbird 238	. . . . . . . . . . . . . . . . . 18 $/\$
66		fveq2 5873	. . . . . . . . . . . . . . . . . . . . 21
67	66	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . 20
68	67	rspcev 3179	. . . . . . . . . . . . . . . . . . 19 $/\$
69	68	expcom 436	. . . . . . . . . . . . . . . . . 18
70	65, 69	sylan9 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71	70	an32s 811	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72		nne 2622	. . . . . . . . . . . . . . . . . 18
73	72	rexbii 2925	. . . . . . . . . . . . . . . . 17
74		rexnal 2871	. . . . . . . . . . . . . . . . 17
75	73, 74	bitr3i 254	. . . . . . . . . . . . . . . 16
76	71, 75	syl6ib 229	. . . . . . . . . . . . . . 15 $/\$ $/\$
77	76	con4d 108	. . . . . . . . . . . . . 14 $/\$ $/\$
78	57, 77	sylan2 476	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	syl5 33	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	79	ralrimiva 2837	. . . . . . . . . . 11 $/\$ $/\$
81		ralunb 3644	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
82		breq1 4420	. . . . . . . . . . . . . 14
83	32, 82	ralsn 4032	. . . . . . . . . . . . 13
84		oveq2 6305	. . . . . . . . . . . . . . 15
85	84	raleqdv 3029	. . . . . . . . . . . . . 14 $/\$ $/\$
86	85	ralrab 3230	. . . . . . . . . . . . 13 $/\$ $/\$
87	83, 86	anbi12i 701	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	81, 87	bitri 252	. . . . . . . . . . 11 $/\$ $/\$ $/\$
89	54, 80, 88	sylanbrc 668	. . . . . . . . . 10 $/\$ $/\$
90		breq1 4420	. . . . . . . . . . 11 $/\$ $/\$
91	90	rspcva 3177	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
92	48, 89, 91	sylancr 667	. . . . . . . . 9 $/\$ $/\$
93	52, 92	sylan 473	. . . . . . . 8 $/\$ $/\$
94	93	3adant2 1024	. . . . . . 7 $/\$ $/\$ $/\$
95	94	adantl 467	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
96	40	zred 11036	. . . . . . . . . . 11
97	96	3ad2ant1 1026	. . . . . . . . . 10 $/\$ $/\$
98	97	adantl 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
99		simpr1 1011	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100		simpll 758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101		simplr 760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102		elfzelz 11794	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	zred 11036	. . . . . . . . . . . . . . . . . . . . . 22
104		nndivre 10641	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
105	103, 104	sylan 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106		elfzle1 11796	. . . . . . . . . . . . . . . . . . . . . . 23
107	103, 106	jca 534	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108		nnrp 11307	. . . . . . . . . . . . . . . . . . . . . . 23
109	108	rpregt0d 11343	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
110		divge0 10470	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111	107, 109, 110	syl2an 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112		elfzle2 11797	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
114	103	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
115		1red 9654	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
116	108	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
117	114, 115, 116	ledivmuld 11387	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
118		nncn 10613	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	118	mulid1d 9656	. . . . . . . . . . . . . . . . . . . . . . . . 25
120	119	breq2d 4429	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	adantl 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
122	117, 121	bitrd 256	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	113, 122	mpbird 235	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124		0re 9639	. . . . . . . . . . . . . . . . . . . . . 22
125		1re 9638	. . . . . . . . . . . . . . . . . . . . . 22
126	124, 125	elicc2i 11696	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	105, 111, 123, 126	syl3anbrc 1189	. . . . . . . . . . . . . . . . . . . 20 $/\$
128	127	ancoms 454	. . . . . . . . . . . . . . . . . . 19 $/\$
129		elsni 4018	. . . . . . . . . . . . . . . . . . . . 21
130	129	oveq2d 6313	. . . . . . . . . . . . . . . . . . . 20
131	130	eleq1d 2489	. . . . . . . . . . . . . . . . . . 19
132	128, 131	syl5ibrcom 225	. . . . . . . . . . . . . . . . . 18 $/\$
133	132	impr 623	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
134	101, 133	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
135		simprr 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136		vex 3081	. . . . . . . . . . . . . . . . . 18
137	136	fconst 5778	. . . . . . . . . . . . . . . . 17
138	137	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139		fzfid 12179	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
140		inidm 3668	. . . . . . . . . . . . . . . 16
141	134, 135, 138, 139, 139, 140	off 6552	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142		poimir.i	. . . . . . . . . . . . . . . . 17
143	142	eleq2i 2498	. . . . . . . . . . . . . . . 16
144		ovex 6325	. . . . . . . . . . . . . . . . 17
145		ovex 6325	. . . . . . . . . . . . . . . . 17
146	144, 145	elmap 7500	. . . . . . . . . . . . . . . 16
147	143, 146	bitri 252	. . . . . . . . . . . . . . 15
148	141, 147	sylibr 215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	148	3adantr3 1166	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150		3anass 986	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
151		ancom 451	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
152	150, 151	bitri 252	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
153		ffn 5738	. . . . . . . . . . . . . . . . . 18
154	153	ad2antrl 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
155		fnconstg 5780	. . . . . . . . . . . . . . . . . 18
156	136, 155	mp1i 13	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
157		fzfid 12179	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
158		simplrr 769	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	136	fvconst2 6127	. . . . . . . . . . . . . . . . . 18
160	159	adantl 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	154, 156, 157, 157, 140, 158, 160	ofval 6546	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
162	161	anasss 651	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
163	152, 162	sylan2b 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
164		nnne0 10638	. . . . . . . . . . . . . . . 16
165	118, 164	dividd 10377	. . . . . . . . . . . . . . 15
166	165	ad2antlr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
167	163, 166	eqtrd 2461	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
168		ovex 6325	. . . . . . . . . . . . . 14
169		eleq1 2492	. . . . . . . . . . . . . . . . 17
170		fveq1 5872	. . . . . . . . . . . . . . . . . 18
171	170	eqeq1d 2422	. . . . . . . . . . . . . . . . 17
172	169, 171	3anbi23d 1338	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
173	172	anbi2d 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		fveq2 5873	. . . . . . . . . . . . . . . . 17
175	174	fveq1d 5875	. . . . . . . . . . . . . . . 16
176	175	breq2d 4429	. . . . . . . . . . . . . . 15
177	173, 176	imbi12d 321	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		poimir.3	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
179	168, 177, 178	vtocl 3130	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180	100, 99, 149, 167, 179	syl13anc 1266	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
181		simpr 462	. . . . . . . . . . . . 13 $/\$
182		simp3 1007	. . . . . . . . . . . . 13 $/\$ $/\$
183		neeq1 2703	. . . . . . . . . . . . . . 15
184	164, 183	syl5ibrcom 225	. . . . . . . . . . . . . 14
185	184	imp 430	. . . . . . . . . . . . 13 $/\$
186	181, 182, 185	syl2an 479	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
187		vex 3081	. . . . . . . . . . . . 13
188		fveq2 5873	. . . . . . . . . . . . . . 15
189	188	breq2d 4429	. . . . . . . . . . . . . 14
190	66	neeq1d 2699	. . . . . . . . . . . . . 14
191	189, 190	anbi12d 715	. . . . . . . . . . . . 13 $/\$ $/\$
192	187, 191	ralsn 4032	. . . . . . . . . . . 12 $/\$ $/\$
193	180, 186, 192	sylanbrc 668	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
194	40	zcnd 11037	. . . . . . . . . . . . . . . . . . 19
195		1cnd 9655	. . . . . . . . . . . . . . . . . . 19
196	194, 195	subeq0ad 9992	. . . . . . . . . . . . . . . . . 18
197	196	biimpcd 227	. . . . . . . . . . . . . . . . 17
198		1z 10963	. . . . . . . . . . . . . . . . . . . . 21
199		fzsn 11834	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
201		oveq2 6305	. . . . . . . . . . . . . . . . . . . 20
202		sneq 4003	. . . . . . . . . . . . . . . . . . . 20
203	200, 201, 202	3eqtr4a 2487	. . . . . . . . . . . . . . . . . . 19
204	203	raleqdv 3029	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
205	204	biimprd 226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
206	197, 205	syl6 34	. . . . . . . . . . . . . . . 16 $/\$ $/\$
207		ralun 3645	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
208		npcan1 10040	. . . . . . . . . . . . . . . . . . . . . . . . 25
209	194, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
210		elfzuz 11790	. . . . . . . . . . . . . . . . . . . . . . . 24
211	209, 210	eqeltrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23
212		peano2zm 10976	. . . . . . . . . . . . . . . . . . . . . . . . 25
213		uzid 11169	. . . . . . . . . . . . . . . . . . . . . . . . 25
214		peano2uz 11208	. . . . . . . . . . . . . . . . . . . . . . . . 25
215	40, 212, 213, 214	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
216	209, 215	eqeltrrd 2509	. . . . . . . . . . . . . . . . . . . . . . 23
217		fzsplit2 11818	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
218	211, 216, 217	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . 22
219	209	oveq1d 6312	. . . . . . . . . . . . . . . . . . . . . . . 24
220		fzsn 11834	. . . . . . . . . . . . . . . . . . . . . . . . 25
221	40, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
222	219, 221	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . 23
223	222	uneq2d 3617	. . . . . . . . . . . . . . . . . . . . . 22
224	218, 223	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . 21
225	224	raleqdv 3029	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
226	207, 225	syl5ibr 224	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
227	226	expd 437	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
228	227	com12 32	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
229	228	adantl 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
230	206, 229	jaoi 380	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$ $/\$
231	230	imdistand 696	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
232	231	com12 32	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
233		elun 3603	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
234		ovex 6325	. . . . . . . . . . . . . . . 16
235	234	elsnc 4017	. . . . . . . . . . . . . . 15
236		oveq2 6305	. . . . . . . . . . . . . . . . 17
237	236	raleqdv 3029	. . . . . . . . . . . . . . . 16 $/\$ $/\$
238	237	elrab 3226	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
239	235, 238	orbi12i 523	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$
240	233, 239	bitri 252	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
241		oveq2 6305	. . . . . . . . . . . . . . 15
242	241	raleqdv 3029	. . . . . . . . . . . . . 14 $/\$ $/\$
243	242	elrab 3226	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
244	232, 240, 243	3imtr4g 273	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
245		elun2 3631	. . . . . . . . . . . 12 $/\$ $/\$
246	244, 245	syl6 34	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
247	99, 193, 246	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		fimaxre2 10548	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
249	45, 31, 248	mp2an 676	. . . . . . . . . . . 12 $/\$
250	45, 36, 249	3pm3.2i 1183	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
251	250	suprubii 10578	. . . . . . . . . 10 $/\$ $/\$
252	247, 251	syl6 34	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253		ltm1 10441	. . . . . . . . . 10
254		peano2rem 9937	. . . . . . . . . . 11
255	45, 48	sselii 3458	. . . . . . . . . . . 12 $/\$
256		ltletr 9721	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	255, 256	mp3an3 1349	. . . . . . . . . . 11 $/\$ $/\$ $/\$