chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 23603

Description: Lemma for chpdifbnd 23605. (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 11590	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3484	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11260	. . . . . . . . . . 11
7	6, 4	remulcld 9622	. . . . . . . . . 10
8		elicc2 11593	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1007	. . . . . . 7
12		chpcl 23263	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 23263	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9988	. . . . 5 ψ ψ
17		0red 9595	. . . . . . . 8
18		1re 9593	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 10076	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11588	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 459	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9741	. . . . . . 7
26	4, 25	elrpd 11258	. . . . . 6
27	26	relogcld 22873	. . . . 5
28	16, 27	remulcld 9622	. . . 4 ψ ψ
29		2re 10606	. . . . . . 7
30	11, 4	resubcld 9988	. . . . . . 7
31		remulcl 9575	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 663	. . . . . 6
33	32, 27	remulcld 9622	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11260	. . . . . . 7
36	11, 4	readdcld 9621	. . . . . . 7
37	35, 36	remulcld 9622	. . . . . 6
38	5	relogcld 22873	. . . . . . . 8
39		remulcl 9575	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 663	. . . . . . 7
41	40, 11	remulcld 9622	. . . . . 6
42	37, 41	readdcld 9621	. . . . 5
43	33, 42	readdcld 9621	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9751	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9622	. . . . . . . 8
48		remulcl 9575	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 663	. . . . . . . . 9
50	49, 38	remulcld 9622	. . . . . . . 8
51	47, 50	readdcld 9621	. . . . . . 7
52	44, 51	syl5eqel 2533	. . . . . 6
53	52, 4	remulcld 9622	. . . . 5
54	33, 53	readdcld 9621	. . . 4
55	13, 27	remulcld 9622	. . . . . . 7 ψ
56		fzfid 12057	. . . . . . . 8
57	10	simp2d 1008	. . . . . . . . . . . 12
58		flword2 11923	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1227	. . . . . . . . . . 11
60		fzss2 11727	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3486	. . . . . . . . 9 $/\$
63		elfznn 11718	. . . . . . . . . . . 12
64	63	adantl 466	. . . . . . . . . . 11 $/\$
65		vmacl 23257	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10572	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 477	. . . . . . . . . . 11 $/\$
69		chpcl 23263	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9622	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 470	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13530	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9621	. . . . . 6 ψ Λ ψ
75		remulcl 9575	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 663	. . . . . . . 8
77	76, 35	resubcld 9988	. . . . . . 7
78	77, 4	remulcld 9622	. . . . . 6
79	5, 26	rpmulcld 11276	. . . . . . . . . 10
80	79	relogcld 22873	. . . . . . . . 9
81		remulcl 9575	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 663	. . . . . . . 8
83	35, 82	readdcld 9621	. . . . . . 7
84	83, 11	remulcld 9622	. . . . . 6
85	15, 27	remulcld 9622	. . . . . . 7 ψ
86	85, 73	readdcld 9621	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9740	. . . . . . . . . . 11
88	11, 87	elrpd 11258	. . . . . . . . . 10
89	88	relogcld 22873	. . . . . . . . 9
90	13, 89	remulcld 9622	. . . . . . . 8 ψ
91		fzfid 12057	. . . . . . . . 9
92		nndivre 10572	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 477	. . . . . . . . . . 11 $/\$
94		chpcl 23263	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9622	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13530	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9621	. . . . . . 7 ψ Λ ψ
99		chpge0 23265	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 22877	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10487	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13530	. . . . . . . . 9 Λ ψ
105		vmage0 23260	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 23265	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10130	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13584	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 465	. . . . . . . . . . . . 13 $/\$
112	11	adantr 465	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11259	. . . . . . . . . . . . 13 $/\$
114	57	adantr 465	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11314	. . . . . . . . . . . 12 $/\$
116		chpwordi 23296	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1227	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10487	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13587	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9737	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10171	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11287	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9575	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 663	. . . . . . . . . 10
125	35, 124	readdcld 9621	. . . . . . . . 9
126	122, 124	resubcld 9988	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9620	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13241	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13220	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9731	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9737	. . . . . . . . . . . . 13
132		elicopnf 11624	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 664	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5852	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5852	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6295	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5852	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6285	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6295	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13492	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5852	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6293	. . . . . . . . . . . . . . . . . . . 20
146		simpl 457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6293	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13503	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2494	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6295	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6295	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6293	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6295	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5856	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4443	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3190	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9737	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10150	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1009	. . . . . . . . . . . 12
165	88, 79	logled 22877	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10628	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 455	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10396	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1227	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10168	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9737	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11310	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9737	. . . . . 6 ψ Λ ψ
178		elicopnf 11624	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 664	. . . . . . . . . 10
181		fveq2 5852	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5852	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6295	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5852	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6293	. . . . . . . . . . . . . . . . . 18
186		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6292	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5856	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6293	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13503	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2494	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6295	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6295	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6293	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6295	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5856	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4443	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3190	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11287	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13240	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 459	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11305	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10172	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9620	. . . . . . 7 ψ
209	85	recnd 9620	. . . . . . 7 ψ
210	73	recnd 9620	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9969	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9620	. . . . . . 7 ψ
213	15	recnd 9620	. . . . . . 7 ψ
214	27	recnd 9620	. . . . . . 7
215	212, 213, 214	subdird 10014	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2485	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9622	. . . . . . . 8
218	217	recnd 9620	. . . . . . 7
219	35, 40	readdcld 9621	. . . . . . . . 9
220	219, 11	remulcld 9622	. . . . . . . 8
221	220	recnd 9620	. . . . . . 7
222	76, 4	remulcld 9622	. . . . . . . 8
223	222	recnd 9620	. . . . . . 7
224	35, 4	remulcld 9622	. . . . . . . . 9
225	224	recnd 9620	. . . . . . . 8
226	225	negcld 9918	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9978	. . . . . 6
228	5, 26	relogmuld 22875	. . . . . . . . . . . . . 14
229	38	recnd 9620	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9780	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2482	. . . . . . . . . . . . 13
232	231	oveq2d 6293	. . . . . . . . . . . 12
233		2cnd 10609	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9618	. . . . . . . . . . . 12
235	232, 234	eqtrd 2482	. . . . . . . . . . 11
236	235	oveq2d 6293	. . . . . . . . . 10
237	35	recnd 9620	. . . . . . . . . . 11
238	76	recnd 9620	. . . . . . . . . . 11
239	40	recnd 9620	. . . . . . . . . . 11
240	237, 238, 239	add12d 9801	. . . . . . . . . 10
241	236, 240	eqtrd 2482	. . . . . . . . 9
242	241	oveq1d 6292	. . . . . . . 8
243	219	recnd 9620	. . . . . . . . 9
244	11	recnd 9620	. . . . . . . . 9
245	238, 243, 244	adddird 9619	. . . . . . . 8
246	242, 245	eqtrd 2482	. . . . . . 7
247	4	recnd 9620	. . . . . . . . 9
248	238, 237, 247	subdird 10014	. . . . . . . 8
249	223, 225	negsubd 9937	. . . . . . . 8
250	248, 249	eqtr4d 2485	. . . . . . 7
251	246, 250	oveq12d 6295	. . . . . 6
252	30	recnd 9620	. . . . . . . . 9
253	233, 252, 214	mul32d 9788	. . . . . . . 8
254	238, 244, 247	subdid 10013	. . . . . . . 8
255	253, 254	eqtrd 2482	. . . . . . 7
256	35, 11	remulcld 9622	. . . . . . . . . . 11
257	256	recnd 9620	. . . . . . . . . 10
258	41	recnd 9620	. . . . . . . . . 10
259	257, 225, 258	add32d 9802	. . . . . . . . 9
260	237, 244, 247	adddid 9618	. . . . . . . . . 10
261	260	oveq1d 6292	. . . . . . . . 9
262	237, 239, 244	adddird 9619	. . . . . . . . . 10
263	262	oveq1d 6292	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2492	. . . . . . . 8
265	221, 225	subnegd 9938	. . . . . . . 8
266	264, 265	eqtr4d 2485	. . . . . . 7
267	255, 266	oveq12d 6295	. . . . . 6
268	227, 251, 267	3eqtr4d 2492	. . . . 5
269	207, 216, 268	3brtr3d 4462	. . . 4 ψ ψ
270	47, 4	remulcld 9622	. . . . . . 7
271	50, 4	remulcld 9622	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10167	. . . . . . . . . 10
273	6	recnd 9620	. . . . . . . . . . . 12
274	19	recnd 9620	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9619	. . . . . . . . . . 11
276	247	mulid2d 9612	. . . . . . . . . . . 12
277	276	oveq2d 6293	. . . . . . . . . . 11
278	275, 277	eqtrd 2482	. . . . . . . . . 10
279	272, 278	breqtrrd 4459	. . . . . . . . 9
280	46, 4	remulcld 9622	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11300	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9620	. . . . . . . . 9
284	237, 283, 247	mulassd 9617	. . . . . . . 8
285	282, 284	breqtrrd 4459	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10627	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 22835	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11228	. . . . . . . . . . . . 13
292		logleb 22853	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 663	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4467	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10130	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10487	. . . . . . . 8
298	49	recnd 9620	. . . . . . . . . 10
299	298, 229, 247	mulassd 9617	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9790	. . . . . . . . 9
301	299, 300	eqtrd 2482	. . . . . . . 8
302	297, 301	breqtrrd 4459	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10171	. . . . . 6
304	44	oveq1i 6287	. . . . . . 7
305	47	recnd 9620	. . . . . . . 8
306	50	recnd 9620	. . . . . . . 8
307	305, 306, 247	adddird 9619	. . . . . . 7
308	304, 307	syl5eq 2494	. . . . . 6
309	303, 308	breqtrrd 4459	. . . . 5
310	42, 53, 33, 309	leadd2dd 10168	. . . 4
311	28, 43, 54, 269, 310	letrd 9737	. . 3 ψ ψ
312	32	recnd 9620	. . . . 5
313	4, 24	rplogcld 22879	. . . . . . . 8
314	4, 313	rerpdivcld 11287	. . . . . . 7
315	52, 314	remulcld 9622	. . . . . 6
316	315	recnd 9620	. . . . 5
317	312, 316, 214	adddird 9619	. . . 4
318	52	recnd 9620	. . . . . . 7
319	314	recnd 9620	. . . . . . 7
320	318, 319, 214	mulassd 9617	. . . . . 6
321	313	rpne0d 11265	. . . . . . . 8
322	247, 214, 321	divcan1d 10322	. . . . . . 7
323	322	oveq2d 6293	. . . . . 6
324	320, 323	eqtrd 2482	. . . . 5
325	324	oveq2d 6293	. . . 4
326	317, 325	eqtrd 2482	. . 3
327	311, 326	breqtrrd 4459	. 2 ψ ψ
328	32, 315	readdcld 9621	. . 3
329	16, 328, 313	lemul1d 11299	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 972

wceq 1381

wcel 1802

wral 2791

wss 3458 class class class wbr 4433

cfv 5574 (class class class)co 6277

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

cpnf 9623

clt 9626

cle 9627

cmin 9805

cneg 9806

cdiv 10207

cn 10537

c2 10586

cuz 11085

crp 11224

cioo 11533

cico 11535

cicc 11536

cfz 11676

cfl 11901

cabs 13041

csu 13482

clog 22807 Λcvma 23230 ψcchp 23231

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-inf2 8056 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568 ax-addf 9569 ax-mulf 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-fal 1387 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-int 4268 df-iun 4313 df-iin 4314 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-se 4825 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-isom 5583 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-of 6521 df-om 6682 df-1st 6781 df-2nd 6782 df-supp 6900 df-recs 7040 df-rdg 7074 df-1o 7128 df-2o 7129 df-oadd 7132 df-er 7309 df-map 7420 df-pm 7421 df-ixp 7468 df-en 7515 df-dom 7516 df-sdom 7517 df-fin 7518 df-fsupp 7828 df-fi 7869 df-sup 7899 df-oi 7933 df-card 8318 df-cda 8546 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-4 10597 df-5 10598 df-6 10599 df-7 10600 df-8 10601 df-9 10602 df-10 10603 df-n0 10797 df-z 10866 df-dec 10980 df-uz 11086 df-q 11187 df-rp 11225 df-xneg 11322 df-xadd 11323 df-xmul 11324 df-ioo 11537 df-ioc 11538 df-ico 11539 df-icc 11540 df-fz 11677 df-fzo 11799 df-fl 11903 df-mod 11971 df-seq 12082 df-exp 12141 df-fac 12328 df-bc 12355 df-hash 12380 df-shft 12874 df-cj 12906 df-re 12907 df-im 12908 df-sqrt 13042 df-abs 13043 df-limsup 13268 df-clim 13285 df-rlim 13286 df-sum 13483 df-ef 13676 df-sin 13678 df-cos 13679 df-pi 13681 df-dvds 13859 df-gcd 14017 df-prm 14090 df-pc 14233 df-struct 14506 df-ndx 14507 df-slot 14508 df-base 14509 df-sets 14510 df-ress 14511 df-plusg 14582 df-mulr 14583 df-starv 14584 df-sca 14585 df-vsca 14586 df-ip 14587 df-tset 14588 df-ple 14589 df-ds 14591 df-unif 14592 df-hom 14593 df-cco 14594 df-rest 14692 df-topn 14693 df-0g 14711 df-gsum 14712 df-topgen 14713 df-pt 14714 df-prds 14717 df-xrs 14771 df-qtop 14776 df-imas 14777 df-xps 14779 df-mre 14855 df-mrc 14856 df-acs 14858 df-mgm 15741 df-sgrp 15780 df-mnd 15790 df-submnd 15836 df-mulg 15929 df-cntz 16224 df-cmn 16669 df-psmet 18279 df-xmet 18280 df-met 18281 df-bl 18282 df-mopn 18283 df-fbas 18284 df-fg 18285 df-cnfld 18289 df-top 19266 df-bases 19268 df-topon 19269 df-topsp 19270 df-cld 19386 df-ntr 19387 df-cls 19388 df-nei 19465 df-lp 19503 df-perf 19504 df-cn 19594 df-cnp 19595 df-haus 19682 df-tx 19929 df-hmeo 20122 df-fil 20213 df-fm 20305 df-flim 20306 df-flf 20307 df-xms 20689 df-ms 20690 df-tms 20691 df-cncf 21248 df-limc 22136 df-dv 22137 df-log 22809 df-vma 23236 df-chp 23237

This theorem is referenced by: chpdifbndlem2 23604

W3C validator