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 32036

Description: Lemma for poimir 32037, combining poimirlem28 32032, poimirlem30 32034, and poimirlem31 32035 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 472	. . . . . 6 $/\$
3		oveq1 6315	. . . . . . . . . . . . . 14
4	3	fveq2d 5883	. . . . . . . . . . . . 13
5	4	fveq1d 5881	. . . . . . . . . . . 12
6	5	breq2d 4407	. . . . . . . . . . 11
7		fveq1 5878	. . . . . . . . . . . 12
8	7	neeq1d 2702	. . . . . . . . . . 11
9	6, 8	anbi12d 725	. . . . . . . . . 10 $/\$ $/\$
10	9	ralbidv 2829	. . . . . . . . 9 $/\$ $/\$
11	10	rabbidv 3022	. . . . . . . 8 $/\$ $/\$
12	11	uneq2d 3579	. . . . . . 7 $/\$ $/\$
13	12	supeq1d 7978	. . . . . 6 $/\$ $/\$
14	1	nnnn0d 10949	. . . . . . . . . . 11
15		0elfz 11915	. . . . . . . . . . 11
16	14, 15	syl 17	. . . . . . . . . 10
17	16	snssd 4108	. . . . . . . . 9
18		ssrab2 3500	. . . . . . . . . . 11 $/\$
19		1eluzge0 11226	. . . . . . . . . . . 12
20		fzss1 11863	. . . . . . . . . . . 12
21	19, 20	ax-mp 5	. . . . . . . . . . 11
22	18, 21	sstri 3427	. . . . . . . . . 10 $/\$
23	22	a1i 11	. . . . . . . . 9 $/\$
24	17, 23	unssd 3601	. . . . . . . 8 $/\$
25		ltso 9732	. . . . . . . . 9
26		snfi 7668	. . . . . . . . . . 11
27		fzfi 12223	. . . . . . . . . . . 12
28		rabfi 7814	. . . . . . . . . . . 12 $/\$
29	27, 28	ax-mp 5	. . . . . . . . . . 11 $/\$
30		unfi 7856	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	26, 29, 30	mp2an 686	. . . . . . . . . 10 $/\$
32		c0ex 9655	. . . . . . . . . . . 12
33	32	snid 3988	. . . . . . . . . . 11
34		elun1 3592	. . . . . . . . . . 11 $/\$
35		ne0i 3728	. . . . . . . . . . 11 $/\$ $/\$
36	33, 34, 35	mp2b 10	. . . . . . . . . 10 $/\$
37		0red 9662	. . . . . . . . . . . . 13
38	37	snssd 4108	. . . . . . . . . . . 12
39	1, 38	ax-mp 5	. . . . . . . . . . 11
40		elfzelz 11826	. . . . . . . . . . . . . 14
41	40	ssriv 3422	. . . . . . . . . . . . 13
42		zssre 10968	. . . . . . . . . . . . 13
43	41, 42	sstri 3427	. . . . . . . . . . . 12
44	18, 43	sstri 3427	. . . . . . . . . . 11 $/\$
45	39, 44	unssi 3600	. . . . . . . . . 10 $/\$
46	31, 36, 45	3pm3.2i 1208	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
47		fisupcl 8003	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	25, 46, 47	mp2an 686	. . . . . . . 8 $/\$ $/\$
49		ssel 3412	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
50	24, 48, 49	mpisyl 21	. . . . . . 7 $/\$
51	50	ad2antrr 740	. . . . . 6 $/\$ $/\$ $/\$
52		elfznn 11854	. . . . . . . . 9
53		nngt0 10660	. . . . . . . . . . . 12
54	53	adantr 472	. . . . . . . . . . 11 $/\$
55		simpr 468	. . . . . . . . . . . . . 14 $/\$
56	55	ralimi 2796	. . . . . . . . . . . . 13 $/\$
57		elfznn 11854	. . . . . . . . . . . . . 14
58		nnre 10638	. . . . . . . . . . . . . . . . . . . 20
59		nnre 10638	. . . . . . . . . . . . . . . . . . . 20
60		lenlt 9730	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	58, 59, 60	syl2an 485	. . . . . . . . . . . . . . . . . . 19 $/\$
62		elfz1b 11890	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	biimpri 211	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
64	63	3expia 1233	. . . . . . . . . . . . . . . . . . 19 $/\$
65	61, 64	sylbird 243	. . . . . . . . . . . . . . . . . 18 $/\$
66		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21
67	66	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . 20
68	67	rspcev 3136	. . . . . . . . . . . . . . . . . . 19 $/\$
69	68	expcom 442	. . . . . . . . . . . . . . . . . 18
70	65, 69	sylan9 669	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71	70	an32s 821	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72		nne 2647	. . . . . . . . . . . . . . . . . 18
73	72	rexbii 2881	. . . . . . . . . . . . . . . . 17
74		rexnal 2836	. . . . . . . . . . . . . . . . 17
75	73, 74	bitr3i 259	. . . . . . . . . . . . . . . 16
76	71, 75	syl6ib 234	. . . . . . . . . . . . . . 15 $/\$ $/\$
77	76	con4d 108	. . . . . . . . . . . . . 14 $/\$ $/\$
78	57, 77	sylan2 482	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	syl5 32	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	79	ralrimiva 2809	. . . . . . . . . . 11 $/\$ $/\$
81		ralunb 3606	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
82		breq1 4398	. . . . . . . . . . . . . 14
83	32, 82	ralsn 4001	. . . . . . . . . . . . 13
84		oveq2 6316	. . . . . . . . . . . . . . 15
85	84	raleqdv 2979	. . . . . . . . . . . . . 14 $/\$ $/\$
86	85	ralrab 3188	. . . . . . . . . . . . 13 $/\$ $/\$
87	83, 86	anbi12i 711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	81, 87	bitri 257	. . . . . . . . . . 11 $/\$ $/\$ $/\$
89	54, 80, 88	sylanbrc 677	. . . . . . . . . 10 $/\$ $/\$
90		breq1 4398	. . . . . . . . . . 11 $/\$ $/\$
91	90	rspcva 3134	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
92	48, 89, 91	sylancr 676	. . . . . . . . 9 $/\$ $/\$
93	52, 92	sylan 479	. . . . . . . 8 $/\$ $/\$
94	93	3adant2 1049	. . . . . . 7 $/\$ $/\$ $/\$
95	94	adantl 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
96	40	zred 11063	. . . . . . . . . . 11
97	96	3ad2ant1 1051	. . . . . . . . . 10 $/\$ $/\$
98	97	adantl 473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
99		simpr1 1036	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100		simpll 768	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101		simplr 770	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	zred 11063	. . . . . . . . . . . . . . . . . . . . . 22
104		nndivre 10667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
105	103, 104	sylan 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106		elfzle1 11828	. . . . . . . . . . . . . . . . . . . . . . 23
107	103, 106	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108		nnrp 11334	. . . . . . . . . . . . . . . . . . . . . . 23
109	108	rpregt0d 11370	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
110		divge0 10496	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111	107, 109, 110	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112		elfzle2 11829	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
114	103	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
115		1red 9676	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
116	108	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
117	114, 115, 116	ledivmuld 11414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
118		nncn 10639	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	118	mulid1d 9678	. . . . . . . . . . . . . . . . . . . . . . . . 25
120	119	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
122	117, 121	bitrd 261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	113, 122	mpbird 240	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124		0re 9661	. . . . . . . . . . . . . . . . . . . . . 22
125		1re 9660	. . . . . . . . . . . . . . . . . . . . . 22
126	124, 125	elicc2i 11725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	105, 111, 123, 126	syl3anbrc 1214	. . . . . . . . . . . . . . . . . . . 20 $/\$
128	127	ancoms 460	. . . . . . . . . . . . . . . . . . 19 $/\$
129		elsni 3985	. . . . . . . . . . . . . . . . . . . . 21
130	129	oveq2d 6324	. . . . . . . . . . . . . . . . . . . 20
131	130	eleq1d 2533	. . . . . . . . . . . . . . . . . . 19
132	128, 131	syl5ibrcom 230	. . . . . . . . . . . . . . . . . 18 $/\$
133	132	impr 631	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
134	101, 133	sylan 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
135		simprr 774	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136		vex 3034	. . . . . . . . . . . . . . . . . 18
137	136	fconst 5782	. . . . . . . . . . . . . . . . 17
138	137	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139		fzfid 12224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
140		inidm 3632	. . . . . . . . . . . . . . . 16
141	134, 135, 138, 139, 139, 140	off 6565	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142		poimir.i	. . . . . . . . . . . . . . . . 17
143	142	eleq2i 2541	. . . . . . . . . . . . . . . 16
144		ovex 6336	. . . . . . . . . . . . . . . . 17
145		ovex 6336	. . . . . . . . . . . . . . . . 17
146	144, 145	elmap 7518	. . . . . . . . . . . . . . . 16
147	143, 146	bitri 257	. . . . . . . . . . . . . . 15
148	141, 147	sylibr 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	148	3adantr3 1191	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150		3anass 1011	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
151		ancom 457	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
152	150, 151	bitri 257	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
153		ffn 5739	. . . . . . . . . . . . . . . . . 18
154	153	ad2antrl 742	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
155		fnconstg 5784	. . . . . . . . . . . . . . . . . 18
156	136, 155	mp1i 13	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
157		fzfid 12224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
158		simplrr 779	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	136	fvconst2 6136	. . . . . . . . . . . . . . . . . 18
160	159	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	154, 156, 157, 157, 140, 158, 160	ofval 6559	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
162	161	anasss 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
163	152, 162	sylan2b 483	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
164		nnne0 10664	. . . . . . . . . . . . . . . 16
165	118, 164	dividd 10403	. . . . . . . . . . . . . . 15
166	165	ad2antlr 741	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
167	163, 166	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
168		ovex 6336	. . . . . . . . . . . . . 14
169		eleq1 2537	. . . . . . . . . . . . . . . . 17
170		fveq1 5878	. . . . . . . . . . . . . . . . . 18
171	170	eqeq1d 2473	. . . . . . . . . . . . . . . . 17
172	169, 171	3anbi23d 1368	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
173	172	anbi2d 718	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		fveq2 5879	. . . . . . . . . . . . . . . . 17
175	174	fveq1d 5881	. . . . . . . . . . . . . . . 16
176	175	breq2d 4407	. . . . . . . . . . . . . . 15
177	173, 176	imbi12d 327	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		poimir.3	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
179	168, 177, 178	vtocl 3086	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180	100, 99, 149, 167, 179	syl13anc 1294	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
181		simpr 468	. . . . . . . . . . . . 13 $/\$
182		simp3 1032	. . . . . . . . . . . . 13 $/\$ $/\$
183		neeq1 2705	. . . . . . . . . . . . . . 15
184	164, 183	syl5ibrcom 230	. . . . . . . . . . . . . 14
185	184	imp 436	. . . . . . . . . . . . 13 $/\$
186	181, 182, 185	syl2an 485	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
187		vex 3034	. . . . . . . . . . . . 13
188		fveq2 5879	. . . . . . . . . . . . . . 15
189	188	breq2d 4407	. . . . . . . . . . . . . 14
190	66	neeq1d 2702	. . . . . . . . . . . . . 14
191	189, 190	anbi12d 725	. . . . . . . . . . . . 13 $/\$ $/\$
192	187, 191	ralsn 4001	. . . . . . . . . . . 12 $/\$ $/\$
193	180, 186, 192	sylanbrc 677	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
194	40	zcnd 11064	. . . . . . . . . . . . . . . . . . 19
195		1cnd 9677	. . . . . . . . . . . . . . . . . . 19
196	194, 195	subeq0ad 10015	. . . . . . . . . . . . . . . . . 18
197	196	biimpcd 232	. . . . . . . . . . . . . . . . 17
198		1z 10991	. . . . . . . . . . . . . . . . . . . . 21
199		fzsn 11866	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
201		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20
202		sneq 3969	. . . . . . . . . . . . . . . . . . . 20
203	200, 201, 202	3eqtr4a 2531	. . . . . . . . . . . . . . . . . . 19
204	203	raleqdv 2979	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
205	204	biimprd 231	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
206	197, 205	syl6 33	. . . . . . . . . . . . . . . 16 $/\$ $/\$
207		ralun 3607	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
208		npcan1 10065	. . . . . . . . . . . . . . . . . . . . . . . . 25
209	194, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
210		elfzuz 11822	. . . . . . . . . . . . . . . . . . . . . . . 24
211	209, 210	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . 23
212		peano2zm 11004	. . . . . . . . . . . . . . . . . . . . . . . . 25
213		uzid 11197	. . . . . . . . . . . . . . . . . . . . . . . . 25
214		peano2uz 11235	. . . . . . . . . . . . . . . . . . . . . . . . 25
215	40, 212, 213, 214	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
216	209, 215	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . . . . . 23
217		fzsplit2 11850	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
218	211, 216, 217	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22
219	209	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . 24
220		fzsn 11866	. . . . . . . . . . . . . . . . . . . . . . . . 25
221	40, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
222	219, 221	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . 23
223	222	uneq2d 3579	. . . . . . . . . . . . . . . . . . . . . 22
224	218, 223	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . 21
225	224	raleqdv 2979	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
226	207, 225	syl5ibr 229	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
227	226	expd 443	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
228	227	com12 31	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
229	228	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
230	206, 229	jaoi 386	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$ $/\$
231	230	imdistand 706	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
232	231	com12 31	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
233		elun 3565	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
234		ovex 6336	. . . . . . . . . . . . . . . 16
235	234	elsnc 3984	. . . . . . . . . . . . . . 15
236		oveq2 6316	. . . . . . . . . . . . . . . . 17
237	236	raleqdv 2979	. . . . . . . . . . . . . . . 16 $/\$ $/\$
238	237	elrab 3184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
239	235, 238	orbi12i 530	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$
240	233, 239	bitri 257	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
241		oveq2 6316	. . . . . . . . . . . . . . 15
242	241	raleqdv 2979	. . . . . . . . . . . . . 14 $/\$ $/\$
243	242	elrab 3184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
244	232, 240, 243	3imtr4g 278	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
245		elun2 3593	. . . . . . . . . . . 12 $/\$ $/\$
246	244, 245	syl6 33	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
247	99, 193, 246	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		fimaxre2 10574	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
249	45, 31, 248	mp2an 686	. . . . . . . . . . . 12 $/\$
250	45, 36, 249	3pm3.2i 1208	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
251	250	suprubii 10604	. . . . . . . . . 10 $/\$ $/\$
252	247, 251	syl6 33	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253		ltm1 10467	. . . . . . . . . 10
254		peano2rem 9961	. . . . . . . . . . 11
255	45, 48	sselii 3415	. . . . . . . . . . . 12 $/\$
256		ltletr 9743	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	255, 256	mp3an3 1379	. . . . . . . . . . 11 $/\$ $/\$ $/\$