ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 21281

Description: Lemma for ostth2 21284. (Contributed by Mario Carneiro, 10-Sep-2014.)

**Hypotheses**
Ref	Expression
qrng.q	ℂ_fld ↾_s
qabsabv.a	AbsVal
padic.j
ostth.k
ostth.1
ostth2.2
ostth2.3
ostth2.4
ostth2.5
ostth2.6
ostth2.7

**Assertion**
Ref	Expression
ostth2lem2	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem ostth2lem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6048	. . . . . . . . 9
2	1	oveq1d 6055	. . . . . . . 8
3	2	oveq2d 6056	. . . . . . 7
4		oveq2 6048	. . . . . . . . 9
5		oveq2 6048	. . . . . . . . 9
6	4, 5	oveq12d 6058	. . . . . . . 8
7	6	breq2d 4184	. . . . . . 7
8	3, 7	raleqbidv 2876	. . . . . 6
9	8	imbi2d 308	. . . . 5
10		oveq2 6048	. . . . . . . . 9
11	10	oveq1d 6055	. . . . . . . 8
12	11	oveq2d 6056	. . . . . . 7
13		oveq2 6048	. . . . . . . . 9
14		oveq2 6048	. . . . . . . . 9
15	13, 14	oveq12d 6058	. . . . . . . 8
16	15	breq2d 4184	. . . . . . 7
17	12, 16	raleqbidv 2876	. . . . . 6
18	17	imbi2d 308	. . . . 5
19		oveq2 6048	. . . . . . . . 9
20	19	oveq1d 6055	. . . . . . . 8
21	20	oveq2d 6056	. . . . . . 7
22		oveq2 6048	. . . . . . . . 9
23		oveq2 6048	. . . . . . . . 9
24	22, 23	oveq12d 6058	. . . . . . . 8
25	24	breq2d 4184	. . . . . . 7
26	21, 25	raleqbidv 2876	. . . . . 6
27	26	imbi2d 308	. . . . 5
28		oveq2 6048	. . . . . . . . 9
29	28	oveq1d 6055	. . . . . . . 8
30	29	oveq2d 6056	. . . . . . 7
31		oveq2 6048	. . . . . . . . 9
32		oveq2 6048	. . . . . . . . 9
33	31, 32	oveq12d 6058	. . . . . . . 8
34	33	breq2d 4184	. . . . . . 7
35	30, 34	raleqbidv 2876	. . . . . 6
36	35	imbi2d 308	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2b2 10504	. . . . . . . . . . . . . . 15 $/\$
39	38	simplbi 447	. . . . . . . . . . . . . 14
40	37, 39	syl 16	. . . . . . . . . . . . 13
41	40	nncnd 9972	. . . . . . . . . . . 12
42	41	exp0d 11472	. . . . . . . . . . 11
43	42	oveq1d 6055	. . . . . . . . . 10
44		1m1e0 10024	. . . . . . . . . 10
45	43, 44	syl6eq 2452	. . . . . . . . 9
46	45	oveq2d 6056	. . . . . . . 8
47	46	eleq2d 2471	. . . . . . 7
48		0le0 10037	. . . . . . . . . 10
49	48	a1i 11	. . . . . . . . 9
50		ostth.1	. . . . . . . . . 10
51		qabsabv.a	. . . . . . . . . . 11 AbsVal
52		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
53	52	qrng0 21268	. . . . . . . . . . 11
54	51, 53	abv0 15874	. . . . . . . . . 10
55	50, 54	syl 16	. . . . . . . . 9
56	41	mul01d 9221	. . . . . . . . . . 11
57	56	oveq1d 6055	. . . . . . . . . 10
58		ostth2.7	. . . . . . . . . . . . . 14
59		1re 9046	. . . . . . . . . . . . . . 15
60		nnq 10543	. . . . . . . . . . . . . . . . 17
61	40, 60	syl 16	. . . . . . . . . . . . . . . 16
62	52	qrngbas 21266	. . . . . . . . . . . . . . . . 17
63	51, 62	abvcl 15867	. . . . . . . . . . . . . . . 16 $/\$
64	50, 61, 63	syl2anc 643	. . . . . . . . . . . . . . 15
65		ifcl 3735	. . . . . . . . . . . . . . 15 $/\$
66	59, 64, 65	sylancr 645	. . . . . . . . . . . . . 14
67	58, 66	syl5eqel 2488	. . . . . . . . . . . . 13
68	67	recnd 9070	. . . . . . . . . . . 12
69		0nn0 10192	. . . . . . . . . . . 12
70		expcl 11354	. . . . . . . . . . . 12 $/\$
71	68, 69, 70	sylancl 644	. . . . . . . . . . 11
72	71	mul02d 9220	. . . . . . . . . 10
73	57, 72	eqtrd 2436	. . . . . . . . 9
74	49, 55, 73	3brtr4d 4202	. . . . . . . 8
75		elfz1eq 11024	. . . . . . . . . 10
76	75	fveq2d 5691	. . . . . . . . 9
77	76	breq1d 4182	. . . . . . . 8
78	74, 77	syl5ibrcom 214	. . . . . . 7
79	47, 78	sylbid 207	. . . . . 6
80	79	ralrimiv 2748	. . . . 5
81		fveq2 5687	. . . . . . . . . 10
82	81	breq1d 4182	. . . . . . . . 9
83	82	cbvralv 2892	. . . . . . . 8
84	50	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
85		elfzelz 11015	. . . . . . . . . . . . . 14
86	85	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
87		zq 10536	. . . . . . . . . . . . 13
88	86, 87	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
89	51, 62	abvcl 15867	. . . . . . . . . . . 12 $/\$
90	84, 88, 89	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
91	40	ad2antrr 707	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		simplr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
93	91, 92	nnexpcld 11499	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	86, 93	zmodcld 11222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nn0zd 10329	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		zq 10536	. . . . . . . . . . . . . 14
97	95, 96	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
98	51, 62	abvcl 15867	. . . . . . . . . . . . 13 $/\$
99	84, 97, 98	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	91, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
101	84, 100, 63	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101, 92	reexpcld 11495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
103	86	zred 10331	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
104	103, 93	nndivred 10004	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
105	104	flcld 11162	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
106		zq 10536	. . . . . . . . . . . . . . 15
107	105, 106	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	51, 62	abvcl 15867	. . . . . . . . . . . . . 14 $/\$
109	84, 107, 108	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	102, 109	remulcld 9072	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
111	99, 110	readdcld 9071	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	91	nnred 9971	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
113		nn0p1nn 10215	. . . . . . . . . . . . . . 15
114	113	ad2antlr 708	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115	114	nnred 9971	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	112, 115	remulcld 9072	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117	67	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		peano2nn0 10216	. . . . . . . . . . . . . 14
119	118	ad2antlr 708	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	117, 119	reexpcld 11495	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	116, 120	remulcld 9072	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122		nnq 10543	. . . . . . . . . . . . . . 15
123	93, 122	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		qmulcl 10548	. . . . . . . . . . . . . 14 $/\$
125	123, 107, 124	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126		qex 10542	. . . . . . . . . . . . . . 15
127		cnfldadd 16663	. . . . . . . . . . . . . . . 16 ℂ_fld
128	52, 127	ressplusg 13526	. . . . . . . . . . . . . . 15
129	126, 128	ax-mp 8	. . . . . . . . . . . . . 14
130	51, 62, 129	abvtri 15873	. . . . . . . . . . . . 13 $/\$ $/\$
131	84, 97, 125, 130	syl3anc 1184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
132	93	nnrpd 10603	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
133		modval 11207	. . . . . . . . . . . . . . . 16 $/\$
134	103, 132, 133	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
135	134	oveq1d 6055	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	103	recnd 9070	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137		qcn 10544	. . . . . . . . . . . . . . . 16
138	125, 137	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	136, 138	npcand 9371	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140	135, 139	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
141	140	fveq2d 5691	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
142		cnfldmul 16664	. . . . . . . . . . . . . . . . . 18 ℂ_fld
143	52, 142	ressmulr 13537	. . . . . . . . . . . . . . . . 17
144	126, 143	ax-mp 8	. . . . . . . . . . . . . . . 16
145	51, 62, 144	abvmul 15872	. . . . . . . . . . . . . . 15 $/\$ $/\$
146	84, 123, 107, 145	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147	52, 51	qabvexp 21273	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	84, 100, 92, 147	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	148	oveq1d 6055	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	146, 149	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	oveq2d 6056	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	131, 141, 151	3brtr3d 4201	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	117, 92	reexpcld 11495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154	116, 153	remulcld 9072	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
155		nn0re 10186	. . . . . . . . . . . . . . . . 17
156	155	ad2antlr 708	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
157	112, 156	remulcld 9072	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	157, 153	remulcld 9072	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159	112, 153	remulcld 9072	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160		zmodfz 11223	. . . . . . . . . . . . . . . 16 $/\$
161	86, 93, 160	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		simprr 734	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163		fveq2 5687	. . . . . . . . . . . . . . . . 17
164	163	breq1d 4182	. . . . . . . . . . . . . . . 16
165	164	rspcv 3008	. . . . . . . . . . . . . . 15
166	161, 162, 165	sylc 58	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	112, 102	remulcld 9072	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
168	102	recnd 9070	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	109	recnd 9070	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
170	168, 169	mulcomd 9065	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
171	51, 62	abvge0 15868	. . . . . . . . . . . . . . . . . . 19 $/\$
172	84, 100, 171	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173	101, 92, 172	expge0d 11496	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
174	105	zred 10331	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175		elfzle1 11016	. . . . . . . . . . . . . . . . . . . . . 22
176	175	ad2antrl 709	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	93	nnred 9971	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178	93	nngt0d 9999	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179		divge0 9835	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
180	103, 176, 177, 178, 179	syl22anc 1185	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181		flge0nn0 11180	. . . . . . . . . . . . . . . . . . . 20 $/\$
182	104, 180, 181	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
183	52, 51	qabvle 21272	. . . . . . . . . . . . . . . . . . 19 $/\$
184	84, 182, 183	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
186		0z 10249	. . . . . . . . . . . . . . . . . . . . . . . . 25
187	91, 119	nnexpcld 11499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
188	187	nnzd 10330	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189		elfzm11 11071	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
190	186, 188, 189	sylancr 645	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
191	185, 190	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	simp3d 971	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
193	91	nncnd 9972	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
194	193, 92	expp1d 11479	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
195	192, 194	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
196		ltdivmul 9838	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
197	103, 112, 177, 178, 196	syl112anc 1188	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
198	195, 197	mpbird 224	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	91	nnzd 10330	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
200		fllt 11170	. . . . . . . . . . . . . . . . . . . . 21 $/\$
201	104, 199, 200	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
202	198, 201	mpbid 202	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
203	174, 112, 202	ltled 9177	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	109, 174, 112, 184, 203	letrd 9183	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
205	109, 112, 102, 173, 204	lemul1ad 9906	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
206	170, 205	eqbrtrd 4192	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
207	91	nnnn0d 10230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
208	207	nn0ge0d 10233	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209		max1 10729	. . . . . . . . . . . . . . . . . . 19 $/\$
210	101, 59, 209	sylancl 644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
211	210, 58	syl6breqr 4212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
212		leexp1a 11393	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
213	101, 117, 92, 172, 211, 212	syl32anc 1192	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	102, 153, 112, 208, 213	lemul2ad 9907	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
215	110, 167, 159, 206, 214	letrd 9183	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
216	99, 110, 158, 159, 166, 215	le2addd 9600	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
217		nn0cn 10187	. . . . . . . . . . . . . . . . . 18
218	217	ad2antlr 708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219		ax-1cn 9004	. . . . . . . . . . . . . . . . . 18
220	219	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	193, 218, 220	adddid 9068	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	193	mulid1d 9061	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	222	oveq2d 6056	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
224	221, 223	eqtrd 2436	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	224	oveq1d 6055	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
226	193, 218	mulcld 9064	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
227	153	recnd 9070	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
228	226, 193, 227	adddird 9069	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
229	225, 228	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
230	216, 229	breqtrrd 4198	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
231		max2 10731	. . . . . . . . . . . . . . . 16 $/\$
232	101, 59, 231	sylancl 644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	232, 58	syl6breqr 4212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
234		nn0z 10260	. . . . . . . . . . . . . . . . 17
235	234	ad2antlr 708	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
236		uzid 10456	. . . . . . . . . . . . . . . 16
237	235, 236	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
238		peano2uz 10486	. . . . . . . . . . . . . . 15
239	237, 238	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
240	117, 233, 239	leexp2ad 11510	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
241	91, 114	nnmulcld 10003	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
242	241	nngt0d 9999	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
243		lemul2 9819	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	153, 120, 116, 242, 243	syl112anc 1188	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
245	240, 244	mpbid 202	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
246	111, 154, 121, 230, 245	letrd 9183	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	90, 111, 121, 152, 246	letrd 9183	. . . . . . . . . 10 $/\$ $/\$ $/\$
248	247	expr 599	. . . . . . . . 9 $/\$ $/\$
249	248	ralrimdva 2756	. . . . . . . 8 $/\$
250	83, 249	syl5bi 209	. . . . . . 7 $/\$
251	250	expcom 425	. . . . . 6
252	251	a2d 24	. . . . 5
253	9, 18, 27, 36, 80, 252	nn0ind 10322	. . . 4
254	253	impcom 420	. . 3 $/\$
255		fveq2 5687	. . . . 5
256	255	breq1d 4182	. . . 4
257	256	rspccv 3009	. . 3
258	254, 257	syl 16	. 2 $/\$
259	258	3impia 1150	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

cvv 2916

cif 3699 class class class wbr 4172

cmpt 4226

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cneg 9248

cdiv 9633

cn 9956

c2 10005

cn0 10177

cz 10238

cuz 10444

cq 10530

crp 10568

cfz 10999

cfl 11156

cmo 11205

cexp 11337

cprime 13034

cpc 13165 ↾_s cress 13425

cplusg 13484

cmulr 13485 AbsValcabv 15859 ℂ_fldccnfld 16658

clog 20405

This theorem is referenced by: ostth2lem3 21282

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-tpos 6438 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-ico 10878 df-fz 11000 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-0g 13682 df-mnd 14645 df-grp 14767 df-minusg 14768 df-subg 14896 df-cmn 15369 df-mgp 15604 df-rng 15618 df-cring 15619 df-ur 15620 df-oppr 15683 df-dvdsr 15701 df-unit 15702 df-invr 15732 df-dvr 15743 df-drng 15792 df-subrg 15821 df-abv 15860 df-cnfld 16659

W3C validator