chpdifbndlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chpdifbndlem1		Structured version Visualization version Unicode version

Theorem chpdifbndlem1 24403

Description: Lemma for chpdifbnd 24405. (Contributed by Mario Carneiro, 25-May-2016.)

**Hypotheses**
Ref	Expression
chpdifbnd.a
chpdifbnd.1
chpdifbnd.b
chpdifbnd.2	ψ Λ ψ
chpdifbnd.c
chpdifbnd.x
chpdifbnd.y

**Assertion**
Ref	Expression
chpdifbndlem1	ψ ψ

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem chpdifbndlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		chpdifbnd.y	. . . . . . . . 9
2		ioossre 11703	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3432	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11348	. . . . . . . . . . 11
7	6, 4	remulcld 9676	. . . . . . . . . 10
8		elicc2 11706	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 667	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 214	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1021	. . . . . . 7
12		chpcl 24063	. . . . . . 7 ψ
13	11, 12	syl 17	. . . . . 6 ψ
14		chpcl 24063	. . . . . . 7 ψ
15	4, 14	syl 17	. . . . . 6 ψ
16	13, 15	resubcld 10054	. . . . 5 ψ ψ
17		0red 9649	. . . . . . . 8
18		1re 9647	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 10143	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11701	. . . . . . . . . 10 $/\$
23	3, 22	syl 17	. . . . . . . . 9 $/\$
24	23	simpld 461	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9801	. . . . . . 7
26	4, 25	elrpd 11345	. . . . . 6
27	26	relogcld 23584	. . . . 5
28	16, 27	remulcld 9676	. . . 4 ψ ψ
29		2re 10686	. . . . . . 7
30	11, 4	resubcld 10054	. . . . . . 7
31		remulcl 9629	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 670	. . . . . 6
33	32, 27	remulcld 9676	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11348	. . . . . . 7
36	11, 4	readdcld 9675	. . . . . . 7
37	35, 36	remulcld 9676	. . . . . 6
38	5	relogcld 23584	. . . . . . . 8
39		remulcl 9629	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 670	. . . . . . 7
41	40, 11	remulcld 9676	. . . . . 6
42	37, 41	readdcld 9675	. . . . 5
43	33, 42	readdcld 9675	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9811	. . . . . . . . . 10
46	6, 45	syl 17	. . . . . . . . 9
47	35, 46	remulcld 9676	. . . . . . . 8
48		remulcl 9629	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 670	. . . . . . . . 9
50	49, 38	remulcld 9676	. . . . . . . 8
51	47, 50	readdcld 9675	. . . . . . 7
52	44, 51	syl5eqel 2535	. . . . . 6
53	52, 4	remulcld 9676	. . . . 5
54	33, 53	readdcld 9675	. . . 4
55	13, 27	remulcld 9676	. . . . . . 7 ψ
56		fzfid 12193	. . . . . . . 8
57	10	simp2d 1022	. . . . . . . . . . . 12
58		flword2 12055	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1269	. . . . . . . . . . 11
60		fzss2 11845	. . . . . . . . . . 11
61	59, 60	syl 17	. . . . . . . . . 10
62	61	sselda 3434	. . . . . . . . 9 $/\$
63		elfznn 11835	. . . . . . . . . . . 12
64	63	adantl 468	. . . . . . . . . . 11 $/\$
65		vmacl 24057	. . . . . . . . . . 11 Λ
66	64, 65	syl 17	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10652	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 480	. . . . . . . . . . 11 $/\$
69		chpcl 24063	. . . . . . . . . . 11 ψ
70	68, 69	syl 17	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9676	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 473	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13812	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9675	. . . . . 6 ψ Λ ψ
75		remulcl 9629	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 670	. . . . . . . 8
77	76, 35	resubcld 10054	. . . . . . 7
78	77, 4	remulcld 9676	. . . . . 6
79	5, 26	rpmulcld 11364	. . . . . . . . . 10
80	79	relogcld 23584	. . . . . . . . 9
81		remulcl 9629	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 670	. . . . . . . 8
83	35, 82	readdcld 9675	. . . . . . 7
84	83, 11	remulcld 9676	. . . . . 6
85	15, 27	remulcld 9676	. . . . . . 7 ψ
86	85, 73	readdcld 9675	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9800	. . . . . . . . . . 11
88	11, 87	elrpd 11345	. . . . . . . . . 10
89	88	relogcld 23584	. . . . . . . . 9
90	13, 89	remulcld 9676	. . . . . . . 8 ψ
91		fzfid 12193	. . . . . . . . 9
92		nndivre 10652	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 480	. . . . . . . . . . 11 $/\$
94		chpcl 24063	. . . . . . . . . . 11 ψ
95	93, 94	syl 17	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9676	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13812	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9675	. . . . . . 7 ψ Λ ψ
99		chpge0 24065	. . . . . . . . . 10 ψ
100	11, 99	syl 17	. . . . . . . . 9 ψ
101	26, 88	logled 23588	. . . . . . . . . 10
102	57, 101	mpbid 214	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10554	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13812	. . . . . . . . 9 Λ ψ
105		vmage0 24060	. . . . . . . . . . . 12 Λ
106	64, 105	syl 17	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 24065	. . . . . . . . . . . 12 ψ
108	68, 107	syl 17	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10197	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13868	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 467	. . . . . . . . . . . . 13 $/\$
112	11	adantr 467	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11346	. . . . . . . . . . . . 13 $/\$
114	57	adantr 467	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11403	. . . . . . . . . . . 12 $/\$
116		chpwordi 24096	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1269	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10554	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13871	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9797	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10239	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11376	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9629	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 670	. . . . . . . . . 10
125	35, 124	readdcld 9675	. . . . . . . . 9
126	122, 124	resubcld 10054	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9674	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13510	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13488	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9788	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9797	. . . . . . . . . . . . 13
132		elicopnf 11737	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 671	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5870	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5870	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6313	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5870	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6313	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13774	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5870	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6311	. . . . . . . . . . . . . . . . . . . 20
146		simpl 459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6311	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13785	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2499	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6313	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6313	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6311	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6313	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5874	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4415	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3148	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 62	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9797	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10217	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 214	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1023	. . . . . . . . . . . 12
165	88, 79	logled 23588	. . . . . . . . . . . 12
166	164, 165	mpbid 214	. . . . . . . . . . 11
167		2pos 10708	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1269	. . . . . . . . . . 11
172	166, 171	mpbid 214	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10235	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9797	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11399	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 214	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9797	. . . . . 6 ψ Λ ψ
178		elicopnf 11737	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 671	. . . . . . . . . 10
181		fveq2 5870	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5870	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6313	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5870	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6311	. . . . . . . . . . . . . . . . . 18
186		simpl 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6310	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5874	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6311	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13785	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2499	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6313	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6313	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6311	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6313	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5874	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4415	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3148	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 62	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11376	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13508	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 214	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 461	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11394	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 236	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10240	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9674	. . . . . . 7 ψ
209	85	recnd 9674	. . . . . . 7 ψ
210	73	recnd 9674	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 10029	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9674	. . . . . . 7 ψ
213	15	recnd 9674	. . . . . . 7 ψ
214	27	recnd 9674	. . . . . . 7
215	212, 213, 214	subdird 10082	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2490	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9676	. . . . . . . 8
218	217	recnd 9674	. . . . . . 7
219	35, 40	readdcld 9675	. . . . . . . . 9
220	219, 11	remulcld 9676	. . . . . . . 8
221	220	recnd 9674	. . . . . . 7
222	76, 4	remulcld 9676	. . . . . . . 8
223	222	recnd 9674	. . . . . . 7
224	35, 4	remulcld 9676	. . . . . . . . 9
225	224	recnd 9674	. . . . . . . 8
226	225	negcld 9978	. . . . . . 7
227	218, 221, 223, 226	addsub4d 10038	. . . . . 6
228	5, 26	relogmuld 23586	. . . . . . . . . . . . . 14
229	38	recnd 9674	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9840	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2487	. . . . . . . . . . . . 13
232	231	oveq2d 6311	. . . . . . . . . . . 12
233		2cnd 10689	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9672	. . . . . . . . . . . 12
235	232, 234	eqtrd 2487	. . . . . . . . . . 11
236	235	oveq2d 6311	. . . . . . . . . 10
237	35	recnd 9674	. . . . . . . . . . 11
238	76	recnd 9674	. . . . . . . . . . 11
239	40	recnd 9674	. . . . . . . . . . 11
240	237, 238, 239	add12d 9861	. . . . . . . . . 10
241	236, 240	eqtrd 2487	. . . . . . . . 9
242	241	oveq1d 6310	. . . . . . . 8
243	219	recnd 9674	. . . . . . . . 9
244	11	recnd 9674	. . . . . . . . 9
245	238, 243, 244	adddird 9673	. . . . . . . 8
246	242, 245	eqtrd 2487	. . . . . . 7
247	4	recnd 9674	. . . . . . . . 9
248	238, 237, 247	subdird 10082	. . . . . . . 8
249	223, 225	negsubd 9997	. . . . . . . 8
250	248, 249	eqtr4d 2490	. . . . . . 7
251	246, 250	oveq12d 6313	. . . . . 6
252	30	recnd 9674	. . . . . . . . 9
253	233, 252, 214	mul32d 9848	. . . . . . . 8
254	238, 244, 247	subdid 10081	. . . . . . . 8
255	253, 254	eqtrd 2487	. . . . . . 7
256	35, 11	remulcld 9676	. . . . . . . . . . 11
257	256	recnd 9674	. . . . . . . . . 10
258	41	recnd 9674	. . . . . . . . . 10
259	257, 225, 258	add32d 9862	. . . . . . . . 9
260	237, 244, 247	adddid 9672	. . . . . . . . . 10
261	260	oveq1d 6310	. . . . . . . . 9
262	237, 239, 244	adddird 9673	. . . . . . . . . 10
263	262	oveq1d 6310	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2497	. . . . . . . 8
265	221, 225	subnegd 9998	. . . . . . . 8
266	264, 265	eqtr4d 2490	. . . . . . 7
267	255, 266	oveq12d 6313	. . . . . 6
268	227, 251, 267	3eqtr4d 2497	. . . . 5
269	207, 216, 268	3brtr3d 4435	. . . 4 ψ ψ
270	47, 4	remulcld 9676	. . . . . . 7
271	50, 4	remulcld 9676	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10234	. . . . . . . . . 10
273	6	recnd 9674	. . . . . . . . . . . 12
274	19	recnd 9674	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9673	. . . . . . . . . . 11
276	247	mulid2d 9666	. . . . . . . . . . . 12
277	276	oveq2d 6311	. . . . . . . . . . 11
278	275, 277	eqtrd 2487	. . . . . . . . . 10
279	272, 278	breqtrrd 4432	. . . . . . . . 9
280	46, 4	remulcld 9676	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11389	. . . . . . . . 9
282	279, 281	mpbid 214	. . . . . . . 8
283	46	recnd 9674	. . . . . . . . 9
284	237, 283, 247	mulassd 9671	. . . . . . . 8
285	282, 284	breqtrrd 4432	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10707	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 23547	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11313	. . . . . . . . . . . . 13
292		logleb 23564	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 670	. . . . . . . . . . . 12
294	290, 293	mpbid 214	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4440	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10197	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10554	. . . . . . . 8
298	49	recnd 9674	. . . . . . . . . 10
299	298, 229, 247	mulassd 9671	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9850	. . . . . . . . 9
301	299, 300	eqtrd 2487	. . . . . . . 8
302	297, 301	breqtrrd 4432	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10239	. . . . . 6
304	44	oveq1i 6305	. . . . . . 7
305	47	recnd 9674	. . . . . . . 8
306	50	recnd 9674	. . . . . . . 8
307	305, 306, 247	adddird 9673	. . . . . . 7
308	304, 307	syl5eq 2499	. . . . . 6
309	303, 308	breqtrrd 4432	. . . . 5
310	42, 53, 33, 309	leadd2dd 10235	. . . 4
311	28, 43, 54, 269, 310	letrd 9797	. . 3 ψ ψ
312	32	recnd 9674	. . . . 5
313	4, 24	rplogcld 23590	. . . . . . . 8
314	4, 313	rerpdivcld 11376	. . . . . . 7
315	52, 314	remulcld 9676	. . . . . 6
316	315	recnd 9674	. . . . 5
317	312, 316, 214	adddird 9673	. . . 4
318	52	recnd 9674	. . . . . . 7
319	314	recnd 9674	. . . . . . 7
320	318, 319, 214	mulassd 9671	. . . . . 6
321	313	rpne0d 11353	. . . . . . . 8
322	247, 214, 321	divcan1d 10391	. . . . . . 7
323	322	oveq2d 6311	. . . . . 6
324	320, 323	eqtrd 2487	. . . . 5
325	324	oveq2d 6311	. . . 4
326	317, 325	eqtrd 2487	. . 3
327	311, 326	breqtrrd 4432	. 2 ψ ψ
328	32, 315	readdcld 9675	. . 3
329	16, 328, 313	lemul1d 11388	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 236	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

