chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 22782

Description: Lemma for chpdifbnd 22784. (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 11349	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3349	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11019	. . . . . . . . . . 11
7	6, 4	remulcld 9406	. . . . . . . . . 10
8		elicc2 11352	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1000	. . . . . . 7
12		chpcl 22442	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 22442	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9768	. . . . 5 ψ ψ
17		0red 9379	. . . . . . . 8
18		1re 9377	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 9854	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11347	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 459	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9524	. . . . . . 7
26	4, 25	elrpd 11017	. . . . . 6
27	26	relogcld 22052	. . . . 5
28	16, 27	remulcld 9406	. . . 4 ψ ψ
29		2re 10383	. . . . . . 7
30	11, 4	resubcld 9768	. . . . . . 7
31		remulcl 9359	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 663	. . . . . 6
33	32, 27	remulcld 9406	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11019	. . . . . . 7
36	11, 4	readdcld 9405	. . . . . . 7
37	35, 36	remulcld 9406	. . . . . 6
38	5	relogcld 22052	. . . . . . . 8
39		remulcl 9359	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 663	. . . . . . 7
41	40, 11	remulcld 9406	. . . . . 6
42	37, 41	readdcld 9405	. . . . 5
43	33, 42	readdcld 9405	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9534	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9406	. . . . . . . 8
48		remulcl 9359	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 663	. . . . . . . . 9
50	49, 38	remulcld 9406	. . . . . . . 8
51	47, 50	readdcld 9405	. . . . . . 7
52	44, 51	syl5eqel 2522	. . . . . 6
53	52, 4	remulcld 9406	. . . . 5
54	33, 53	readdcld 9405	. . . 4
55	13, 27	remulcld 9406	. . . . . . 7 ψ
56		fzfid 11787	. . . . . . . 8
57	10	simp2d 1001	. . . . . . . . . . . 12
58		flword2 11653	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1218	. . . . . . . . . . 11
60		fzss2 11490	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3351	. . . . . . . . 9 $/\$
63		elfznn 11470	. . . . . . . . . . . 12
64	63	adantl 466	. . . . . . . . . . 11 $/\$
65		vmacl 22436	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10349	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 477	. . . . . . . . . . 11 $/\$
69		chpcl 22442	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9406	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 470	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13203	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9405	. . . . . 6 ψ Λ ψ
75		remulcl 9359	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 663	. . . . . . . 8
77	76, 35	resubcld 9768	. . . . . . 7
78	77, 4	remulcld 9406	. . . . . 6
79	5, 26	rpmulcld 11035	. . . . . . . . . 10
80	79	relogcld 22052	. . . . . . . . 9
81		remulcl 9359	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 663	. . . . . . . 8
83	35, 82	readdcld 9405	. . . . . . 7
84	83, 11	remulcld 9406	. . . . . 6
85	15, 27	remulcld 9406	. . . . . . 7 ψ
86	85, 73	readdcld 9405	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9523	. . . . . . . . . . 11
88	11, 87	elrpd 11017	. . . . . . . . . 10
89	88	relogcld 22052	. . . . . . . . 9
90	13, 89	remulcld 9406	. . . . . . . 8 ψ
91		fzfid 11787	. . . . . . . . 9
92		nndivre 10349	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 477	. . . . . . . . . . 11 $/\$
94		chpcl 22442	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9406	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13203	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9405	. . . . . . 7 ψ Λ ψ
99		chpge0 22444	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 22056	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10265	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13203	. . . . . . . . 9 Λ ψ
105		vmage0 22439	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 22444	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 9908	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13251	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 465	. . . . . . . . . . . . 13 $/\$
112	11	adantr 465	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11018	. . . . . . . . . . . . 13 $/\$
114	57	adantr 465	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11073	. . . . . . . . . . . 12 $/\$
116		chpwordi 22475	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1218	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10265	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13254	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9520	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 9949	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11046	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9359	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 663	. . . . . . . . . 10
125	35, 124	readdcld 9405	. . . . . . . . 9
126	122, 124	resubcld 9768	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9404	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 12914	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 12893	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9514	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9520	. . . . . . . . . . . . 13
132		elicopnf 11377	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 664	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5686	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5686	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6104	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5686	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6094	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6104	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13165	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5686	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6102	. . . . . . . . . . . . . . . . . . . 20
146		simpl 457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6102	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13176	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2482	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6104	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6104	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6102	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6104	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5690	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4297	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3064	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9520	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 9928	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1002	. . . . . . . . . . . 12
165	88, 79	logled 22056	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10405	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 455	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10174	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1218	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 9946	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9520	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11069	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9520	. . . . . 6 ψ Λ ψ
178		elicopnf 11377	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 664	. . . . . . . . . 10
181		fveq2 5686	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5686	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6104	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5686	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6102	. . . . . . . . . . . . . . . . . 18
186		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6101	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5690	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6102	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13176	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2482	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6104	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6104	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6102	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6104	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5690	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4297	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3064	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11046	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 12913	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 459	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11064	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 9950	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9404	. . . . . . 7 ψ
209	85	recnd 9404	. . . . . . 7 ψ
210	73	recnd 9404	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9749	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9404	. . . . . . 7 ψ
213	15	recnd 9404	. . . . . . 7 ψ
214	27	recnd 9404	. . . . . . 7
215	212, 213, 214	subdird 9793	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2473	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9406	. . . . . . . 8
218	217	recnd 9404	. . . . . . 7
219	35, 40	readdcld 9405	. . . . . . . . 9
220	219, 11	remulcld 9406	. . . . . . . 8
221	220	recnd 9404	. . . . . . 7
222	76, 4	remulcld 9406	. . . . . . . 8
223	222	recnd 9404	. . . . . . 7
224	35, 4	remulcld 9406	. . . . . . . . 9
225	224	recnd 9404	. . . . . . . 8
226	225	negcld 9698	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9758	. . . . . 6
228	5, 26	relogmuld 22054	. . . . . . . . . . . . . 14
229	38	recnd 9404	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9563	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2470	. . . . . . . . . . . . 13
232	231	oveq2d 6102	. . . . . . . . . . . 12
233		2cnd 10386	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9402	. . . . . . . . . . . 12
235	232, 234	eqtrd 2470	. . . . . . . . . . 11
236	235	oveq2d 6102	. . . . . . . . . 10
237	35	recnd 9404	. . . . . . . . . . 11
238	76	recnd 9404	. . . . . . . . . . 11
239	40	recnd 9404	. . . . . . . . . . 11
240	237, 238, 239	add12d 9583	. . . . . . . . . 10
241	236, 240	eqtrd 2470	. . . . . . . . 9
242	241	oveq1d 6101	. . . . . . . 8
243	219	recnd 9404	. . . . . . . . 9
244	11	recnd 9404	. . . . . . . . 9
245	238, 243, 244	adddird 9403	. . . . . . . 8
246	242, 245	eqtrd 2470	. . . . . . 7
247	4	recnd 9404	. . . . . . . . 9
248	238, 237, 247	subdird 9793	. . . . . . . 8
249	223, 225	negsubd 9717	. . . . . . . 8
250	248, 249	eqtr4d 2473	. . . . . . 7
251	246, 250	oveq12d 6104	. . . . . 6
252	30	recnd 9404	. . . . . . . . 9
253	233, 252, 214	mul32d 9571	. . . . . . . 8
254	238, 244, 247	subdid 9792	. . . . . . . 8
255	253, 254	eqtrd 2470	. . . . . . 7
256	35, 11	remulcld 9406	. . . . . . . . . . 11
257	256	recnd 9404	. . . . . . . . . 10
258	41	recnd 9404	. . . . . . . . . 10
259	257, 225, 258	add32d 9584	. . . . . . . . 9
260	237, 244, 247	adddid 9402	. . . . . . . . . 10
261	260	oveq1d 6101	. . . . . . . . 9
262	237, 239, 244	adddird 9403	. . . . . . . . . 10
263	262	oveq1d 6101	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2480	. . . . . . . 8
265	221, 225	subnegd 9718	. . . . . . . 8
266	264, 265	eqtr4d 2473	. . . . . . 7
267	255, 266	oveq12d 6104	. . . . . 6
268	227, 251, 267	3eqtr4d 2480	. . . . 5
269	207, 216, 268	3brtr3d 4316	. . . 4 ψ ψ
270	47, 4	remulcld 9406	. . . . . . 7
271	50, 4	remulcld 9406	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 9945	. . . . . . . . . 10
273	6	recnd 9404	. . . . . . . . . . . 12
274	19	recnd 9404	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9403	. . . . . . . . . . 11
276	247	mulid2d 9396	. . . . . . . . . . . 12
277	276	oveq2d 6102	. . . . . . . . . . 11
278	275, 277	eqtrd 2470	. . . . . . . . . 10
279	272, 278	breqtrrd 4313	. . . . . . . . 9
280	46, 4	remulcld 9406	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11059	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9404	. . . . . . . . 9
284	237, 283, 247	mulassd 9401	. . . . . . . 8
285	282, 284	breqtrrd 4313	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10404	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 22014	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 10987	. . . . . . . . . . . . 13
292		logleb 22032	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 663	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4321	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 9908	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10265	. . . . . . . 8
298	49	recnd 9404	. . . . . . . . . 10
299	298, 229, 247	mulassd 9401	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9573	. . . . . . . . 9
301	299, 300	eqtrd 2470	. . . . . . . 8
302	297, 301	breqtrrd 4313	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 9949	. . . . . 6
304	44	oveq1i 6096	. . . . . . 7
305	47	recnd 9404	. . . . . . . 8
306	50	recnd 9404	. . . . . . . 8
307	305, 306, 247	adddird 9403	. . . . . . 7
308	304, 307	syl5eq 2482	. . . . . 6
309	303, 308	breqtrrd 4313	. . . . 5
310	42, 53, 33, 309	leadd2dd 9946	. . . 4
311	28, 43, 54, 269, 310	letrd 9520	. . 3 ψ ψ
312	32	recnd 9404	. . . . 5
313	4, 24	rplogcld 22058	. . . . . . . 8
314	4, 313	rerpdivcld 11046	. . . . . . 7
315	52, 314	remulcld 9406	. . . . . 6
316	315	recnd 9404	. . . . 5
317	312, 316, 214	adddird 9403	. . . 4
318	52	recnd 9404	. . . . . . 7
319	314	recnd 9404	. . . . . . 7
320	318, 319, 214	mulassd 9401	. . . . . 6
321	313	rpne0d 11024	. . . . . . . 8
322	247, 214, 321	divcan1d 10100	. . . . . . 7
323	322	oveq2d 6102	. . . . . 6
324	320, 323	eqtrd 2470	. . . . 5
325	324	oveq2d 6102	. . . 4
326	317, 325	eqtrd 2470	. . 3
327	311, 326	breqtrrd 4313	. 2 ψ ψ
328	32, 315	readdcld 9405	. . 3
329	16, 328, 313	lemul1d 11058	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2710

wss 3323 class class class wbr 4287

cfv 5413 (class class class)co 6086

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

cpnf 9407

clt 9410

cle 9411

cmin 9587

cneg 9588

cdiv 9985

cn 10314

c2 10363

cuz 10853

crp 10983

cioo 11292

cico 11294

cicc 11295

cfz 11429

cfl 11632

cabs 12715

csu 13155

clog 21986 Λcvma 22409 ψcchp 22410

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-ef 13345 df-sin 13347 df-cos 13348 df-pi 13350 df-dvds 13528 df-gcd 13683 df-prm 13756 df-pc 13896 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15539 df-cntz 15826 df-cmn 16270 df-psmet 17789 df-xmet 17790 df-met 17791 df-bl 17792 df-mopn 17793 df-fbas 17794 df-fg 17795 df-cnfld 17799 df-top 18483 df-bases 18485 df-topon 18486 df-topsp 18487 df-cld 18603 df-ntr 18604 df-cls 18605 df-nei 18682 df-lp 18720 df-perf 18721 df-cn 18811 df-cnp 18812 df-haus 18899 df-tx 19115 df-hmeo 19308 df-fil 19399 df-fm 19491 df-flim 19492 df-flf 19493 df-xms 19875 df-ms 19876 df-tms 19877 df-cncf 20434 df-limc 21321 df-dv 21322 df-log 21988 df-vma 22415 df-chp 22416

This theorem is referenced by: chpdifbndlem2 22783

W3C validator