chpdifbndlem1 - Metamath Proof Explorer

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

Theorem chpdifbndlem1 23494

Description: Lemma for chpdifbnd 23496. (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 11586	. . . . . . . . . . 11
3		chpdifbnd.x	. . . . . . . . . . 11
4	2, 3	sseldi 3502	. . . . . . . . . 10
5		chpdifbnd.a	. . . . . . . . . . . 12
6	5	rpred 11256	. . . . . . . . . . 11
7	6, 4	remulcld 9624	. . . . . . . . . 10
8		elicc2 11589	. . . . . . . . . 10 $/\$ $/\$ $/\$
9	4, 7, 8	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
10	1, 9	mpbid 210	. . . . . . . 8 $/\$ $/\$
11	10	simp1d 1008	. . . . . . 7
12		chpcl 23154	. . . . . . 7 ψ
13	11, 12	syl 16	. . . . . 6 ψ
14		chpcl 23154	. . . . . . 7 ψ
15	4, 14	syl 16	. . . . . 6 ψ
16	13, 15	resubcld 9987	. . . . 5 ψ ψ
17		0red 9597	. . . . . . . 8
18		1re 9595	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8
20		0lt1 10075	. . . . . . . . 9
21	20	a1i 11	. . . . . . . 8
22		eliooord 11584	. . . . . . . . . 10 $/\$
23	3, 22	syl 16	. . . . . . . . 9 $/\$
24	23	simpld 459	. . . . . . . 8
25	17, 19, 4, 21, 24	lttrd 9742	. . . . . . 7
26	4, 25	elrpd 11254	. . . . . 6
27	26	relogcld 22764	. . . . 5
28	16, 27	remulcld 9624	. . . 4 ψ ψ
29		2re 10605	. . . . . . 7
30	11, 4	resubcld 9987	. . . . . . 7
31		remulcl 9577	. . . . . . 7 $/\$
32	29, 30, 31	sylancr 663	. . . . . 6
33	32, 27	remulcld 9624	. . . . 5
34		chpdifbnd.b	. . . . . . . 8
35	34	rpred 11256	. . . . . . 7
36	11, 4	readdcld 9623	. . . . . . 7
37	35, 36	remulcld 9624	. . . . . 6
38	5	relogcld 22764	. . . . . . . 8
39		remulcl 9577	. . . . . . . 8 $/\$
40	29, 38, 39	sylancr 663	. . . . . . 7
41	40, 11	remulcld 9624	. . . . . 6
42	37, 41	readdcld 9623	. . . . 5
43	33, 42	readdcld 9623	. . . 4
44		chpdifbnd.c	. . . . . . 7
45		peano2re 9752	. . . . . . . . . 10
46	6, 45	syl 16	. . . . . . . . 9
47	35, 46	remulcld 9624	. . . . . . . 8
48		remulcl 9577	. . . . . . . . . 10 $/\$
49	29, 6, 48	sylancr 663	. . . . . . . . 9
50	49, 38	remulcld 9624	. . . . . . . 8
51	47, 50	readdcld 9623	. . . . . . 7
52	44, 51	syl5eqel 2559	. . . . . 6
53	52, 4	remulcld 9624	. . . . 5
54	33, 53	readdcld 9623	. . . 4
55	13, 27	remulcld 9624	. . . . . . 7 ψ
56		fzfid 12051	. . . . . . . 8
57	10	simp2d 1009	. . . . . . . . . . . 12
58		flword2 11917	. . . . . . . . . . . 12 $/\$ $/\$
59	4, 11, 57, 58	syl3anc 1228	. . . . . . . . . . 11
60		fzss2 11723	. . . . . . . . . . 11
61	59, 60	syl 16	. . . . . . . . . 10
62	61	sselda 3504	. . . . . . . . 9 $/\$
63		elfznn 11714	. . . . . . . . . . . 12
64	63	adantl 466	. . . . . . . . . . 11 $/\$
65		vmacl 23148	. . . . . . . . . . 11 Λ
66	64, 65	syl 16	. . . . . . . . . 10 $/\$ Λ
67		nndivre 10571	. . . . . . . . . . . 12 $/\$
68	4, 63, 67	syl2an 477	. . . . . . . . . . 11 $/\$
69		chpcl 23154	. . . . . . . . . . 11 ψ
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ ψ
71	66, 70	remulcld 9624	. . . . . . . . 9 $/\$ Λ ψ
72	62, 71	syldan 470	. . . . . . . 8 $/\$ Λ ψ
73	56, 72	fsumrecl 13519	. . . . . . 7 Λ ψ
74	55, 73	readdcld 9623	. . . . . 6 ψ Λ ψ
75		remulcl 9577	. . . . . . . . 9 $/\$
76	29, 27, 75	sylancr 663	. . . . . . . 8
77	76, 35	resubcld 9987	. . . . . . 7
78	77, 4	remulcld 9624	. . . . . 6
79	5, 26	rpmulcld 11272	. . . . . . . . . 10
80	79	relogcld 22764	. . . . . . . . 9
81		remulcl 9577	. . . . . . . . 9 $/\$
82	29, 80, 81	sylancr 663	. . . . . . . 8
83	35, 82	readdcld 9623	. . . . . . 7
84	83, 11	remulcld 9624	. . . . . 6
85	15, 27	remulcld 9624	. . . . . . 7 ψ
86	85, 73	readdcld 9623	. . . . . 6 ψ Λ ψ
87	17, 4, 11, 25, 57	ltletrd 9741	. . . . . . . . . . 11
88	11, 87	elrpd 11254	. . . . . . . . . 10
89	88	relogcld 22764	. . . . . . . . 9
90	13, 89	remulcld 9624	. . . . . . . 8 ψ
91		fzfid 12051	. . . . . . . . 9
92		nndivre 10571	. . . . . . . . . . . 12 $/\$
93	11, 63, 92	syl2an 477	. . . . . . . . . . 11 $/\$
94		chpcl 23154	. . . . . . . . . . 11 ψ
95	93, 94	syl 16	. . . . . . . . . 10 $/\$ ψ
96	66, 95	remulcld 9624	. . . . . . . . 9 $/\$ Λ ψ
97	91, 96	fsumrecl 13519	. . . . . . . 8 Λ ψ
98	90, 97	readdcld 9623	. . . . . . 7 ψ Λ ψ
99		chpge0 23156	. . . . . . . . . 10 ψ
100	11, 99	syl 16	. . . . . . . . 9 ψ
101	26, 88	logled 22768	. . . . . . . . . 10
102	57, 101	mpbid 210	. . . . . . . . 9
103	27, 89, 13, 100, 102	lemul2ad 10486	. . . . . . . 8 ψ ψ
104	91, 71	fsumrecl 13519	. . . . . . . . 9 Λ ψ
105		vmage0 23151	. . . . . . . . . . . 12 Λ
106	64, 105	syl 16	. . . . . . . . . . 11 $/\$ Λ
107		chpge0 23156	. . . . . . . . . . . 12 ψ
108	68, 107	syl 16	. . . . . . . . . . 11 $/\$ ψ
109	66, 70, 106, 108	mulge0d 10129	. . . . . . . . . 10 $/\$ Λ ψ
110	91, 71, 109, 61	fsumless 13573	. . . . . . . . 9 Λ ψ Λ ψ
111	4	adantr 465	. . . . . . . . . . . . 13 $/\$
112	11	adantr 465	. . . . . . . . . . . . 13 $/\$
113	64	nnrpd 11255	. . . . . . . . . . . . 13 $/\$
114	57	adantr 465	. . . . . . . . . . . . 13 $/\$
115	111, 112, 113, 114	lediv1dd 11310	. . . . . . . . . . . 12 $/\$
116		chpwordi 23187	. . . . . . . . . . . 12 $/\$ $/\$ ψ ψ
117	68, 93, 115, 116	syl3anc 1228	. . . . . . . . . . 11 $/\$ ψ ψ
118	70, 95, 66, 106, 117	lemul2ad 10486	. . . . . . . . . 10 $/\$ Λ ψ Λ ψ
119	91, 71, 96, 118	fsumle 13576	. . . . . . . . 9 Λ ψ Λ ψ
120	73, 104, 97, 110, 119	letrd 9738	. . . . . . . 8 Λ ψ Λ ψ
121	55, 73, 90, 97, 103, 120	le2addd 10170	. . . . . . 7 ψ Λ ψ ψ Λ ψ
122	98, 88	rerpdivcld 11283	. . . . . . . . 9 ψ Λ ψ
123		remulcl 9577	. . . . . . . . . . 11 $/\$
124	29, 89, 123	sylancr 663	. . . . . . . . . 10
125	35, 124	readdcld 9623	. . . . . . . . 9
126	122, 124	resubcld 9987	. . . . . . . . . . 11 ψ Λ ψ
127	126	recnd 9622	. . . . . . . . . . . 12 ψ Λ ψ
128	127	abscld 13230	. . . . . . . . . . 11 ψ Λ ψ
129	126	leabsd 13209	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
130	19, 4, 24	ltled 9732	. . . . . . . . . . . . . 14
131	19, 4, 11, 130, 57	letrd 9738	. . . . . . . . . . . . 13
132		elicopnf 11620	. . . . . . . . . . . . . 14 $/\$
133	18, 132	ax-mp 5	. . . . . . . . . . . . 13 $/\$
134	11, 131, 133	sylanbrc 664	. . . . . . . . . . . 12
135		chpdifbnd.2	. . . . . . . . . . . 12 ψ Λ ψ
136		fveq2 5866	. . . . . . . . . . . . . . . . . . 19 ψ ψ
137		fveq2 5866	. . . . . . . . . . . . . . . . . . 19
138	136, 137	oveq12d 6302	. . . . . . . . . . . . . . . . . 18 ψ ψ
139		fveq2 5866	. . . . . . . . . . . . . . . . . . . . 21 Λ Λ
140		oveq2 6292	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq2d 5870	. . . . . . . . . . . . . . . . . . . . 21 ψ ψ
142	139, 141	oveq12d 6302	. . . . . . . . . . . . . . . . . . . 20 Λ ψ Λ ψ
143	142	cbvsumv 13481	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
144		fveq2 5866	. . . . . . . . . . . . . . . . . . . . 21
145	144	oveq2d 6300	. . . . . . . . . . . . . . . . . . . 20
146		simpl 457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	146	oveq1d 6299	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	fveq2d 5870	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ψ ψ
149	148	oveq2d 6300	. . . . . . . . . . . . . . . . . . . 20 $/\$ Λ ψ Λ ψ
150	145, 149	sumeq12rdv 13492	. . . . . . . . . . . . . . . . . . 19 Λ ψ Λ ψ
151	143, 150	syl5eq 2520	. . . . . . . . . . . . . . . . . 18 Λ ψ Λ ψ
152	138, 151	oveq12d 6302	. . . . . . . . . . . . . . . . 17 ψ Λ ψ ψ Λ ψ
153		id 22	. . . . . . . . . . . . . . . . 17
154	152, 153	oveq12d 6302	. . . . . . . . . . . . . . . 16 ψ Λ ψ ψ Λ ψ
155	137	oveq2d 6300	. . . . . . . . . . . . . . . 16
156	154, 155	oveq12d 6302	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
157	156	fveq2d 5870	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
158	157	breq1d 4457	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
159	158	rspcv 3210	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
160	134, 135, 159	sylc 60	. . . . . . . . . . 11 ψ Λ ψ
161	126, 128, 35, 129, 160	letrd 9738	. . . . . . . . . 10 ψ Λ ψ
162	122, 124, 35	lesubaddd 10149	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
163	161, 162	mpbid 210	. . . . . . . . 9 ψ Λ ψ
164	10	simp3d 1010	. . . . . . . . . . . 12
165	88, 79	logled 22768	. . . . . . . . . . . 12
166	164, 165	mpbid 210	. . . . . . . . . . 11
167		2pos 10627	. . . . . . . . . . . . . 14
168	29, 167	pm3.2i 455	. . . . . . . . . . . . 13 $/\$
169	168	a1i 11	. . . . . . . . . . . 12 $/\$
170		lemul2 10395	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	89, 80, 169, 170	syl3anc 1228	. . . . . . . . . . 11
172	166, 171	mpbid 210	. . . . . . . . . 10
173	124, 82, 35, 172	leadd2dd 10167	. . . . . . . . 9
174	122, 125, 83, 163, 173	letrd 9738	. . . . . . . 8 ψ Λ ψ
175	98, 83, 88	ledivmul2d 11306	. . . . . . . 8 ψ Λ ψ ψ Λ ψ
176	174, 175	mpbid 210	. . . . . . 7 ψ Λ ψ
177	74, 98, 84, 121, 176	letrd 9738	. . . . . 6 ψ Λ ψ
178		elicopnf 11620	. . . . . . . . . . . 12 $/\$
179	18, 178	ax-mp 5	. . . . . . . . . . 11 $/\$
180	4, 130, 179	sylanbrc 664	. . . . . . . . . 10
181		fveq2 5866	. . . . . . . . . . . . . . . . 17 ψ ψ
182		fveq2 5866	. . . . . . . . . . . . . . . . 17
183	181, 182	oveq12d 6302	. . . . . . . . . . . . . . . 16 ψ ψ
184		fveq2 5866	. . . . . . . . . . . . . . . . . . 19
185	184	oveq2d 6300	. . . . . . . . . . . . . . . . . 18
186		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187	186	oveq1d 6299	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	187	fveq2d 5870	. . . . . . . . . . . . . . . . . . 19 $/\$ ψ ψ
189	188	oveq2d 6300	. . . . . . . . . . . . . . . . . 18 $/\$ Λ ψ Λ ψ
190	185, 189	sumeq12rdv 13492	. . . . . . . . . . . . . . . . 17 Λ ψ Λ ψ
191	143, 190	syl5eq 2520	. . . . . . . . . . . . . . . 16 Λ ψ Λ ψ
192	183, 191	oveq12d 6302	. . . . . . . . . . . . . . 15 ψ Λ ψ ψ Λ ψ
193		id 22	. . . . . . . . . . . . . . 15
194	192, 193	oveq12d 6302	. . . . . . . . . . . . . 14 ψ Λ ψ ψ Λ ψ
195	182	oveq2d 6300	. . . . . . . . . . . . . 14
196	194, 195	oveq12d 6302	. . . . . . . . . . . . 13 ψ Λ ψ ψ Λ ψ
197	196	fveq2d 5870	. . . . . . . . . . . 12 ψ Λ ψ ψ Λ ψ
198	197	breq1d 4457	. . . . . . . . . . 11 ψ Λ ψ ψ Λ ψ
199	198	rspcv 3210	. . . . . . . . . 10 ψ Λ ψ ψ Λ ψ
200	180, 135, 199	sylc 60	. . . . . . . . 9 ψ Λ ψ
201	86, 26	rerpdivcld 11283	. . . . . . . . . 10 ψ Λ ψ
202	201, 76, 35	absdifled 13229	. . . . . . . . 9 ψ Λ ψ ψ Λ ψ $/\$ ψ Λ ψ
203	200, 202	mpbid 210	. . . . . . . 8 ψ Λ ψ $/\$ ψ Λ ψ
204	203	simpld 459	. . . . . . 7 ψ Λ ψ
205	77, 86, 26	lemuldivd 11301	. . . . . . 7 ψ Λ ψ ψ Λ ψ
206	204, 205	mpbird 232	. . . . . 6 ψ Λ ψ
207	74, 78, 84, 86, 177, 206	le2subd 10171	. . . . 5 ψ Λ ψ ψ Λ ψ
208	55	recnd 9622	. . . . . . 7 ψ
209	85	recnd 9622	. . . . . . 7 ψ
210	73	recnd 9622	. . . . . . 7 Λ ψ
211	208, 209, 210	pnpcan2d 9968	. . . . . 6 ψ Λ ψ ψ Λ ψ ψ ψ
212	13	recnd 9622	. . . . . . 7 ψ
213	15	recnd 9622	. . . . . . 7 ψ
214	27	recnd 9622	. . . . . . 7
215	212, 213, 214	subdird 10013	. . . . . 6 ψ ψ ψ ψ
216	211, 215	eqtr4d 2511	. . . . 5 ψ Λ ψ ψ Λ ψ ψ ψ
217	76, 11	remulcld 9624	. . . . . . . 8
218	217	recnd 9622	. . . . . . 7
219	35, 40	readdcld 9623	. . . . . . . . 9
220	219, 11	remulcld 9624	. . . . . . . 8
221	220	recnd 9622	. . . . . . 7
222	76, 4	remulcld 9624	. . . . . . . 8
223	222	recnd 9622	. . . . . . 7
224	35, 4	remulcld 9624	. . . . . . . . 9
225	224	recnd 9622	. . . . . . . 8
226	225	negcld 9917	. . . . . . 7
227	218, 221, 223, 226	addsub4d 9977	. . . . . 6
228	5, 26	relogmuld 22766	. . . . . . . . . . . . . 14
229	38	recnd 9622	. . . . . . . . . . . . . . 15
230	229, 214	addcomd 9781	. . . . . . . . . . . . . 14
231	228, 230	eqtrd 2508	. . . . . . . . . . . . 13
232	231	oveq2d 6300	. . . . . . . . . . . 12
233		2cnd 10608	. . . . . . . . . . . . 13
234	233, 214, 229	adddid 9620	. . . . . . . . . . . 12
235	232, 234	eqtrd 2508	. . . . . . . . . . 11
236	235	oveq2d 6300	. . . . . . . . . 10
237	35	recnd 9622	. . . . . . . . . . 11
238	76	recnd 9622	. . . . . . . . . . 11
239	40	recnd 9622	. . . . . . . . . . 11
240	237, 238, 239	add12d 9801	. . . . . . . . . 10
241	236, 240	eqtrd 2508	. . . . . . . . 9
242	241	oveq1d 6299	. . . . . . . 8
243	219	recnd 9622	. . . . . . . . 9
244	11	recnd 9622	. . . . . . . . 9
245	238, 243, 244	adddird 9621	. . . . . . . 8
246	242, 245	eqtrd 2508	. . . . . . 7
247	4	recnd 9622	. . . . . . . . 9
248	238, 237, 247	subdird 10013	. . . . . . . 8
249	223, 225	negsubd 9936	. . . . . . . 8
250	248, 249	eqtr4d 2511	. . . . . . 7
251	246, 250	oveq12d 6302	. . . . . 6
252	30	recnd 9622	. . . . . . . . 9
253	233, 252, 214	mul32d 9789	. . . . . . . 8
254	238, 244, 247	subdid 10012	. . . . . . . 8
255	253, 254	eqtrd 2508	. . . . . . 7
256	35, 11	remulcld 9624	. . . . . . . . . . 11
257	256	recnd 9622	. . . . . . . . . 10
258	41	recnd 9622	. . . . . . . . . 10
259	257, 225, 258	add32d 9802	. . . . . . . . 9
260	237, 244, 247	adddid 9620	. . . . . . . . . 10
261	260	oveq1d 6299	. . . . . . . . 9
262	237, 239, 244	adddird 9621	. . . . . . . . . 10
263	262	oveq1d 6299	. . . . . . . . 9
264	259, 261, 263	3eqtr4d 2518	. . . . . . . 8
265	221, 225	subnegd 9937	. . . . . . . 8
266	264, 265	eqtr4d 2511	. . . . . . 7
267	255, 266	oveq12d 6302	. . . . . 6
268	227, 251, 267	3eqtr4d 2518	. . . . 5
269	207, 216, 268	3brtr3d 4476	. . . 4 ψ ψ
270	47, 4	remulcld 9624	. . . . . . 7
271	50, 4	remulcld 9624	. . . . . . 7
272	11, 7, 4, 164	leadd1dd 10166	. . . . . . . . . 10
273	6	recnd 9622	. . . . . . . . . . . 12
274	19	recnd 9622	. . . . . . . . . . . 12
275	273, 274, 247	adddird 9621	. . . . . . . . . . 11
276	247	mulid2d 9614	. . . . . . . . . . . 12
277	276	oveq2d 6300	. . . . . . . . . . 11
278	275, 277	eqtrd 2508	. . . . . . . . . 10
279	272, 278	breqtrrd 4473	. . . . . . . . 9
280	46, 4	remulcld 9624	. . . . . . . . . 10
281	36, 280, 34	lemul2d 11296	. . . . . . . . 9
282	279, 281	mpbid 210	. . . . . . . 8
283	46	recnd 9622	. . . . . . . . 9
284	237, 283, 247	mulassd 9619	. . . . . . . 8
285	282, 284	breqtrrd 4473	. . . . . . 7
286	29	a1i 11	. . . . . . . . . 10
287		0le2 10626	. . . . . . . . . . 11
288	287	a1i 11	. . . . . . . . . 10
289		log1 22726	. . . . . . . . . . 11
290		chpdifbnd.1	. . . . . . . . . . . 12
291		1rp 11224	. . . . . . . . . . . . 13
292		logleb 22744	. . . . . . . . . . . . 13 $/\$
293	291, 5, 292	sylancr 663	. . . . . . . . . . . 12
294	290, 293	mpbid 210	. . . . . . . . . . 11
295	289, 294	syl5eqbrr 4481	. . . . . . . . . 10
296	286, 38, 288, 295	mulge0d 10129	. . . . . . . . 9
297	11, 7, 40, 296, 164	lemul2ad 10486	. . . . . . . 8
298	49	recnd 9622	. . . . . . . . . 10
299	298, 229, 247	mulassd 9619	. . . . . . . . 9
300	233, 273, 229, 247	mul4d 9791	. . . . . . . . 9
301	299, 300	eqtrd 2508	. . . . . . . 8
302	297, 301	breqtrrd 4473	. . . . . . 7
303	37, 41, 270, 271, 285, 302	le2addd 10170	. . . . . 6
304	44	oveq1i 6294	. . . . . . 7
305	47	recnd 9622	. . . . . . . 8
306	50	recnd 9622	. . . . . . . 8
307	305, 306, 247	adddird 9621	. . . . . . 7
308	304, 307	syl5eq 2520	. . . . . 6
309	303, 308	breqtrrd 4473	. . . . 5
310	42, 53, 33, 309	leadd2dd 10167	. . . 4
311	28, 43, 54, 269, 310	letrd 9738	. . 3 ψ ψ
312	32	recnd 9622	. . . . 5
313	4, 24	rplogcld 22770	. . . . . . . 8
314	4, 313	rerpdivcld 11283	. . . . . . 7
315	52, 314	remulcld 9624	. . . . . 6
316	315	recnd 9622	. . . . 5
317	312, 316, 214	adddird 9621	. . . 4
318	52	recnd 9622	. . . . . . 7
319	314	recnd 9622	. . . . . . 7
320	318, 319, 214	mulassd 9619	. . . . . 6
321	313	rpne0d 11261	. . . . . . . 8
322	247, 214, 321	divcan1d 10321	. . . . . . 7
323	322	oveq2d 6300	. . . . . 6
324	320, 323	eqtrd 2508	. . . . 5
325	324	oveq2d 6300	. . . 4
326	317, 325	eqtrd 2508	. . 3
327	311, 326	breqtrrd 4473	. 2 ψ ψ
328	32, 315	readdcld 9623	. . 3
329	16, 328, 313	lemul1d 11295	. 2 ψ ψ ψ ψ
330	327, 329	mpbird 232	1 ψ ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2814

wss 3476 class class class wbr 4447

cfv 5588 (class class class)co 6284

cr 9491

cc0 9492

c1 9493

caddc 9495

cmul 9497

cpnf 9625

clt 9628

cle 9629

cmin 9805

cneg 9806

cdiv 10206

cn 10536

c2 10585

cuz 11082

crp 11220

cioo 11529

cico 11531

cicc 11532

cfz 11672

cfl 11895

cabs 13030

csu 13471

clog 22698 Λcvma 23121 ψcchp 23122

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571 ax-mulf 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-supp 6902 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fsupp 7830 df-fi 7871 df-sup 7901 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-4 10596 df-5 10597 df-6 10598 df-7 10599 df-8 10600 df-9 10601 df-10 10602 df-n0 10796 df-z 10865 df-dec 10977 df-uz 11083 df-q 11183 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-ioo 11533 df-ioc 11534 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-mod 11965 df-seq 12076 df-exp 12135 df-fac 12322 df-bc 12349 df-hash 12374 df-shft 12863 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-limsup 13257 df-clim 13274 df-rlim 13275 df-sum 13472 df-ef 13665 df-sin 13667 df-cos 13668 df-pi 13670 df-dvds 13848 df-gcd 14004 df-prm 14077 df-pc 14220 df-struct 14492 df-ndx 14493 df-slot 14494 df-base 14495 df-sets 14496 df-ress 14497 df-plusg 14568 df-mulr 14569 df-starv 14570 df-sca 14571 df-vsca 14572 df-ip 14573 df-tset 14574 df-ple 14575 df-ds 14577 df-unif 14578 df-hom 14579 df-cco 14580 df-rest 14678 df-topn 14679 df-0g 14697 df-gsum 14698 df-topgen 14699 df-pt 14700 df-prds 14703 df-xrs 14757 df-qtop 14762 df-imas 14763 df-xps 14765 df-mre 14841 df-mrc 14842 df-acs 14844 df-mnd 15732 df-submnd 15787 df-mulg 15870 df-cntz 16160 df-cmn 16606 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-mopn 18214 df-fbas 18215 df-fg 18216 df-cnfld 18220 df-top 19194 df-bases 19196 df-topon 19197 df-topsp 19198 df-cld 19314 df-ntr 19315 df-cls 19316 df-nei 19393 df-lp 19431 df-perf 19432 df-cn 19522 df-cnp 19523 df-haus 19610 df-tx 19826 df-hmeo 20019 df-fil 20110 df-fm 20202 df-flim 20203 df-flf 20204 df-xms 20586 df-ms 20587 df-tms 20588 df-cncf 21145 df-limc 22033 df-dv 22034 df-log 22700 df-vma 23127 df-chp 23128

This theorem is referenced by: chpdifbndlem2 23495

W3C validator