wral 2739

wss 3406 class class class wbr 4405

cfv 5585 (class class class)co 6295

cr 9543

cc0 9544

c1 9545

caddc 9547

cmul 9549

cpnf 9677

clt 9680

cle 9681

cmin 9865

cneg 9866

cdiv 10276

cn 10616

c2 10666

cuz 11166

crp 11309

cioo 11642

cico 11644

cicc 11645

cfz 11791

cfl 12033

cabs 13309

csu 13764

clog 23516 Λcvma 24030 ψcchp 24031

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-inf2 8151 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 ax-pre-sup 9622 ax-addf 9623 ax-mulf 9624

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-iin 4284 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-se 4797 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-isom 5594 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-supp 6920 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-map 7479 df-pm 7480 df-ixp 7528 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-fsupp 7889 df-fi 7930 df-sup 7961 df-inf 7962 df-oi 8030 df-card 8378 df-cda 8603 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-7 10680 df-8 10681 df-9 10682 df-10 10683 df-n0 10877 df-z 10945 df-dec 11059 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ioc 11647 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-fac 12467 df-bc 12495 df-hash 12523 df-shft 13142 df-cj 13174 df-re 13175 df-im 13176 df-sqrt 13310 df-abs 13311 df-limsup 13538 df-clim 13564 df-rlim 13565 df-sum 13765 df-ef 14133 df-sin 14135 df-cos 14136 df-pi 14138 df-dvds 14318 df-gcd 14481 df-prm 14635 df-pc 14799 df-struct 15135 df-ndx 15136 df-slot 15137 df-base 15138 df-sets 15139 df-ress 15140 df-plusg 15215 df-mulr 15216 df-starv 15217 df-sca 15218 df-vsca 15219 df-ip 15220 df-tset 15221 df-ple 15222 df-ds 15224 df-unif 15225 df-hom 15226 df-cco 15227 df-rest 15333 df-topn 15334 df-0g 15352 df-gsum 15353 df-topgen 15354 df-pt 15355 df-prds 15358 df-xrs 15412 df-qtop 15418 df-imas 15419 df-xps 15422 df-mre 15504 df-mrc 15505 df-acs 15507 df-mgm 16500 df-sgrp 16539 df-mnd 16549 df-submnd 16595 df-mulg 16688 df-cntz 16983 df-cmn 17444 df-psmet 18974 df-xmet 18975 df-met 18976 df-bl 18977 df-mopn 18978 df-fbas 18979 df-fg 18980 df-cnfld 18983 df-top 19933 df-bases 19934 df-topon 19935 df-topsp 19936 df-cld 20046 df-ntr 20047 df-cls 20048 df-nei 20126 df-lp 20164 df-perf 20165 df-cn 20255 df-cnp 20256 df-haus 20343 df-tx 20589 df-hmeo 20782 df-fil 20873 df-fm 20965 df-flim 20966 df-flf 20967 df-xms 21347 df-ms 21348 df-tms 21349 df-cncf 21922 df-limc 22833 df-dv 22834 df-log 23518 df-vma 24036 df-chp 24037

This theorem is referenced by: chpdifbndlem2 24404

W3C validator