chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 22687

Description: Lemma for chpdifbnd 22689. (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 11345	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3342	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11015	. . . . . . . . . . 11
7	6, 4	remulcld 9402	. . . . . . . . . 10
8		elicc2 11348	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 654	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 993	. . . . . . 7
12		chpcl 22347	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 22347	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9764	. . . . 5 ψ ψ
17		0red 9375	. . . . . . . 8
18		1re 9373	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 9850	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11343	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 456	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9520	. . . . . . 7
26	4, 25	elrpd 11013	. . . . . 6
27	26	relogcld 21957	. . . . 5
28	16, 27	remulcld 9402	. . . 4 ψ ψ
29		2re 10379	. . . . . . 7
30	11, 4	resubcld 9764	. . . . . . 7
31		remulcl 9355	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 656	. . . . . 6
33	32, 27	remulcld 9402	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11015	. . . . . . 7
36	11, 4	readdcld 9401	. . . . . . 7
37	35, 36	remulcld 9402	. . . . . 6
38	5	relogcld 21957	. . . . . . . 8
39		remulcl 9355	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 656	. . . . . . 7
41	40, 11	remulcld 9402	. . . . . 6
42	37, 41	readdcld 9401	. . . . 5
43	33, 42	readdcld 9401	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9530	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9402	. . . . . . . 8
48		remulcl 9355	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 656	. . . . . . . . 9
50	49, 38	remulcld 9402	. . . . . . . 8
51	47, 50	readdcld 9401	. . . . . . 7
52	44, 51	syl5eqel 2517	. . . . . 6
53	52, 4	remulcld 9402	. . . . 5
54	33, 53	readdcld 9401	. . . 4
55	13, 27	remulcld 9402	. . . . . . 7 ψ
56		fzfid 11779	. . . . . . . 8
57	10	simp2d 994	. . . . . . . . . . . 12
58		flword2 11645	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1211	. . . . . . . . . . 11
60		fzss2 11485	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3344	. . . . . . . . 9 $/\$
63		elfznn 11465	. . . . . . . . . . . 12
64	63	adantl 463	. . . . . . . . . . 11 $/\$
65		vmacl 22341	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10345	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 474	. . . . . . . . . . 11 $/\$
69		chpcl 22347	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9402	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 467	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13195	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9401	. . . . . 6 ψ Λ ψ
75		remulcl 9355	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 656	. . . . . . . 8
77	76, 35	resubcld 9764	. . . . . . 7
78	77, 4	remulcld 9402	. . . . . 6
79	5, 26	rpmulcld 11031	. . . . . . . . . 10
80	79	relogcld 21957	. . . . . . . . 9
81		remulcl 9355	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 656	. . . . . . . 8
83	35, 82	readdcld 9401	. . . . . . 7
84	83, 11	remulcld 9402	. . . . . 6
85	15, 27	remulcld 9402	. . . . . . 7 ψ
86	85, 73	readdcld 9401	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9519	. . . . . . . . . . 11
88	11, 87	elrpd 11013	. . . . . . . . . 10
89	88	relogcld 21957	. . . . . . . . 9
90	13, 89	remulcld 9402	. . . . . . . 8 ψ
91		fzfid 11779	. . . . . . . . 9
92		nndivre 10345	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 474	. . . . . . . . . . 11 $/\$
94		chpcl 22347	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9402	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13195	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9401	. . . . . . 7 ψ Λ ψ
99		chpge0 22349	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 21961	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10261	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13195	. . . . . . . . 9 Λ ψ
105		vmage0 22344	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 22349	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 9904	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13242	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 462	. . . . . . . . . . . . 13 $/\$
112	11	adantr 462	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11014	. . . . . . . . . . . . 13 $/\$
114	57	adantr 462	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11069	. . . . . . . . . . . 12 $/\$
116		chpwordi 22380	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1211	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10261	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13245	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9516	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 9945	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11042	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9355	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 656	. . . . . . . . . 10
125	35, 124	readdcld 9401	. . . . . . . . 9
126	122, 124	resubcld 9764	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9400	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 12906	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 12885	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9510	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9516	. . . . . . . . . . . . 13
132		elicopnf 11373	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 657	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5679	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5679	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6098	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5679	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6088	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5683	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6098	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13157	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5679	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6096	. . . . . . . . . . . . . . . . . . . 20
146		simpl 454	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6095	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5683	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6096	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13168	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2477	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6098	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6098	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6096	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6098	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5683	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4290	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3058	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9516	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 9924	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 995	. . . . . . . . . . . 12
165	88, 79	logled 21961	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10401	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 452	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10170	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1211	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 9942	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9516	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11065	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9516	. . . . . 6 ψ Λ ψ
178		elicopnf 11373	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 657	. . . . . . . . . 10
181		fveq2 5679	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5679	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6098	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5679	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6096	. . . . . . . . . . . . . . . . . 18
186		simpl 454	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6095	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5683	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6096	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13168	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2477	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6098	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6098	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6096	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6098	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5683	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4290	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3058	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11042	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 12905	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 456	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11060	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 9946	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9400	. . . . . . 7 ψ
209	85	recnd 9400	. . . . . . 7 ψ
210	73	recnd 9400	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9745	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9400	. . . . . . 7 ψ
213	15	recnd 9400	. . . . . . 7 ψ
214	27	recnd 9400	. . . . . . 7
215	212, 213, 214	subdird 9789	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2468	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9402	. . . . . . . 8
218	217	recnd 9400	. . . . . . 7
219	35, 40	readdcld 9401	. . . . . . . . 9
220	219, 11	remulcld 9402	. . . . . . . 8
221	220	recnd 9400	. . . . . . 7
222	76, 4	remulcld 9402	. . . . . . . 8
223	222	recnd 9400	. . . . . . 7
224	35, 4	remulcld 9402	. . . . . . . . 9
225	224	recnd 9400	. . . . . . . 8
226	225	negcld 9694	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9754	. . . . . 6
228	5, 26	relogmuld 21959	. . . . . . . . . . . . . 14
229	38	recnd 9400	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9559	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2465	. . . . . . . . . . . . 13
232	231	oveq2d 6096	. . . . . . . . . . . 12
233		2cnd 10382	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9398	. . . . . . . . . . . 12
235	232, 234	eqtrd 2465	. . . . . . . . . . 11
236	235	oveq2d 6096	. . . . . . . . . 10
237	35	recnd 9400	. . . . . . . . . . 11
238	76	recnd 9400	. . . . . . . . . . 11
239	40	recnd 9400	. . . . . . . . . . 11
240	237, 238, 239	add12d 9579	. . . . . . . . . 10
241	236, 240	eqtrd 2465	. . . . . . . . 9
242	241	oveq1d 6095	. . . . . . . 8
243	219	recnd 9400	. . . . . . . . 9
244	11	recnd 9400	. . . . . . . . 9
245	238, 243, 244	adddird 9399	. . . . . . . 8
246	242, 245	eqtrd 2465	. . . . . . 7
247	4	recnd 9400	. . . . . . . . 9
248	238, 237, 247	subdird 9789	. . . . . . . 8
249	223, 225	negsubd 9713	. . . . . . . 8
250	248, 249	eqtr4d 2468	. . . . . . 7
251	246, 250	oveq12d 6098	. . . . . 6
252	30	recnd 9400	. . . . . . . . 9
253	233, 252, 214	mul32d 9567	. . . . . . . 8
254	238, 244, 247	subdid 9788	. . . . . . . 8
255	253, 254	eqtrd 2465	. . . . . . 7
256	35, 11	remulcld 9402	. . . . . . . . . . 11
257	256	recnd 9400	. . . . . . . . . 10
258	41	recnd 9400	. . . . . . . . . 10
259	257, 225, 258	add32d 9580	. . . . . . . . 9
260	237, 244, 247	adddid 9398	. . . . . . . . . 10
261	260	oveq1d 6095	. . . . . . . . 9
262	237, 239, 244	adddird 9399	. . . . . . . . . 10
263	262	oveq1d 6095	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2475	. . . . . . . 8
265	221, 225	subnegd 9714	. . . . . . . 8
266	264, 265	eqtr4d 2468	. . . . . . 7
267	255, 266	oveq12d 6098	. . . . . 6
268	227, 251, 267	3eqtr4d 2475	. . . . 5
269	207, 216, 268	3brtr3d 4309	. . . 4 ψ ψ
270	47, 4	remulcld 9402	. . . . . . 7
271	50, 4	remulcld 9402	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 9941	. . . . . . . . . 10
273	6	recnd 9400	. . . . . . . . . . . 12
274	19	recnd 9400	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9399	. . . . . . . . . . 11
276	247	mulid2d 9392	. . . . . . . . . . . 12
277	276	oveq2d 6096	. . . . . . . . . . 11
278	275, 277	eqtrd 2465	. . . . . . . . . 10
279	272, 278	breqtrrd 4306	. . . . . . . . 9
280	46, 4	remulcld 9402	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11055	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9400	. . . . . . . . 9
284	237, 283, 247	mulassd 9397	. . . . . . . 8
285	282, 284	breqtrrd 4306	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10400	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 21919	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 10983	. . . . . . . . . . . . 13
292		logleb 21937	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 656	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4314	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 9904	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10261	. . . . . . . 8
298	49	recnd 9400	. . . . . . . . . 10
299	298, 229, 247	mulassd 9397	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9569	. . . . . . . . 9
301	299, 300	eqtrd 2465	. . . . . . . 8
302	297, 301	breqtrrd 4306	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 9945	. . . . . 6
304	44	oveq1i 6090	. . . . . . 7
305	47	recnd 9400	. . . . . . . 8
306	50	recnd 9400	. . . . . . . 8
307	305, 306, 247	adddird 9399	. . . . . . 7
308	304, 307	syl5eq 2477	. . . . . 6
309	303, 308	breqtrrd 4306	. . . . 5
310	42, 53, 33, 309	leadd2dd 9942	. . . 4
311	28, 43, 54, 269, 310	letrd 9516	. . 3 ψ ψ
312	32	recnd 9400	. . . . 5
313	4, 24	rplogcld 21963	. . . . . . . 8
314	4, 313	rerpdivcld 11042	. . . . . . 7
315	52, 314	remulcld 9402	. . . . . 6
316	315	recnd 9400	. . . . 5
317	312, 316, 214	adddird 9399	. . . 4
318	52	recnd 9400	. . . . . . 7
319	314	recnd 9400	. . . . . . 7
320	318, 319, 214	mulassd 9397	. . . . . 6
321	313	rpne0d 11020	. . . . . . . 8
322	247, 214, 321	divcan1d 10096	. . . . . . 7
323	322	oveq2d 6096	. . . . . 6
324	320, 323	eqtrd 2465	. . . . 5
325	324	oveq2d 6096	. . . 4
326	317, 325	eqtrd 2465	. . 3
327	311, 326	breqtrrd 4306	. 2 ψ ψ
328	32, 315	readdcld 9401	. . 3
329	16, 328, 313	lemul1d 11054	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1362

wcel 1755

wral 2705

wss 3316 class class class wbr 4280

cfv 5406 (class class class)co 6080

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

cpnf 9403

clt 9406

cle 9407

cmin 9583

cneg 9584

cdiv 9981

cn 10310

c2 10359

cuz 10849

crp 10979

cioo 11288

cico 11290

cicc 11291

cfz 11424

cfl 11624

cabs 12707

csu 13147

clog 21891 Λcvma 22314 ψcchp 22315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ioc 11293 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-mod 11693 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-shft 12540 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-sum 13148 df-ef 13336 df-sin 13338 df-cos 13339 df-pi 13341 df-dvds 13519 df-gcd 13674 df-prm 13747 df-pc 13887 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-submnd 15448 df-mulg 15528 df-cntz 15815 df-cmn 16259 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-fbas 17658 df-fg 17659 df-cnfld 17663 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cld 18465 df-ntr 18466 df-cls 18467 df-nei 18544 df-lp 18582 df-perf 18583 df-cn 18673 df-cnp 18674 df-haus 18761 df-tx 18977 df-hmeo 19170 df-fil 19261 df-fm 19353 df-flim 19354 df-flf 19355 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296 df-limc 21183 df-dv 21184 df-log 21893 df-vma 22320 df-chp 22321

This theorem is referenced by: chpdifbndlem2 22688

W3C validator