chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 24387

Description: Lemma for chpdifbnd 24389. (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 11702	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3464	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11347	. . . . . . . . . . 11
7	6, 4	remulcld 9677	. . . . . . . . . 10
8		elicc2 11705	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 666	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 214	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1018	. . . . . . 7
12		chpcl 24047	. . . . . . 7 ψ
13	11, 12	syl 17	. . . . . 6 ψ
14		chpcl 24047	. . . . . . 7 ψ
15	4, 14	syl 17	. . . . . 6 ψ
16	13, 15	resubcld 10053	. . . . 5 ψ ψ
17		0red 9650	. . . . . . . 8
18		1re 9648	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 10142	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11700	. . . . . . . . . 10 $/\$
23	3, 22	syl 17	. . . . . . . . 9 $/\$
24	23	simpld 461	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9802	. . . . . . 7
26	4, 25	elrpd 11344	. . . . . 6
27	26	relogcld 23568	. . . . 5
28	16, 27	remulcld 9677	. . . 4 ψ ψ
29		2re 10685	. . . . . . 7
30	11, 4	resubcld 10053	. . . . . . 7
31		remulcl 9630	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 668	. . . . . 6
33	32, 27	remulcld 9677	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11347	. . . . . . 7
36	11, 4	readdcld 9676	. . . . . . 7
37	35, 36	remulcld 9677	. . . . . 6
38	5	relogcld 23568	. . . . . . . 8
39		remulcl 9630	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 668	. . . . . . 7
41	40, 11	remulcld 9677	. . . . . 6
42	37, 41	readdcld 9676	. . . . 5
43	33, 42	readdcld 9676	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9812	. . . . . . . . . 10
46	6, 45	syl 17	. . . . . . . . 9
47	35, 46	remulcld 9677	. . . . . . . 8
48		remulcl 9630	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 668	. . . . . . . . 9
50	49, 38	remulcld 9677	. . . . . . . 8
51	47, 50	readdcld 9676	. . . . . . 7
52	44, 51	syl5eqel 2515	. . . . . 6
53	52, 4	remulcld 9677	. . . . 5
54	33, 53	readdcld 9676	. . . 4
55	13, 27	remulcld 9677	. . . . . . 7 ψ
56		fzfid 12191	. . . . . . . 8
57	10	simp2d 1019	. . . . . . . . . . . 12
58		flword2 12053	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1265	. . . . . . . . . . 11
60		fzss2 11844	. . . . . . . . . . 11
61	59, 60	syl 17	. . . . . . . . . 10
62	61	sselda 3466	. . . . . . . . 9 $/\$
63		elfznn 11834	. . . . . . . . . . . 12
64	63	adantl 468	. . . . . . . . . . 11 $/\$
65		vmacl 24041	. . . . . . . . . . 11 Λ
66	64, 65	syl 17	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10651	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 480	. . . . . . . . . . 11 $/\$
69		chpcl 24047	. . . . . . . . . . 11 ψ
70	68, 69	syl 17	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9677	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 473	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13797	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9676	. . . . . 6 ψ Λ ψ
75		remulcl 9630	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 668	. . . . . . . 8
77	76, 35	resubcld 10053	. . . . . . 7
78	77, 4	remulcld 9677	. . . . . 6
79	5, 26	rpmulcld 11363	. . . . . . . . . 10
80	79	relogcld 23568	. . . . . . . . 9
81		remulcl 9630	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 668	. . . . . . . 8
83	35, 82	readdcld 9676	. . . . . . 7
84	83, 11	remulcld 9677	. . . . . 6
85	15, 27	remulcld 9677	. . . . . . 7 ψ
86	85, 73	readdcld 9676	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9801	. . . . . . . . . . 11
88	11, 87	elrpd 11344	. . . . . . . . . 10
89	88	relogcld 23568	. . . . . . . . 9
90	13, 89	remulcld 9677	. . . . . . . 8 ψ
91		fzfid 12191	. . . . . . . . 9
92		nndivre 10651	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 480	. . . . . . . . . . 11 $/\$
94		chpcl 24047	. . . . . . . . . . 11 ψ
95	93, 94	syl 17	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9677	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13797	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9676	. . . . . . 7 ψ Λ ψ
99		chpge0 24049	. . . . . . . . . 10 ψ
100	11, 99	syl 17	. . . . . . . . 9 ψ
101	26, 88	logled 23572	. . . . . . . . . 10
102	57, 101	mpbid 214	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10553	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13797	. . . . . . . . 9 Λ ψ
105		vmage0 24044	. . . . . . . . . . . 12 Λ
106	64, 105	syl 17	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 24049	. . . . . . . . . . . 12 ψ
108	68, 107	syl 17	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10196	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13853	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 467	. . . . . . . . . . . . 13 $/\$
112	11	adantr 467	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11345	. . . . . . . . . . . . 13 $/\$
114	57	adantr 467	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11402	. . . . . . . . . . . 12 $/\$
116		chpwordi 24080	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1265	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10553	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13856	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9798	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10238	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11375	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9630	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 668	. . . . . . . . . 10
125	35, 124	readdcld 9676	. . . . . . . . 9
126	122, 124	resubcld 10053	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9675	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13495	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13474	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9789	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9798	. . . . . . . . . . . . 13
132		elicopnf 11736	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 669	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5880	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5880	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6322	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5880	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6312	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5884	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6322	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13759	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5880	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6320	. . . . . . . . . . . . . . . . . . . 20
146		simpl 459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6319	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5884	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6320	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13770	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2476	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6322	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 23	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6322	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6320	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6322	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5884	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4432	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3179	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 63	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9798	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10216	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 214	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1020	. . . . . . . . . . . 12
165	88, 79	logled 23572	. . . . . . . . . . . 12
166	164, 165	mpbid 214	. . . . . . . . . . 11
167		2pos 10707	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10464	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1265	. . . . . . . . . . 11
172	166, 171	mpbid 214	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10234	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9798	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11398	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 214	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9798	. . . . . 6 ψ Λ ψ
178		elicopnf 11736	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 669	. . . . . . . . . 10
181		fveq2 5880	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5880	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6322	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5880	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6320	. . . . . . . . . . . . . . . . . 18
186		simpl 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6319	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5884	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6320	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13770	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2476	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6322	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 23	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6322	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6320	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6322	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5884	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4432	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3179	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 63	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11375	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13494	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 214	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 461	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11393	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 236	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10239	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9675	. . . . . . 7 ψ
209	85	recnd 9675	. . . . . . 7 ψ
210	73	recnd 9675	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 10030	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9675	. . . . . . 7 ψ
213	15	recnd 9675	. . . . . . 7 ψ
214	27	recnd 9675	. . . . . . 7
215	212, 213, 214	subdird 10081	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2467	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9677	. . . . . . . 8
218	217	recnd 9675	. . . . . . 7
219	35, 40	readdcld 9676	. . . . . . . . 9
220	219, 11	remulcld 9677	. . . . . . . 8
221	220	recnd 9675	. . . . . . 7
222	76, 4	remulcld 9677	. . . . . . . 8
223	222	recnd 9675	. . . . . . 7
224	35, 4	remulcld 9677	. . . . . . . . 9
225	224	recnd 9675	. . . . . . . 8
226	225	negcld 9979	. . . . . . 7
227	218, 221, 223, 226	addsub4d 10039	. . . . . 6
228	5, 26	relogmuld 23570	. . . . . . . . . . . . . 14
229	38	recnd 9675	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9841	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2464	. . . . . . . . . . . . 13
232	231	oveq2d 6320	. . . . . . . . . . . 12
233		2cnd 10688	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9673	. . . . . . . . . . . 12
235	232, 234	eqtrd 2464	. . . . . . . . . . 11
236	235	oveq2d 6320	. . . . . . . . . 10
237	35	recnd 9675	. . . . . . . . . . 11
238	76	recnd 9675	. . . . . . . . . . 11
239	40	recnd 9675	. . . . . . . . . . 11
240	237, 238, 239	add12d 9862	. . . . . . . . . 10
241	236, 240	eqtrd 2464	. . . . . . . . 9
242	241	oveq1d 6319	. . . . . . . 8
243	219	recnd 9675	. . . . . . . . 9
244	11	recnd 9675	. . . . . . . . 9
245	238, 243, 244	adddird 9674	. . . . . . . 8
246	242, 245	eqtrd 2464	. . . . . . 7
247	4	recnd 9675	. . . . . . . . 9
248	238, 237, 247	subdird 10081	. . . . . . . 8
249	223, 225	negsubd 9998	. . . . . . . 8
250	248, 249	eqtr4d 2467	. . . . . . 7
251	246, 250	oveq12d 6322	. . . . . 6
252	30	recnd 9675	. . . . . . . . 9
253	233, 252, 214	mul32d 9849	. . . . . . . 8
254	238, 244, 247	subdid 10080	. . . . . . . 8
255	253, 254	eqtrd 2464	. . . . . . 7
256	35, 11	remulcld 9677	. . . . . . . . . . 11
257	256	recnd 9675	. . . . . . . . . 10
258	41	recnd 9675	. . . . . . . . . 10
259	257, 225, 258	add32d 9863	. . . . . . . . 9
260	237, 244, 247	adddid 9673	. . . . . . . . . 10
261	260	oveq1d 6319	. . . . . . . . 9
262	237, 239, 244	adddird 9674	. . . . . . . . . 10
263	262	oveq1d 6319	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2474	. . . . . . . 8
265	221, 225	subnegd 9999	. . . . . . . 8
266	264, 265	eqtr4d 2467	. . . . . . 7
267	255, 266	oveq12d 6322	. . . . . 6
268	227, 251, 267	3eqtr4d 2474	. . . . 5
269	207, 216, 268	3brtr3d 4452	. . . 4 ψ ψ
270	47, 4	remulcld 9677	. . . . . . 7
271	50, 4	remulcld 9677	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10233	. . . . . . . . . 10
273	6	recnd 9675	. . . . . . . . . . . 12
274	19	recnd 9675	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9674	. . . . . . . . . . 11
276	247	mulid2d 9667	. . . . . . . . . . . 12
277	276	oveq2d 6320	. . . . . . . . . . 11
278	275, 277	eqtrd 2464	. . . . . . . . . 10
279	272, 278	breqtrrd 4449	. . . . . . . . 9
280	46, 4	remulcld 9677	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11388	. . . . . . . . 9
282	279, 281	mpbid 214	. . . . . . . 8
283	46	recnd 9675	. . . . . . . . 9
284	237, 283, 247	mulassd 9672	. . . . . . . 8
285	282, 284	breqtrrd 4449	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10706	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 23531	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11312	. . . . . . . . . . . . 13
292		logleb 23548	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 668	. . . . . . . . . . . 12
294	290, 293	mpbid 214	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4457	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10196	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10553	. . . . . . . 8
298	49	recnd 9675	. . . . . . . . . 10
299	298, 229, 247	mulassd 9672	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9851	. . . . . . . . 9
301	299, 300	eqtrd 2464	. . . . . . . 8
302	297, 301	breqtrrd 4449	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10238	. . . . . 6
304	44	oveq1i 6314	. . . . . . 7
305	47	recnd 9675	. . . . . . . 8
306	50	recnd 9675	. . . . . . . 8
307	305, 306, 247	adddird 9674	. . . . . . 7
308	304, 307	syl5eq 2476	. . . . . 6
309	303, 308	breqtrrd 4449	. . . . 5
310	42, 53, 33, 309	leadd2dd 10234	. . . 4
311	28, 43, 54, 269, 310	letrd 9798	. . 3 ψ ψ
312	32	recnd 9675	. . . . 5
313	4, 24	rplogcld 23574	. . . . . . . 8
314	4, 313	rerpdivcld 11375	. . . . . . 7
315	52, 314	remulcld 9677	. . . . . 6
316	315	recnd 9675	. . . . 5
317	312, 316, 214	adddird 9674	. . . 4
318	52	recnd 9675	. . . . . . 7
319	314	recnd 9675	. . . . . . 7
320	318, 319, 214	mulassd 9672	. . . . . 6
321	313	rpne0d 11352	. . . . . . . 8
322	247, 214, 321	divcan1d 10390	. . . . . . 7
323	322	oveq2d 6320	. . . . . 6
324	320, 323	eqtrd 2464	. . . . 5
325	324	oveq2d 6320	. . . 4
326	317, 325	eqtrd 2464	. . 3
327	311, 326	breqtrrd 4449	. 2 ψ ψ
328	32, 315	readdcld 9676	. . 3
329	16, 328, 313	lemul1d 11387	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 236	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1438

wcel 1869

wral 2776

wss 3438 class class class wbr 4422

cfv 5600 (class class class)co 6304

cr 9544

cc0 9545

c1 9546

caddc 9548

cmul 9550

cpnf 9678

clt 9681

cle 9682

cmin 9866

cneg 9867

cdiv 10275

cn 10615

c2 10665

cuz 11165

crp 11308

cioo 11641

cico 11643

cicc 11644

cfz 11790

cfl 12031

cabs 13295

csu 13749

clog 23500 Λcvma 24014 ψcchp 24015

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4535 ax-sep 4545 ax-nul 4554 ax-pow 4601 ax-pr 4659 ax-un 6596 ax-inf2 8154 ax-cnex 9601 ax-resscn 9602 ax-1cn 9603 ax-icn 9604 ax-addcl 9605 ax-addrcl 9606 ax-mulcl 9607 ax-mulrcl 9608 ax-mulcom 9609 ax-addass 9610 ax-mulass 9611 ax-distr 9612 ax-i2m1 9613 ax-1ne0 9614 ax-1rid 9615 ax-rnegex 9616 ax-rrecex 9617 ax-cnre 9618 ax-pre-lttri 9619 ax-pre-lttrn 9620 ax-pre-ltadd 9621 ax-pre-mulgt0 9622 ax-pre-sup 9623 ax-addf 9624 ax-mulf 9625

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3302 df-csb 3398 df-dif 3441 df-un 3443 df-in 3445 df-ss 3452 df-pss 3454 df-nul 3764 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4219 df-int 4255 df-iun 4300 df-iin 4301 df-br 4423 df-opab 4482 df-mpt 4483 df-tr 4518 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-se 4812 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-isom 5609 df-riota 6266 df-ov 6307 df-oprab 6308 df-mpt2 6309 df-of 6544 df-om 6706 df-1st 6806 df-2nd 6807 df-supp 6925 df-wrecs 7038 df-recs 7100 df-rdg 7138 df-1o 7192 df-2o 7193 df-oadd 7196 df-er 7373 df-map 7484 df-pm 7485 df-ixp 7533 df-en 7580 df-dom 7581 df-sdom 7582 df-fin 7583 df-fsupp 7892 df-fi 7933 df-sup 7964 df-inf 7965 df-oi 8033 df-card 8380 df-cda 8604 df-pnf 9683 df-mnf 9684 df-xr 9685 df-ltxr 9686 df-le 9687 df-sub 9868 df-neg 9869 df-div 10276 df-nn 10616 df-2 10674 df-3 10675 df-4 10676 df-5 10677 df-6 10678 df-7 10679 df-8 10680 df-9 10681 df-10 10682 df-n0 10876 df-z 10944 df-dec 11058 df-uz 11166 df-q 11271 df-rp 11309 df-xneg 11415 df-xadd 11416 df-xmul 11417 df-ioo 11645 df-ioc 11646 df-ico 11647 df-icc 11648 df-fz 11791 df-fzo 11922 df-fl 12033 df-mod 12102 df-seq 12219 df-exp 12278 df-fac 12465 df-bc 12493 df-hash 12521 df-shft 13128 df-cj 13160 df-re 13161 df-im 13162 df-sqrt 13296 df-abs 13297 df-limsup 13523 df-clim 13549 df-rlim 13550 df-sum 13750 df-ef 14118 df-sin 14120 df-cos 14121 df-pi 14123 df-dvds 14303 df-gcd 14466 df-prm 14620 df-pc 14784 df-struct 15120 df-ndx 15121 df-slot 15122 df-base 15123 df-sets 15124 df-ress 15125 df-plusg 15200 df-mulr 15201 df-starv 15202 df-sca 15203 df-vsca 15204 df-ip 15205 df-tset 15206 df-ple 15207 df-ds 15209 df-unif 15210 df-hom 15211 df-cco 15212 df-rest 15318 df-topn 15319 df-0g 15337 df-gsum 15338 df-topgen 15339 df-pt 15340 df-prds 15343 df-xrs 15397 df-qtop 15403 df-imas 15404 df-xps 15407 df-mre 15489 df-mrc 15490 df-acs 15492 df-mgm 16485 df-sgrp 16524 df-mnd 16534 df-submnd 16580 df-mulg 16673 df-cntz 16968 df-cmn 17429 df-psmet 18959 df-xmet 18960 df-met 18961 df-bl 18962 df-mopn 18963 df-fbas 18964 df-fg 18965 df-cnfld 18968 df-top 19917 df-bases 19918 df-topon 19919 df-topsp 19920 df-cld 20030 df-ntr 20031 df-cls 20032 df-nei 20110 df-lp 20148 df-perf 20149 df-cn 20239 df-cnp 20240 df-haus 20327 df-tx 20573 df-hmeo 20766 df-fil 20857 df-fm 20949 df-flim 20950 df-flf 20951 df-xms 21331 df-ms 21332 df-tms 21333 df-cncf 21906 df-limc 22817 df-dv 22818 df-log 23502 df-vma 24020 df-chp 24021

This theorem is referenced by: chpdifbndlem2 24388

W3C validator