ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 24468

Description: Lemma for ostth2 24471. (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 6312	. . . . . . . . 9
2	1	oveq1d 6319	. . . . . . . 8
3	2	oveq2d 6320	. . . . . . 7
4		oveq2 6312	. . . . . . . . 9
5		oveq2 6312	. . . . . . . . 9
6	4, 5	oveq12d 6322	. . . . . . . 8
7	6	breq2d 4434	. . . . . . 7
8	3, 7	raleqbidv 3040	. . . . . 6
9	8	imbi2d 318	. . . . 5
10		oveq2 6312	. . . . . . . . 9
11	10	oveq1d 6319	. . . . . . . 8
12	11	oveq2d 6320	. . . . . . 7
13		oveq2 6312	. . . . . . . . 9
14		oveq2 6312	. . . . . . . . 9
15	13, 14	oveq12d 6322	. . . . . . . 8
16	15	breq2d 4434	. . . . . . 7
17	12, 16	raleqbidv 3040	. . . . . 6
18	17	imbi2d 318	. . . . 5
19		oveq2 6312	. . . . . . . . 9
20	19	oveq1d 6319	. . . . . . . 8
21	20	oveq2d 6320	. . . . . . 7
22		oveq2 6312	. . . . . . . . 9
23		oveq2 6312	. . . . . . . . 9
24	22, 23	oveq12d 6322	. . . . . . . 8
25	24	breq2d 4434	. . . . . . 7
26	21, 25	raleqbidv 3040	. . . . . 6
27	26	imbi2d 318	. . . . 5
28		oveq2 6312	. . . . . . . . 9
29	28	oveq1d 6319	. . . . . . . 8
30	29	oveq2d 6320	. . . . . . 7
31		oveq2 6312	. . . . . . . . 9
32		oveq2 6312	. . . . . . . . 9
33	31, 32	oveq12d 6322	. . . . . . . 8
34	33	breq2d 4434	. . . . . . 7
35	30, 34	raleqbidv 3040	. . . . . 6
36	35	imbi2d 318	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2nn 11203	. . . . . . . . . . . . . 14
39	37, 38	syl 17	. . . . . . . . . . . . 13
40	39	nncnd 10631	. . . . . . . . . . . 12
41	40	exp0d 12415	. . . . . . . . . . 11
42	41	oveq1d 6319	. . . . . . . . . 10
43		1m1e0 10684	. . . . . . . . . 10
44	42, 43	syl6eq 2480	. . . . . . . . 9
45	44	oveq2d 6320	. . . . . . . 8
46	45	eleq2d 2493	. . . . . . 7
47		0le0 10705	. . . . . . . . . 10
48	47	a1i 11	. . . . . . . . 9
49		ostth.1	. . . . . . . . . 10
50		qabsabv.a	. . . . . . . . . . 11 AbsVal
51		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
52	51	qrng0 24455	. . . . . . . . . . 11
53	50, 52	abv0 18056	. . . . . . . . . 10
54	49, 53	syl 17	. . . . . . . . 9
55	40	mul01d 9838	. . . . . . . . . . 11
56	55	oveq1d 6319	. . . . . . . . . 10
57		ostth2.7	. . . . . . . . . . . . . 14
58		1re 9648	. . . . . . . . . . . . . . 15
59		nnq 11283	. . . . . . . . . . . . . . . . 17
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16
61	51	qrngbas 24453	. . . . . . . . . . . . . . . . 17
62	50, 61	abvcl 18049	. . . . . . . . . . . . . . . 16 $/\$
63	49, 60, 62	syl2anc 666	. . . . . . . . . . . . . . 15
64		ifcl 3953	. . . . . . . . . . . . . . 15 $/\$
65	58, 63, 64	sylancr 668	. . . . . . . . . . . . . 14
66	57, 65	syl5eqel 2515	. . . . . . . . . . . . 13
67	66	recnd 9675	. . . . . . . . . . . 12
68		0nn0 10890	. . . . . . . . . . . 12
69		expcl 12295	. . . . . . . . . . . 12 $/\$
70	67, 68, 69	sylancl 667	. . . . . . . . . . 11
71	70	mul02d 9837	. . . . . . . . . 10
72	56, 71	eqtrd 2464	. . . . . . . . 9
73	48, 54, 72	3brtr4d 4453	. . . . . . . 8
74		elfz1eq 11816	. . . . . . . . . 10
75	74	fveq2d 5884	. . . . . . . . 9
76	75	breq1d 4432	. . . . . . . 8
77	73, 76	syl5ibrcom 226	. . . . . . 7
78	46, 77	sylbid 219	. . . . . 6
79	78	ralrimiv 2838	. . . . 5
80		fveq2 5880	. . . . . . . . . 10
81	80	breq1d 4432	. . . . . . . . 9
82	81	cbvralv 3056	. . . . . . . 8
83	49	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84		elfzelz 11806	. . . . . . . . . . . . . 14
85	84	ad2antrl 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
86		zq 11276	. . . . . . . . . . . . 13
87	85, 86	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88	50, 61	abvcl 18049	. . . . . . . . . . . 12 $/\$
89	83, 87, 88	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90	39	ad2antrr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91		simplr 761	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92	90, 91	nnexpcld 12442	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
93	85, 92	zmodcld 12122	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	93	nn0zd 11044	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
95		zq 11276	. . . . . . . . . . . . . 14
96	94, 95	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	50, 61	abvcl 18049	. . . . . . . . . . . . 13 $/\$
98	83, 96, 97	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	83, 99, 62	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100, 91	reexpcld 12438	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
102	85	zred 11046	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 92	nndivred 10664	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	103	flcld 12039	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		zq 11276	. . . . . . . . . . . . . . 15
106	104, 105	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	50, 61	abvcl 18049	. . . . . . . . . . . . . 14 $/\$
108	83, 106, 107	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	101, 108	remulcld 9677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	98, 109	readdcld 9676	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	90	nnred 10630	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
112		nn0p1nn 10915	. . . . . . . . . . . . . . 15
113	112	ad2antlr 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	113	nnred 10630	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	111, 114	remulcld 9677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
116	66	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		peano2nn0 10916	. . . . . . . . . . . . . 14
118	117	ad2antlr 732	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
119	116, 118	reexpcld 12438	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	115, 119	remulcld 9677	. . . . . . . . . . 11 $/\$ $/\$ $/\$
121		nnq 11283	. . . . . . . . . . . . . . 15
122	92, 121	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123		qmulcl 11288	. . . . . . . . . . . . . 14 $/\$
124	122, 106, 123	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125		qex 11282	. . . . . . . . . . . . . . 15
126		cnfldadd 18972	. . . . . . . . . . . . . . . 16 ℂ_fld
127	51, 126	ressplusg 15236	. . . . . . . . . . . . . . 15
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14
129	50, 61, 128	abvtri 18055	. . . . . . . . . . . . 13 $/\$ $/\$
130	83, 96, 124, 129	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	92	nnrpd 11345	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
132		modval 12103	. . . . . . . . . . . . . . . 16 $/\$
133	102, 131, 132	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
134	133	oveq1d 6319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
135	102	recnd 9675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		qcn 11284	. . . . . . . . . . . . . . . 16
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	135, 137	npcand 9996	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	134, 138	eqtrd 2464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139	fveq2d 5884	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141		cnfldmul 18973	. . . . . . . . . . . . . . . . . 18 ℂ_fld
142	51, 141	ressmulr 15247	. . . . . . . . . . . . . . . . 17
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16
144	50, 61, 143	abvmul 18054	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	83, 122, 106, 144	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	51, 50	qabvexp 24460	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	83, 99, 91, 146	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148	147	oveq1d 6319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	145, 148	eqtrd 2464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	149	oveq2d 6320	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	130, 140, 150	3brtr3d 4452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	116, 91	reexpcld 12438	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	115, 152	remulcld 9677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154		nn0re 10884	. . . . . . . . . . . . . . . . 17
155	154	ad2antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	111, 155	remulcld 9677	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 152	remulcld 9677	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	111, 152	remulcld 9677	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		zmodfz 12123	. . . . . . . . . . . . . . . 16 $/\$
160	85, 92, 159	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
161		simprr 765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		fveq2 5880	. . . . . . . . . . . . . . . . 17
163	162	breq1d 4432	. . . . . . . . . . . . . . . 16
164	163	rspcv 3179	. . . . . . . . . . . . . . 15
165	160, 161, 164	sylc 63	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166	111, 101	remulcld 9677	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167	101	recnd 9675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
168	108	recnd 9675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	167, 168	mulcomd 9670	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
170	50, 61	abvge0 18050	. . . . . . . . . . . . . . . . . . 19 $/\$
171	83, 99, 170	syl2anc 666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
172	100, 91, 171	expge0d 12439	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
173	104	zred 11046	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
174		elfzle1 11808	. . . . . . . . . . . . . . . . . . . . . 22
175	174	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
176	92	nnred 10630	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	92	nngt0d 10659	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178		divge0 10480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179	102, 175, 176, 177, 178	syl22anc 1266	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
180		flge0nn0 12059	. . . . . . . . . . . . . . . . . . . 20 $/\$
181	103, 179, 180	syl2anc 666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	51, 50	qabvle 24459	. . . . . . . . . . . . . . . . . . 19 $/\$
183	83, 181, 182	syl2anc 666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184		simprl 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
185		0z 10954	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	90, 118	nnexpcld 12442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
187	186	nnzd 11045	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188		elfzm11 11871	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189	185, 187, 188	sylancr 668	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
190	184, 189	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	simp3d 1020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
192	90	nncnd 10631	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
193	192, 91	expp1d 12422	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
194	191, 193	breqtrd 4447	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
195		ltdivmul 10486	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
196	102, 111, 176, 177, 195	syl112anc 1269	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
197	194, 196	mpbird 236	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	90	nnzd 11045	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		fllt 12047	. . . . . . . . . . . . . . . . . . . . 21 $/\$
200	103, 198, 199	syl2anc 666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	197, 200	mpbid 214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202	173, 111, 201	ltled 9789	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	108, 173, 111, 183, 202	letrd 9798	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
204	108, 111, 101, 172, 203	lemul1ad 10552	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
205	169, 204	eqbrtrd 4443	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
206	90	nnnn0d 10931	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	nn0ge0d 10934	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208		max1 11486	. . . . . . . . . . . . . . . . . . 19 $/\$
209	100, 58, 208	sylancl 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
210	209, 57	syl6breqr 4463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211		leexp1a 12336	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	100, 116, 91, 171, 210, 211	syl32anc 1273	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
213	101, 152, 111, 207, 212	lemul2ad 10553	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
214	109, 166, 158, 205, 213	letrd 9798	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	98, 109, 157, 158, 165, 214	le2addd 10238	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
216		nn0cn 10885	. . . . . . . . . . . . . . . . . 18
217	216	ad2antlr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
218		1cnd 9665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219	192, 217, 218	adddid 9673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
220	192	mulid1d 9666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	220	oveq2d 6320	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	219, 221	eqtrd 2464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
223	222	oveq1d 6319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
224	192, 217	mulcld 9669	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	152	recnd 9675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	224, 192, 225	adddird 9674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
227	223, 226	eqtrd 2464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
228	215, 227	breqtrrd 4449	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
229		max2 11488	. . . . . . . . . . . . . . . 16 $/\$
230	100, 58, 229	sylancl 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	230, 57	syl6breqr 4463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
232		nn0z 10966	. . . . . . . . . . . . . . . . 17
233	232	ad2antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
234		uzid 11179	. . . . . . . . . . . . . . . 16
235	233, 234	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
236		peano2uz 11218	. . . . . . . . . . . . . . 15
237	235, 236	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
238	116, 231, 237	leexp2ad 12453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
239	90, 113	nnmulcld 10663	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	239	nngt0d 10659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241		lemul2 10464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
242	152, 119, 115, 240, 241	syl112anc 1269	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
243	238, 242	mpbid 214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
244	110, 153, 120, 228, 243	letrd 9798	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	89, 110, 120, 151, 244	letrd 9798	. . . . . . . . . 10 $/\$ $/\$ $/\$
246	245	expr 619	. . . . . . . . 9 $/\$ $/\$
247	246	ralrimdva 2844	. . . . . . . 8 $/\$
248	82, 247	syl5bi 221	. . . . . . 7 $/\$
249	248	expcom 437	. . . . . 6
250	249	a2d 30	. . . . 5
251	9, 18, 27, 36, 79, 250	nn0ind 11036	. . . 4
252	251	impcom 432	. . 3 $/\$
253		fveq2 5880	. . . . 5
254	253	breq1d 4432	. . . 4
255	254	rspccv 3180	. . 3
256	252, 255	syl 17	. 2 $/\$
257	256	3impia 1203	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wral 2776

cvv 3082

cif 3911 class class class wbr 4422

cmpt 4481

cfv 5600 (class class class)co 6304

cc 9543

cr 9544

cc0 9545

c1 9546

caddc 9548

cmul 9550

clt 9681

cle 9682

cmin 9866

cneg 9867

cdiv 10275

cn 10615

c2 10665

cn0 10875

cz 10943

cuz 11165

cq 11270

crp 11308

cfz 11790

cfl 12031

cmo 12101

cexp 12277

cprime 14619

cpc 14783 ↾_s cress 15119

cplusg 15187

cmulr 15188 AbsValcabv 18041 ℂ_fldccnfld 18967

clog 23500

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4535 ax-sep 4545 ax-nul 4554 ax-pow 4601 ax-pr 4659 ax-un 6596 ax-cnex 9601 ax-resscn 9602 ax-1cn 9603 ax-icn 9604 ax-addcl 9605 ax-addrcl 9606 ax-mulcl 9607 ax-mulrcl 9608 ax-mulcom 9609 ax-addass 9610 ax-mulass 9611 ax-distr 9612 ax-i2m1 9613 ax-1ne0 9614 ax-1rid 9615 ax-rnegex 9616 ax-rrecex 9617 ax-cnre 9618 ax-pre-lttri 9619 ax-pre-lttrn 9620 ax-pre-ltadd 9621 ax-pre-mulgt0 9622 ax-pre-sup 9623 ax-addf 9624 ax-mulf 9625

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3302 df-csb 3398 df-dif 3441 df-un 3443 df-in 3445 df-ss 3452 df-pss 3454 df-nul 3764 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4219 df-int 4255 df-iun 4300 df-br 4423 df-opab 4482 df-mpt 4483 df-tr 4518 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-riota 6266 df-ov 6307 df-oprab 6308 df-mpt2 6309 df-om 6706 df-1st 6806 df-2nd 6807 df-tpos 6983 df-wrecs 7038 df-recs 7100 df-rdg 7138 df-1o 7192 df-oadd 7196 df-er 7373 df-map 7484 df-en 7580 df-dom 7581 df-sdom 7582 df-fin 7583 df-sup 7964 df-inf 7965 df-pnf 9683 df-mnf 9684 df-xr 9685 df-ltxr 9686 df-le 9687 df-sub 9868 df-neg 9869 df-div 10276 df-nn 10616 df-2 10674 df-3 10675 df-4 10676 df-5 10677 df-6 10678 df-7 10679 df-8 10680 df-9 10681 df-10 10682 df-n0 10876 df-z 10944 df-dec 11058 df-uz 11166 df-q 11271 df-rp 11309 df-ico 11647 df-fz 11791 df-fl 12033 df-mod 12102 df-seq 12219 df-exp 12278 df-struct 15120 df-ndx 15121 df-slot 15122 df-base 15123 df-sets 15124 df-ress 15125 df-plusg 15200 df-mulr 15201 df-starv 15202 df-tset 15206 df-ple 15207 df-ds 15209 df-unif 15210 df-0g 15337 df-mgm 16485 df-sgrp 16524 df-mnd 16534 df-grp 16670 df-minusg 16671 df-subg 16811 df-cmn 17429 df-mgp 17721 df-ur 17733 df-ring 17779 df-cring 17780 df-oppr 17848 df-dvdsr 17866 df-unit 17867 df-invr 17897 df-dvr 17908 df-drng 17974 df-subrg 18003 df-abv 18042 df-cnfld 18968

This theorem is referenced by: ostth2lem3 24469

W3C validator