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 24470

Description: Lemma for chpdifbnd 24472. (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 11721	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3416	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11364	. . . . . . . . . . 11
7	6, 4	remulcld 9689	. . . . . . . . . 10
8		elicc2 11724	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 673	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 215	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1042	. . . . . . 7
12		chpcl 24130	. . . . . . 7 ψ
13	11, 12	syl 17	. . . . . 6 ψ
14		chpcl 24130	. . . . . . 7 ψ
15	4, 14	syl 17	. . . . . 6 ψ
16	13, 15	resubcld 10068	. . . . 5 ψ ψ
17		0red 9662	. . . . . . . 8
18		1re 9660	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 10157	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11719	. . . . . . . . . 10 $/\$
23	3, 22	syl 17	. . . . . . . . 9 $/\$
24	23	simpld 466	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9813	. . . . . . 7
26	4, 25	elrpd 11361	. . . . . 6
27	26	relogcld 23651	. . . . 5
28	16, 27	remulcld 9689	. . . 4 ψ ψ
29		2re 10701	. . . . . . 7
30	11, 4	resubcld 10068	. . . . . . 7
31		remulcl 9642	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 676	. . . . . 6
33	32, 27	remulcld 9689	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11364	. . . . . . 7
36	11, 4	readdcld 9688	. . . . . . 7
37	35, 36	remulcld 9689	. . . . . 6
38	5	relogcld 23651	. . . . . . . 8
39		remulcl 9642	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 676	. . . . . . 7
41	40, 11	remulcld 9689	. . . . . 6
42	37, 41	readdcld 9688	. . . . 5
43	33, 42	readdcld 9688	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9824	. . . . . . . . . 10
46	6, 45	syl 17	. . . . . . . . 9
47	35, 46	remulcld 9689	. . . . . . . 8
48		remulcl 9642	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 676	. . . . . . . . 9
50	49, 38	remulcld 9689	. . . . . . . 8
51	47, 50	readdcld 9688	. . . . . . 7
52	44, 51	syl5eqel 2553	. . . . . 6
53	52, 4	remulcld 9689	. . . . 5
54	33, 53	readdcld 9688	. . . 4
55	13, 27	remulcld 9689	. . . . . . 7 ψ
56		fzfid 12224	. . . . . . . 8
57	10	simp2d 1043	. . . . . . . . . . . 12
58		flword2 12081	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1292	. . . . . . . . . . 11
60		fzss2 11864	. . . . . . . . . . 11
61	59, 60	syl 17	. . . . . . . . . 10
62	61	sselda 3418	. . . . . . . . 9 $/\$
63		elfznn 11854	. . . . . . . . . . . 12
64	63	adantl 473	. . . . . . . . . . 11 $/\$
65		vmacl 24124	. . . . . . . . . . 11 Λ
66	64, 65	syl 17	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10667	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 485	. . . . . . . . . . 11 $/\$
69		chpcl 24130	. . . . . . . . . . 11 ψ
70	68, 69	syl 17	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9689	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 478	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13877	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9688	. . . . . 6 ψ Λ ψ
75		remulcl 9642	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 676	. . . . . . . 8
77	76, 35	resubcld 10068	. . . . . . 7
78	77, 4	remulcld 9689	. . . . . 6
79	5, 26	rpmulcld 11380	. . . . . . . . . 10
80	79	relogcld 23651	. . . . . . . . 9
81		remulcl 9642	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 676	. . . . . . . 8
83	35, 82	readdcld 9688	. . . . . . 7
84	83, 11	remulcld 9689	. . . . . 6
85	15, 27	remulcld 9689	. . . . . . 7 ψ
86	85, 73	readdcld 9688	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9812	. . . . . . . . . . 11
88	11, 87	elrpd 11361	. . . . . . . . . 10
89	88	relogcld 23651	. . . . . . . . 9
90	13, 89	remulcld 9689	. . . . . . . 8 ψ
91		fzfid 12224	. . . . . . . . 9
92		nndivre 10667	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 485	. . . . . . . . . . 11 $/\$
94		chpcl 24130	. . . . . . . . . . 11 ψ
95	93, 94	syl 17	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9689	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13877	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9688	. . . . . . 7 ψ Λ ψ
99		chpge0 24132	. . . . . . . . . 10 ψ
100	11, 99	syl 17	. . . . . . . . 9 ψ
101	26, 88	logled 23655	. . . . . . . . . 10
102	57, 101	mpbid 215	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10569	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13877	. . . . . . . . 9 Λ ψ
105		vmage0 24127	. . . . . . . . . . . 12 Λ
106	64, 105	syl 17	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 24132	. . . . . . . . . . . 12 ψ
108	68, 107	syl 17	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10211	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13933	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 472	. . . . . . . . . . . . 13 $/\$
112	11	adantr 472	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11362	. . . . . . . . . . . . 13 $/\$
114	57	adantr 472	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11419	. . . . . . . . . . . 12 $/\$
116		chpwordi 24163	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1292	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10569	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13936	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9809	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10253	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11392	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9642	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 676	. . . . . . . . . 10
125	35, 124	readdcld 9688	. . . . . . . . 9
126	122, 124	resubcld 10068	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9687	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13575	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13553	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9800	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9809	. . . . . . . . . . . . 13
132		elicopnf 11755	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 677	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5879	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13839	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6324	. . . . . . . . . . . . . . . . . . . 20
146		simpl 464	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6324	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13850	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2517	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6326	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6326	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6324	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6326	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5883	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4405	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3132	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 61	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9809	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10231	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 215	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1044	. . . . . . . . . . . 12
165	88, 79	logled 23655	. . . . . . . . . . . 12
166	164, 165	mpbid 215	. . . . . . . . . . 11
167		2pos 10723	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 462	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10480	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1292	. . . . . . . . . . 11
172	166, 171	mpbid 215	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10249	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9809	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11415	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 215	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9809	. . . . . 6 ψ Λ ψ
178		elicopnf 11755	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 677	. . . . . . . . . 10
181		fveq2 5879	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5879	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6326	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
186		simpl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6323	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13850	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2517	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6326	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6326	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6324	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6326	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5883	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4405	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3132	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 61	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11392	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13573	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 215	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 466	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11410	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 240	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10254	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9687	. . . . . . 7 ψ
209	85	recnd 9687	. . . . . . 7 ψ
210	73	recnd 9687	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 10043	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9687	. . . . . . 7 ψ
213	15	recnd 9687	. . . . . . 7 ψ
214	27	recnd 9687	. . . . . . 7
215	212, 213, 214	subdird 10096	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2508	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9689	. . . . . . . 8
218	217	recnd 9687	. . . . . . 7
219	35, 40	readdcld 9688	. . . . . . . . 9
220	219, 11	remulcld 9689	. . . . . . . 8
221	220	recnd 9687	. . . . . . 7
222	76, 4	remulcld 9689	. . . . . . . 8
223	222	recnd 9687	. . . . . . 7
224	35, 4	remulcld 9689	. . . . . . . . 9
225	224	recnd 9687	. . . . . . . 8
226	225	negcld 9992	. . . . . . 7
227	218, 221, 223, 226	addsub4d 10052	. . . . . 6
228	5, 26	relogmuld 23653	. . . . . . . . . . . . . 14
229	38	recnd 9687	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9853	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2505	. . . . . . . . . . . . 13
232	231	oveq2d 6324	. . . . . . . . . . . 12
233		2cnd 10704	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9685	. . . . . . . . . . . 12
235	232, 234	eqtrd 2505	. . . . . . . . . . 11
236	235	oveq2d 6324	. . . . . . . . . 10
237	35	recnd 9687	. . . . . . . . . . 11
238	76	recnd 9687	. . . . . . . . . . 11
239	40	recnd 9687	. . . . . . . . . . 11
240	237, 238, 239	add12d 9876	. . . . . . . . . 10
241	236, 240	eqtrd 2505	. . . . . . . . 9
242	241	oveq1d 6323	. . . . . . . 8
243	219	recnd 9687	. . . . . . . . 9
244	11	recnd 9687	. . . . . . . . 9
245	238, 243, 244	adddird 9686	. . . . . . . 8
246	242, 245	eqtrd 2505	. . . . . . 7
247	4	recnd 9687	. . . . . . . . 9
248	238, 237, 247	subdird 10096	. . . . . . . 8
249	223, 225	negsubd 10011	. . . . . . . 8
250	248, 249	eqtr4d 2508	. . . . . . 7
251	246, 250	oveq12d 6326	. . . . . 6
252	30	recnd 9687	. . . . . . . . 9
253	233, 252, 214	mul32d 9861	. . . . . . . 8
254	238, 244, 247	subdid 10095	. . . . . . . 8
255	253, 254	eqtrd 2505	. . . . . . 7
256	35, 11	remulcld 9689	. . . . . . . . . . 11
257	256	recnd 9687	. . . . . . . . . 10
258	41	recnd 9687	. . . . . . . . . 10
259	257, 225, 258	add32d 9877	. . . . . . . . 9
260	237, 244, 247	adddid 9685	. . . . . . . . . 10
261	260	oveq1d 6323	. . . . . . . . 9
262	237, 239, 244	adddird 9686	. . . . . . . . . 10
263	262	oveq1d 6323	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2515	. . . . . . . 8
265	221, 225	subnegd 10012	. . . . . . . 8
266	264, 265	eqtr4d 2508	. . . . . . 7
267	255, 266	oveq12d 6326	. . . . . 6
268	227, 251, 267	3eqtr4d 2515	. . . . 5
269	207, 216, 268	3brtr3d 4425	. . . 4 ψ ψ
270	47, 4	remulcld 9689	. . . . . . 7
271	50, 4	remulcld 9689	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10248	. . . . . . . . . 10
273	6	recnd 9687	. . . . . . . . . . . 12
274	19	recnd 9687	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9686	. . . . . . . . . . 11
276	247	mulid2d 9679	. . . . . . . . . . . 12
277	276	oveq2d 6324	. . . . . . . . . . 11
278	275, 277	eqtrd 2505	. . . . . . . . . 10
279	272, 278	breqtrrd 4422	. . . . . . . . 9
280	46, 4	remulcld 9689	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11405	. . . . . . . . 9
282	279, 281	mpbid 215	. . . . . . . 8
283	46	recnd 9687	. . . . . . . . 9
284	237, 283, 247	mulassd 9684	. . . . . . . 8
285	282, 284	breqtrrd 4422	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10722	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 23614	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11329	. . . . . . . . . . . . 13
292		logleb 23631	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 676	. . . . . . . . . . . 12
294	290, 293	mpbid 215	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4430	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10211	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10569	. . . . . . . 8
298	49	recnd 9687	. . . . . . . . . 10
299	298, 229, 247	mulassd 9684	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9863	. . . . . . . . 9
301	299, 300	eqtrd 2505	. . . . . . . 8
302	297, 301	breqtrrd 4422	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10253	. . . . . 6
304	44	oveq1i 6318	. . . . . . 7
305	47	recnd 9687	. . . . . . . 8
306	50	recnd 9687	. . . . . . . 8
307	305, 306, 247	adddird 9686	. . . . . . 7
308	304, 307	syl5eq 2517	. . . . . 6
309	303, 308	breqtrrd 4422	. . . . 5
310	42, 53, 33, 309	leadd2dd 10249	. . . 4
311	28, 43, 54, 269, 310	letrd 9809	. . 3 ψ ψ
312	32	recnd 9687	. . . . 5
313	4, 24	rplogcld 23657	. . . . . . . 8
314	4, 313	rerpdivcld 11392	. . . . . . 7
315	52, 314	remulcld 9689	. . . . . 6
316	315	recnd 9687	. . . . 5
317	312, 316, 214	adddird 9686	. . . 4
318	52	recnd 9687	. . . . . . 7
319	314	recnd 9687	. . . . . . 7
320	318, 319, 214	mulassd 9684	. . . . . 6
321	313	rpne0d 11369	. . . . . . . 8
322	247, 214, 321	divcan1d 10406	. . . . . . 7
323	322	oveq2d 6324	. . . . . 6
324	320, 323	eqtrd 2505	. . . . 5
325	324	oveq2d 6324	. . . 4
326	317, 325	eqtrd 2505	. . 3
327	311, 326	breqtrrd 4422	. 2 ψ ψ
328	32, 315	readdcld 9688	. . 3
329	16, 328, 313	lemul1d 11404	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 240	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

wss 3390 class class class wbr 4395

cfv 5589 (class class class)co 6308

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

cn 10631

c2 10681

cuz 11182

crp 11325

cioo 11660

cico 11662

cicc 11663

cfz 11810

cfl 12059

cabs 13374

csu 13829

clog 23583 Λcvma 24097 ψcchp 24098

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-vma 24103 df-chp 24104

This theorem is referenced by: chpdifbndlem2 24471

W3C validator