chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 23855

Description: Lemma for chpdifbnd 23857. (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 11507	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3415	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11177	. . . . . . . . . . 11
7	6, 4	remulcld 9535	. . . . . . . . . 10
8		elicc2 11510	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 659	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1006	. . . . . . 7
12		chpcl 23515	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 23515	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9905	. . . . 5 ψ ψ
17		0red 9508	. . . . . . . 8
18		1re 9506	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 9992	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11505	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 457	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9654	. . . . . . 7
26	4, 25	elrpd 11174	. . . . . 6
27	26	relogcld 23095	. . . . 5
28	16, 27	remulcld 9535	. . . 4 ψ ψ
29		2re 10522	. . . . . . 7
30	11, 4	resubcld 9905	. . . . . . 7
31		remulcl 9488	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 661	. . . . . 6
33	32, 27	remulcld 9535	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11177	. . . . . . 7
36	11, 4	readdcld 9534	. . . . . . 7
37	35, 36	remulcld 9535	. . . . . 6
38	5	relogcld 23095	. . . . . . . 8
39		remulcl 9488	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 661	. . . . . . 7
41	40, 11	remulcld 9535	. . . . . 6
42	37, 41	readdcld 9534	. . . . 5
43	33, 42	readdcld 9534	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9664	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9535	. . . . . . . 8
48		remulcl 9488	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 661	. . . . . . . . 9
50	49, 38	remulcld 9535	. . . . . . . 8
51	47, 50	readdcld 9534	. . . . . . 7
52	44, 51	syl5eqel 2474	. . . . . 6
53	52, 4	remulcld 9535	. . . . 5
54	33, 53	readdcld 9534	. . . 4
55	13, 27	remulcld 9535	. . . . . . 7 ψ
56		fzfid 11986	. . . . . . . 8
57	10	simp2d 1007	. . . . . . . . . . . 12
58		flword2 11848	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1226	. . . . . . . . . . 11
60		fzss2 11645	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3417	. . . . . . . . 9 $/\$
63		elfznn 11635	. . . . . . . . . . . 12
64	63	adantl 464	. . . . . . . . . . 11 $/\$
65		vmacl 23509	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10488	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 475	. . . . . . . . . . 11 $/\$
69		chpcl 23515	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9535	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 468	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13558	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9534	. . . . . 6 ψ Λ ψ
75		remulcl 9488	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 661	. . . . . . . 8
77	76, 35	resubcld 9905	. . . . . . 7
78	77, 4	remulcld 9535	. . . . . 6
79	5, 26	rpmulcld 11193	. . . . . . . . . 10
80	79	relogcld 23095	. . . . . . . . 9
81		remulcl 9488	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 661	. . . . . . . 8
83	35, 82	readdcld 9534	. . . . . . 7
84	83, 11	remulcld 9535	. . . . . 6
85	15, 27	remulcld 9535	. . . . . . 7 ψ
86	85, 73	readdcld 9534	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9653	. . . . . . . . . . 11
88	11, 87	elrpd 11174	. . . . . . . . . 10
89	88	relogcld 23095	. . . . . . . . 9
90	13, 89	remulcld 9535	. . . . . . . 8 ψ
91		fzfid 11986	. . . . . . . . 9
92		nndivre 10488	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 475	. . . . . . . . . . 11 $/\$
94		chpcl 23515	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9535	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13558	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9534	. . . . . . 7 ψ Λ ψ
99		chpge0 23517	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 23099	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10402	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13558	. . . . . . . . 9 Λ ψ
105		vmage0 23512	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 23517	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10046	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13612	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 463	. . . . . . . . . . . . 13 $/\$
112	11	adantr 463	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11175	. . . . . . . . . . . . 13 $/\$
114	57	adantr 463	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11231	. . . . . . . . . . . 12 $/\$
116		chpwordi 23548	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1226	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10402	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13615	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9650	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10087	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11204	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9488	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 661	. . . . . . . . . 10
125	35, 124	readdcld 9534	. . . . . . . . 9
126	122, 124	resubcld 9905	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9533	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13269	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13248	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9644	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9650	. . . . . . . . . . . . 13
132		elicopnf 11541	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 662	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5774	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5774	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6214	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5774	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6204	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6214	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13520	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5774	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6212	. . . . . . . . . . . . . . . . . . . 20
146		simpl 455	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6211	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6212	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13531	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2435	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6214	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6214	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6212	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6214	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5778	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4377	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3131	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9650	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10066	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1008	. . . . . . . . . . . 12
165	88, 79	logled 23099	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10544	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 453	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10312	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1226	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10084	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9650	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11227	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9650	. . . . . 6 ψ Λ ψ
178		elicopnf 11541	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 662	. . . . . . . . . 10
181		fveq2 5774	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5774	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6214	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5774	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6212	. . . . . . . . . . . . . . . . . 18
186		simpl 455	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6211	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5778	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6212	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13531	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2435	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6214	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6214	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6212	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6214	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5778	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4377	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3131	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11204	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13268	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 457	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11222	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10088	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9533	. . . . . . 7 ψ
209	85	recnd 9533	. . . . . . 7 ψ
210	73	recnd 9533	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9882	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9533	. . . . . . 7 ψ
213	15	recnd 9533	. . . . . . 7 ψ
214	27	recnd 9533	. . . . . . 7
215	212, 213, 214	subdird 9931	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2426	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9535	. . . . . . . 8
218	217	recnd 9533	. . . . . . 7
219	35, 40	readdcld 9534	. . . . . . . . 9
220	219, 11	remulcld 9535	. . . . . . . 8
221	220	recnd 9533	. . . . . . 7
222	76, 4	remulcld 9535	. . . . . . . 8
223	222	recnd 9533	. . . . . . 7
224	35, 4	remulcld 9535	. . . . . . . . 9
225	224	recnd 9533	. . . . . . . 8
226	225	negcld 9831	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9891	. . . . . 6
228	5, 26	relogmuld 23097	. . . . . . . . . . . . . 14
229	38	recnd 9533	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9693	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2423	. . . . . . . . . . . . 13
232	231	oveq2d 6212	. . . . . . . . . . . 12
233		2cnd 10525	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9531	. . . . . . . . . . . 12
235	232, 234	eqtrd 2423	. . . . . . . . . . 11
236	235	oveq2d 6212	. . . . . . . . . 10
237	35	recnd 9533	. . . . . . . . . . 11
238	76	recnd 9533	. . . . . . . . . . 11
239	40	recnd 9533	. . . . . . . . . . 11
240	237, 238, 239	add12d 9714	. . . . . . . . . 10
241	236, 240	eqtrd 2423	. . . . . . . . 9
242	241	oveq1d 6211	. . . . . . . 8
243	219	recnd 9533	. . . . . . . . 9
244	11	recnd 9533	. . . . . . . . 9
245	238, 243, 244	adddird 9532	. . . . . . . 8
246	242, 245	eqtrd 2423	. . . . . . 7
247	4	recnd 9533	. . . . . . . . 9
248	238, 237, 247	subdird 9931	. . . . . . . 8
249	223, 225	negsubd 9850	. . . . . . . 8
250	248, 249	eqtr4d 2426	. . . . . . 7
251	246, 250	oveq12d 6214	. . . . . 6
252	30	recnd 9533	. . . . . . . . 9
253	233, 252, 214	mul32d 9701	. . . . . . . 8
254	238, 244, 247	subdid 9930	. . . . . . . 8
255	253, 254	eqtrd 2423	. . . . . . 7
256	35, 11	remulcld 9535	. . . . . . . . . . 11
257	256	recnd 9533	. . . . . . . . . 10
258	41	recnd 9533	. . . . . . . . . 10
259	257, 225, 258	add32d 9715	. . . . . . . . 9
260	237, 244, 247	adddid 9531	. . . . . . . . . 10
261	260	oveq1d 6211	. . . . . . . . 9
262	237, 239, 244	adddird 9532	. . . . . . . . . 10
263	262	oveq1d 6211	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2433	. . . . . . . 8
265	221, 225	subnegd 9851	. . . . . . . 8
266	264, 265	eqtr4d 2426	. . . . . . 7
267	255, 266	oveq12d 6214	. . . . . 6
268	227, 251, 267	3eqtr4d 2433	. . . . 5
269	207, 216, 268	3brtr3d 4396	. . . 4 ψ ψ
270	47, 4	remulcld 9535	. . . . . . 7
271	50, 4	remulcld 9535	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10083	. . . . . . . . . 10
273	6	recnd 9533	. . . . . . . . . . . 12
274	19	recnd 9533	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9532	. . . . . . . . . . 11
276	247	mulid2d 9525	. . . . . . . . . . . 12
277	276	oveq2d 6212	. . . . . . . . . . 11
278	275, 277	eqtrd 2423	. . . . . . . . . 10
279	272, 278	breqtrrd 4393	. . . . . . . . 9
280	46, 4	remulcld 9535	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11217	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9533	. . . . . . . . 9
284	237, 283, 247	mulassd 9530	. . . . . . . 8
285	282, 284	breqtrrd 4393	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10543	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 23058	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11143	. . . . . . . . . . . . 13
292		logleb 23075	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 661	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4401	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10046	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10402	. . . . . . . 8
298	49	recnd 9533	. . . . . . . . . 10
299	298, 229, 247	mulassd 9530	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9703	. . . . . . . . 9
301	299, 300	eqtrd 2423	. . . . . . . 8
302	297, 301	breqtrrd 4393	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10087	. . . . . 6
304	44	oveq1i 6206	. . . . . . 7
305	47	recnd 9533	. . . . . . . 8
306	50	recnd 9533	. . . . . . . 8
307	305, 306, 247	adddird 9532	. . . . . . 7
308	304, 307	syl5eq 2435	. . . . . 6
309	303, 308	breqtrrd 4393	. . . . 5
310	42, 53, 33, 309	leadd2dd 10084	. . . 4
311	28, 43, 54, 269, 310	letrd 9650	. . 3 ψ ψ
312	32	recnd 9533	. . . . 5
313	4, 24	rplogcld 23101	. . . . . . . 8
314	4, 313	rerpdivcld 11204	. . . . . . 7
315	52, 314	remulcld 9535	. . . . . 6
316	315	recnd 9533	. . . . 5
317	312, 316, 214	adddird 9532	. . . 4
318	52	recnd 9533	. . . . . . 7
319	314	recnd 9533	. . . . . . 7
320	318, 319, 214	mulassd 9530	. . . . . 6
321	313	rpne0d 11182	. . . . . . . 8
322	247, 214, 321	divcan1d 10238	. . . . . . 7
323	322	oveq2d 6212	. . . . . 6
324	320, 323	eqtrd 2423	. . . . 5
325	324	oveq2d 6212	. . . 4
326	317, 325	eqtrd 2423	. . 3
327	311, 326	breqtrrd 4393	. 2 ψ ψ
328	32, 315	readdcld 9534	. . 3
329	16, 328, 313	lemul1d 11216	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wral 2732

wss 3389 class class class wbr 4367

cfv 5496 (class class class)co 6196

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

cpnf 9536

clt 9539

cle 9540

cmin 9718

cneg 9719

cdiv 10123

cn 10452

c2 10502

cuz 11001

crp 11139

cioo 11450

cico 11452

cicc 11453

cfz 11593

cfl 11826

cabs 13069

csu 13510

clog 23027 Λcvma 23482 ψcchp 23483

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481 ax-addf 9482 ax-mulf 9483

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-iin 4246 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-of 6439 df-om 6600 df-1st 6699 df-2nd 6700 df-supp 6818 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-map 7340 df-pm 7341 df-ixp 7389 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-fsupp 7745 df-fi 7786 df-sup 7816 df-oi 7850 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-5 10514 df-6 10515 df-7 10516 df-8 10517 df-9 10518 df-10 10519 df-n0 10713 df-z 10782 df-dec 10896 df-uz 11002 df-q 11102 df-rp 11140 df-xneg 11239 df-xadd 11240 df-xmul 11241 df-ioo 11454 df-ioc 11455 df-ico 11456 df-icc 11457 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-fac 12256 df-bc 12283 df-hash 12308 df-shft 12902 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-limsup 13296 df-clim 13313 df-rlim 13314 df-sum 13511 df-ef 13805 df-sin 13807 df-cos 13808 df-pi 13810 df-dvds 13989 df-gcd 14147 df-prm 14220 df-pc 14363 df-struct 14636 df-ndx 14637 df-slot 14638 df-base 14639 df-sets 14640 df-ress 14641 df-plusg 14715 df-mulr 14716 df-starv 14717 df-sca 14718 df-vsca 14719 df-ip 14720 df-tset 14721 df-ple 14722 df-ds 14724 df-unif 14725 df-hom 14726 df-cco 14727 df-rest 14830 df-topn 14831 df-0g 14849 df-gsum 14850 df-topgen 14851 df-pt 14852 df-prds 14855 df-xrs 14909 df-qtop 14914 df-imas 14915 df-xps 14917 df-mre 14993 df-mrc 14994 df-acs 14996 df-mgm 15989 df-sgrp 16028 df-mnd 16038 df-submnd 16084 df-mulg 16177 df-cntz 16472 df-cmn 16917 df-psmet 18524 df-xmet 18525 df-met 18526 df-bl 18527 df-mopn 18528 df-fbas 18529 df-fg 18530 df-cnfld 18534 df-top 19484 df-bases 19486 df-topon 19487 df-topsp 19488 df-cld 19605 df-ntr 19606 df-cls 19607 df-nei 19685 df-lp 19723 df-perf 19724 df-cn 19814 df-cnp 19815 df-haus 19902 df-tx 20148 df-hmeo 20341 df-fil 20432 df-fm 20524 df-flim 20525 df-flf 20526 df-xms 20908 df-ms 20909 df-tms 20910 df-cncf 21467 df-limc 22355 df-dv 22356 df-log 23029 df-vma 23488 df-chp 23489

This theorem is referenced by: chpdifbndlem2 23856

W3C validator