chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 22934

Description: Lemma for chpdifbnd 22936. (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 11467	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3461	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11137	. . . . . . . . . . 11
7	6, 4	remulcld 9524	. . . . . . . . . 10
8		elicc2 11470	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1000	. . . . . . 7
12		chpcl 22594	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 22594	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9886	. . . . 5 ψ ψ
17		0red 9497	. . . . . . . 8
18		1re 9495	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 9972	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11465	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 459	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9642	. . . . . . 7
26	4, 25	elrpd 11135	. . . . . 6
27	26	relogcld 22204	. . . . 5
28	16, 27	remulcld 9524	. . . 4 ψ ψ
29		2re 10501	. . . . . . 7
30	11, 4	resubcld 9886	. . . . . . 7
31		remulcl 9477	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 663	. . . . . 6
33	32, 27	remulcld 9524	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11137	. . . . . . 7
36	11, 4	readdcld 9523	. . . . . . 7
37	35, 36	remulcld 9524	. . . . . 6
38	5	relogcld 22204	. . . . . . . 8
39		remulcl 9477	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 663	. . . . . . 7
41	40, 11	remulcld 9524	. . . . . 6
42	37, 41	readdcld 9523	. . . . 5
43	33, 42	readdcld 9523	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9652	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9524	. . . . . . . 8
48		remulcl 9477	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 663	. . . . . . . . 9
50	49, 38	remulcld 9524	. . . . . . . 8
51	47, 50	readdcld 9523	. . . . . . 7
52	44, 51	syl5eqel 2546	. . . . . 6
53	52, 4	remulcld 9524	. . . . 5
54	33, 53	readdcld 9523	. . . 4
55	13, 27	remulcld 9524	. . . . . . 7 ψ
56		fzfid 11911	. . . . . . . 8
57	10	simp2d 1001	. . . . . . . . . . . 12
58		flword2 11777	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1219	. . . . . . . . . . 11
60		fzss2 11614	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3463	. . . . . . . . 9 $/\$
63		elfznn 11594	. . . . . . . . . . . 12
64	63	adantl 466	. . . . . . . . . . 11 $/\$
65		vmacl 22588	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10467	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 477	. . . . . . . . . . 11 $/\$
69		chpcl 22594	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9524	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 470	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13328	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9523	. . . . . 6 ψ Λ ψ
75		remulcl 9477	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 663	. . . . . . . 8
77	76, 35	resubcld 9886	. . . . . . 7
78	77, 4	remulcld 9524	. . . . . 6
79	5, 26	rpmulcld 11153	. . . . . . . . . 10
80	79	relogcld 22204	. . . . . . . . 9
81		remulcl 9477	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 663	. . . . . . . 8
83	35, 82	readdcld 9523	. . . . . . 7
84	83, 11	remulcld 9524	. . . . . 6
85	15, 27	remulcld 9524	. . . . . . 7 ψ
86	85, 73	readdcld 9523	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9641	. . . . . . . . . . 11
88	11, 87	elrpd 11135	. . . . . . . . . 10
89	88	relogcld 22204	. . . . . . . . 9
90	13, 89	remulcld 9524	. . . . . . . 8 ψ
91		fzfid 11911	. . . . . . . . 9
92		nndivre 10467	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 477	. . . . . . . . . . 11 $/\$
94		chpcl 22594	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9524	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13328	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9523	. . . . . . 7 ψ Λ ψ
99		chpge0 22596	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 22208	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10383	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13328	. . . . . . . . 9 Λ ψ
105		vmage0 22591	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 22596	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10026	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13376	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 465	. . . . . . . . . . . . 13 $/\$
112	11	adantr 465	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11136	. . . . . . . . . . . . 13 $/\$
114	57	adantr 465	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11191	. . . . . . . . . . . 12 $/\$
116		chpwordi 22627	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1219	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10383	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13379	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9638	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10067	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11164	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9477	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 663	. . . . . . . . . 10
125	35, 124	readdcld 9523	. . . . . . . . 9
126	122, 124	resubcld 9886	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9522	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13039	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13018	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9632	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9638	. . . . . . . . . . . . 13
132		elicopnf 11501	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 664	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5798	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5798	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6217	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5798	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6207	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6217	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13290	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5798	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6215	. . . . . . . . . . . . . . . . . . . 20
146		simpl 457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6214	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6215	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13301	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2507	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6217	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6217	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6215	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6217	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5802	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4409	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3173	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9638	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10046	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1002	. . . . . . . . . . . 12
165	88, 79	logled 22208	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10523	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 455	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1219	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10064	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9638	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11187	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9638	. . . . . 6 ψ Λ ψ
178		elicopnf 11501	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 664	. . . . . . . . . 10
181		fveq2 5798	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5798	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6217	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5798	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6215	. . . . . . . . . . . . . . . . . 18
186		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6214	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5802	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6215	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13301	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2507	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6217	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6217	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6215	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6217	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5802	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4409	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3173	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11164	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13038	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 459	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11182	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10068	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9522	. . . . . . 7 ψ
209	85	recnd 9522	. . . . . . 7 ψ
210	73	recnd 9522	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9867	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9522	. . . . . . 7 ψ
213	15	recnd 9522	. . . . . . 7 ψ
214	27	recnd 9522	. . . . . . 7
215	212, 213, 214	subdird 9911	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2498	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9524	. . . . . . . 8
218	217	recnd 9522	. . . . . . 7
219	35, 40	readdcld 9523	. . . . . . . . 9
220	219, 11	remulcld 9524	. . . . . . . 8
221	220	recnd 9522	. . . . . . 7
222	76, 4	remulcld 9524	. . . . . . . 8
223	222	recnd 9522	. . . . . . 7
224	35, 4	remulcld 9524	. . . . . . . . 9
225	224	recnd 9522	. . . . . . . 8
226	225	negcld 9816	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9876	. . . . . 6
228	5, 26	relogmuld 22206	. . . . . . . . . . . . . 14
229	38	recnd 9522	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9681	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2495	. . . . . . . . . . . . 13
232	231	oveq2d 6215	. . . . . . . . . . . 12
233		2cnd 10504	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9520	. . . . . . . . . . . 12
235	232, 234	eqtrd 2495	. . . . . . . . . . 11
236	235	oveq2d 6215	. . . . . . . . . 10
237	35	recnd 9522	. . . . . . . . . . 11
238	76	recnd 9522	. . . . . . . . . . 11
239	40	recnd 9522	. . . . . . . . . . 11
240	237, 238, 239	add12d 9701	. . . . . . . . . 10
241	236, 240	eqtrd 2495	. . . . . . . . 9
242	241	oveq1d 6214	. . . . . . . 8
243	219	recnd 9522	. . . . . . . . 9
244	11	recnd 9522	. . . . . . . . 9
245	238, 243, 244	adddird 9521	. . . . . . . 8
246	242, 245	eqtrd 2495	. . . . . . 7
247	4	recnd 9522	. . . . . . . . 9
248	238, 237, 247	subdird 9911	. . . . . . . 8
249	223, 225	negsubd 9835	. . . . . . . 8
250	248, 249	eqtr4d 2498	. . . . . . 7
251	246, 250	oveq12d 6217	. . . . . 6
252	30	recnd 9522	. . . . . . . . 9
253	233, 252, 214	mul32d 9689	. . . . . . . 8
254	238, 244, 247	subdid 9910	. . . . . . . 8
255	253, 254	eqtrd 2495	. . . . . . 7
256	35, 11	remulcld 9524	. . . . . . . . . . 11
257	256	recnd 9522	. . . . . . . . . 10
258	41	recnd 9522	. . . . . . . . . 10
259	257, 225, 258	add32d 9702	. . . . . . . . 9
260	237, 244, 247	adddid 9520	. . . . . . . . . 10
261	260	oveq1d 6214	. . . . . . . . 9
262	237, 239, 244	adddird 9521	. . . . . . . . . 10
263	262	oveq1d 6214	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2505	. . . . . . . 8
265	221, 225	subnegd 9836	. . . . . . . 8
266	264, 265	eqtr4d 2498	. . . . . . 7
267	255, 266	oveq12d 6217	. . . . . 6
268	227, 251, 267	3eqtr4d 2505	. . . . 5
269	207, 216, 268	3brtr3d 4428	. . . 4 ψ ψ
270	47, 4	remulcld 9524	. . . . . . 7
271	50, 4	remulcld 9524	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10063	. . . . . . . . . 10
273	6	recnd 9522	. . . . . . . . . . . 12
274	19	recnd 9522	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9521	. . . . . . . . . . 11
276	247	mulid2d 9514	. . . . . . . . . . . 12
277	276	oveq2d 6215	. . . . . . . . . . 11
278	275, 277	eqtrd 2495	. . . . . . . . . 10
279	272, 278	breqtrrd 4425	. . . . . . . . 9
280	46, 4	remulcld 9524	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11177	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9522	. . . . . . . . 9
284	237, 283, 247	mulassd 9519	. . . . . . . 8
285	282, 284	breqtrrd 4425	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10522	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 22166	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11105	. . . . . . . . . . . . 13
292		logleb 22184	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 663	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4433	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10026	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10383	. . . . . . . 8
298	49	recnd 9522	. . . . . . . . . 10
299	298, 229, 247	mulassd 9519	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9691	. . . . . . . . 9
301	299, 300	eqtrd 2495	. . . . . . . 8
302	297, 301	breqtrrd 4425	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10067	. . . . . 6
304	44	oveq1i 6209	. . . . . . 7
305	47	recnd 9522	. . . . . . . 8
306	50	recnd 9522	. . . . . . . 8
307	305, 306, 247	adddird 9521	. . . . . . 7
308	304, 307	syl5eq 2507	. . . . . 6
309	303, 308	breqtrrd 4425	. . . . 5
310	42, 53, 33, 309	leadd2dd 10064	. . . 4
311	28, 43, 54, 269, 310	letrd 9638	. . 3 ψ ψ
312	32	recnd 9522	. . . . 5
313	4, 24	rplogcld 22210	. . . . . . . 8
314	4, 313	rerpdivcld 11164	. . . . . . 7
315	52, 314	remulcld 9524	. . . . . 6
316	315	recnd 9522	. . . . 5
317	312, 316, 214	adddird 9521	. . . 4
318	52	recnd 9522	. . . . . . 7
319	314	recnd 9522	. . . . . . 7
320	318, 319, 214	mulassd 9519	. . . . . 6
321	313	rpne0d 11142	. . . . . . . 8
322	247, 214, 321	divcan1d 10218	. . . . . . 7
323	322	oveq2d 6215	. . . . . 6
324	320, 323	eqtrd 2495	. . . . 5
325	324	oveq2d 6215	. . . 4
326	317, 325	eqtrd 2495	. . 3
327	311, 326	breqtrrd 4425	. 2 ψ ψ
328	32, 315	readdcld 9523	. . 3
329	16, 328, 313	lemul1d 11176	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wral 2798

wss 3435 class class class wbr 4399

cfv 5525 (class class class)co 6199

cr 9391

cc0 9392

c1 9393

caddc 9395

cmul 9397

cpnf 9525

clt 9528

cle 9529

cmin 9705

cneg 9706

cdiv 10103

cn 10432

c2 10481

cuz 10971

crp 11101

cioo 11410

cico 11412

cicc 11413

cfz 11553

cfl 11756

cabs 12840

csu 13280

clog 22138 Λcvma 22561 ψcchp 22562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470 ax-addf 9471 ax-mulf 9472

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-iin 4281 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-of 6429 df-om 6586 df-1st 6686 df-2nd 6687 df-supp 6800 df-recs 6941 df-rdg 6975 df-1o 7029 df-2o 7030 df-oadd 7033 df-er 7210 df-map 7325 df-pm 7326 df-ixp 7373 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-fsupp 7731 df-fi 7771 df-sup 7801 df-oi 7834 df-card 8219 df-cda 8447 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-div 10104 df-nn 10433 df-2 10490 df-3 10491 df-4 10492 df-5 10493 df-6 10494 df-7 10495 df-8 10496 df-9 10497 df-10 10498 df-n0 10690 df-z 10757 df-dec 10866 df-uz 10972 df-q 11064 df-rp 11102 df-xneg 11199 df-xadd 11200 df-xmul 11201 df-ioo 11414 df-ioc 11415 df-ico 11416 df-icc 11417 df-fz 11554 df-fzo 11665 df-fl 11758 df-mod 11825 df-seq 11923 df-exp 11982 df-fac 12168 df-bc 12195 df-hash 12220 df-shft 12673 df-cj 12705 df-re 12706 df-im 12707 df-sqr 12841 df-abs 12842 df-limsup 13066 df-clim 13083 df-rlim 13084 df-sum 13281 df-ef 13470 df-sin 13472 df-cos 13473 df-pi 13475 df-dvds 13653 df-gcd 13808 df-prm 13881 df-pc 14021 df-struct 14293 df-ndx 14294 df-slot 14295 df-base 14296 df-sets 14297 df-ress 14298 df-plusg 14369 df-mulr 14370 df-starv 14371 df-sca 14372 df-vsca 14373 df-ip 14374 df-tset 14375 df-ple 14376 df-ds 14378 df-unif 14379 df-hom 14380 df-cco 14381 df-rest 14479 df-topn 14480 df-0g 14498 df-gsum 14499 df-topgen 14500 df-pt 14501 df-prds 14504 df-xrs 14558 df-qtop 14563 df-imas 14564 df-xps 14566 df-mre 14642 df-mrc 14643 df-acs 14645 df-mnd 15533 df-submnd 15583 df-mulg 15666 df-cntz 15953 df-cmn 16399 df-psmet 17933 df-xmet 17934 df-met 17935 df-bl 17936 df-mopn 17937 df-fbas 17938 df-fg 17939 df-cnfld 17943 df-top 18634 df-bases 18636 df-topon 18637 df-topsp 18638 df-cld 18754 df-ntr 18755 df-cls 18756 df-nei 18833 df-lp 18871 df-perf 18872 df-cn 18962 df-cnp 18963 df-haus 19050 df-tx 19266 df-hmeo 19459 df-fil 19550 df-fm 19642 df-flim 19643 df-flf 19644 df-xms 20026 df-ms 20027 df-tms 20028 df-cncf 20585 df-limc 21473 df-dv 21474 df-log 22140 df-vma 22567 df-chp 22568

This theorem is referenced by: chpdifbndlem2 22935

W3C validator