ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 24484

Description: Lemma for ostth2 24487. (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 6303	. . . . . . . . 9
2	1	oveq1d 6310	. . . . . . . 8
3	2	oveq2d 6311	. . . . . . 7
4		oveq2 6303	. . . . . . . . 9
5		oveq2 6303	. . . . . . . . 9
6	4, 5	oveq12d 6313	. . . . . . . 8
7	6	breq2d 4417	. . . . . . 7
8	3, 7	raleqbidv 3003	. . . . . 6
9	8	imbi2d 318	. . . . 5
10		oveq2 6303	. . . . . . . . 9
11	10	oveq1d 6310	. . . . . . . 8
12	11	oveq2d 6311	. . . . . . 7
13		oveq2 6303	. . . . . . . . 9
14		oveq2 6303	. . . . . . . . 9
15	13, 14	oveq12d 6313	. . . . . . . 8
16	15	breq2d 4417	. . . . . . 7
17	12, 16	raleqbidv 3003	. . . . . 6
18	17	imbi2d 318	. . . . 5
19		oveq2 6303	. . . . . . . . 9
20	19	oveq1d 6310	. . . . . . . 8
21	20	oveq2d 6311	. . . . . . 7
22		oveq2 6303	. . . . . . . . 9
23		oveq2 6303	. . . . . . . . 9
24	22, 23	oveq12d 6313	. . . . . . . 8
25	24	breq2d 4417	. . . . . . 7
26	21, 25	raleqbidv 3003	. . . . . 6
27	26	imbi2d 318	. . . . 5
28		oveq2 6303	. . . . . . . . 9
29	28	oveq1d 6310	. . . . . . . 8
30	29	oveq2d 6311	. . . . . . 7
31		oveq2 6303	. . . . . . . . 9
32		oveq2 6303	. . . . . . . . 9
33	31, 32	oveq12d 6313	. . . . . . . 8
34	33	breq2d 4417	. . . . . . 7
35	30, 34	raleqbidv 3003	. . . . . 6
36	35	imbi2d 318	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2nn 11204	. . . . . . . . . . . . . 14
39	37, 38	syl 17	. . . . . . . . . . . . 13
40	39	nncnd 10632	. . . . . . . . . . . 12
41	40	exp0d 12417	. . . . . . . . . . 11
42	41	oveq1d 6310	. . . . . . . . . 10
43		1m1e0 10685	. . . . . . . . . 10
44	42, 43	syl6eq 2503	. . . . . . . . 9
45	44	oveq2d 6311	. . . . . . . 8
46	45	eleq2d 2516	. . . . . . 7
47		0le0 10706	. . . . . . . . . 10
48	47	a1i 11	. . . . . . . . 9
49		ostth.1	. . . . . . . . . 10
50		qabsabv.a	. . . . . . . . . . 11 AbsVal
51		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
52	51	qrng0 24471	. . . . . . . . . . 11
53	50, 52	abv0 18071	. . . . . . . . . 10
54	49, 53	syl 17	. . . . . . . . 9
55	40	mul01d 9837	. . . . . . . . . . 11
56	55	oveq1d 6310	. . . . . . . . . 10
57		ostth2.7	. . . . . . . . . . . . . 14
58		1re 9647	. . . . . . . . . . . . . . 15
59		nnq 11284	. . . . . . . . . . . . . . . . 17
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16
61	51	qrngbas 24469	. . . . . . . . . . . . . . . . 17
62	50, 61	abvcl 18064	. . . . . . . . . . . . . . . 16 $/\$
63	49, 60, 62	syl2anc 667	. . . . . . . . . . . . . . 15
64		ifcl 3925	. . . . . . . . . . . . . . 15 $/\$
65	58, 63, 64	sylancr 670	. . . . . . . . . . . . . 14
66	57, 65	syl5eqel 2535	. . . . . . . . . . . . 13
67	66	recnd 9674	. . . . . . . . . . . 12
68		0nn0 10891	. . . . . . . . . . . 12
69		expcl 12297	. . . . . . . . . . . 12 $/\$
70	67, 68, 69	sylancl 669	. . . . . . . . . . 11
71	70	mul02d 9836	. . . . . . . . . 10
72	56, 71	eqtrd 2487	. . . . . . . . 9
73	48, 54, 72	3brtr4d 4436	. . . . . . . 8
74		elfz1eq 11817	. . . . . . . . . 10
75	74	fveq2d 5874	. . . . . . . . 9
76	75	breq1d 4415	. . . . . . . 8
77	73, 76	syl5ibrcom 226	. . . . . . 7
78	46, 77	sylbid 219	. . . . . 6
79	78	ralrimiv 2802	. . . . 5
80		fveq2 5870	. . . . . . . . . 10
81	80	breq1d 4415	. . . . . . . . 9
82	81	cbvralv 3021	. . . . . . . 8
83	49	ad2antrr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84		elfzelz 11807	. . . . . . . . . . . . . 14
85	84	ad2antrl 735	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
86		zq 11277	. . . . . . . . . . . . 13
87	85, 86	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88	50, 61	abvcl 18064	. . . . . . . . . . . 12 $/\$
89	83, 87, 88	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90	39	ad2antrr 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91		simplr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92	90, 91	nnexpcld 12444	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
93	85, 92	zmodcld 12124	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	93	nn0zd 11045	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
95		zq 11277	. . . . . . . . . . . . . 14
96	94, 95	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	50, 61	abvcl 18064	. . . . . . . . . . . . 13 $/\$
98	83, 96, 97	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	83, 99, 62	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100, 91	reexpcld 12440	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
102	85	zred 11047	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 92	nndivred 10665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	103	flcld 12041	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		zq 11277	. . . . . . . . . . . . . . 15
106	104, 105	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	50, 61	abvcl 18064	. . . . . . . . . . . . . 14 $/\$
108	83, 106, 107	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	101, 108	remulcld 9676	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	98, 109	readdcld 9675	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	90	nnred 10631	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
112		nn0p1nn 10916	. . . . . . . . . . . . . . 15
113	112	ad2antlr 734	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	113	nnred 10631	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	111, 114	remulcld 9676	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
116	66	ad2antrr 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		peano2nn0 10917	. . . . . . . . . . . . . 14
118	117	ad2antlr 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
119	116, 118	reexpcld 12440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	115, 119	remulcld 9676	. . . . . . . . . . 11 $/\$ $/\$ $/\$
121		nnq 11284	. . . . . . . . . . . . . . 15
122	92, 121	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123		qmulcl 11289	. . . . . . . . . . . . . 14 $/\$
124	122, 106, 123	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125		qex 11283	. . . . . . . . . . . . . . 15
126		cnfldadd 18987	. . . . . . . . . . . . . . . 16 ℂ_fld
127	51, 126	ressplusg 15251	. . . . . . . . . . . . . . 15
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14
129	50, 61, 128	abvtri 18070	. . . . . . . . . . . . 13 $/\$ $/\$
130	83, 96, 124, 129	syl3anc 1269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	92	nnrpd 11346	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
132		modval 12105	. . . . . . . . . . . . . . . 16 $/\$
133	102, 131, 132	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
134	133	oveq1d 6310	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
135	102	recnd 9674	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		qcn 11285	. . . . . . . . . . . . . . . 16
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	135, 137	npcand 9995	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	134, 138	eqtrd 2487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139	fveq2d 5874	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141		cnfldmul 18988	. . . . . . . . . . . . . . . . . 18 ℂ_fld
142	51, 141	ressmulr 15262	. . . . . . . . . . . . . . . . 17
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16
144	50, 61, 143	abvmul 18069	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	83, 122, 106, 144	syl3anc 1269	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	51, 50	qabvexp 24476	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	83, 99, 91, 146	syl3anc 1269	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148	147	oveq1d 6310	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	145, 148	eqtrd 2487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	149	oveq2d 6311	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	130, 140, 150	3brtr3d 4435	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	116, 91	reexpcld 12440	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	115, 152	remulcld 9676	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154		nn0re 10885	. . . . . . . . . . . . . . . . 17
155	154	ad2antlr 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	111, 155	remulcld 9676	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 152	remulcld 9676	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	111, 152	remulcld 9676	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		zmodfz 12125	. . . . . . . . . . . . . . . 16 $/\$
160	85, 92, 159	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
161		simprr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		fveq2 5870	. . . . . . . . . . . . . . . . 17
163	162	breq1d 4415	. . . . . . . . . . . . . . . 16
164	163	rspcv 3148	. . . . . . . . . . . . . . 15
165	160, 161, 164	sylc 62	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166	111, 101	remulcld 9676	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167	101	recnd 9674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
168	108	recnd 9674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	167, 168	mulcomd 9669	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
170	50, 61	abvge0 18065	. . . . . . . . . . . . . . . . . . 19 $/\$
171	83, 99, 170	syl2anc 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
172	100, 91, 171	expge0d 12441	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
173	104	zred 11047	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
174		elfzle1 11809	. . . . . . . . . . . . . . . . . . . . . 22
175	174	ad2antrl 735	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
176	92	nnred 10631	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	92	nngt0d 10660	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178		divge0 10481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179	102, 175, 176, 177, 178	syl22anc 1270	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
180		flge0nn0 12061	. . . . . . . . . . . . . . . . . . . 20 $/\$
181	103, 179, 180	syl2anc 667	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	51, 50	qabvle 24475	. . . . . . . . . . . . . . . . . . 19 $/\$
183	83, 181, 182	syl2anc 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184		simprl 765	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
185		0z 10955	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	90, 118	nnexpcld 12444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
187	186	nnzd 11046	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188		elfzm11 11872	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189	185, 187, 188	sylancr 670	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
190	184, 189	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	simp3d 1023	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
192	90	nncnd 10632	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
193	192, 91	expp1d 12424	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
194	191, 193	breqtrd 4430	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
195		ltdivmul 10487	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
196	102, 111, 176, 177, 195	syl112anc 1273	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
197	194, 196	mpbird 236	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	90	nnzd 11046	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		fllt 12049	. . . . . . . . . . . . . . . . . . . . 21 $/\$
200	103, 198, 199	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	197, 200	mpbid 214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202	173, 111, 201	ltled 9788	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	108, 173, 111, 183, 202	letrd 9797	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
204	108, 111, 101, 172, 203	lemul1ad 10553	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
205	169, 204	eqbrtrd 4426	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
206	90	nnnn0d 10932	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	nn0ge0d 10935	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208		max1 11487	. . . . . . . . . . . . . . . . . . 19 $/\$
209	100, 58, 208	sylancl 669	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
210	209, 57	syl6breqr 4446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211		leexp1a 12338	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	100, 116, 91, 171, 210, 211	syl32anc 1277	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
213	101, 152, 111, 207, 212	lemul2ad 10554	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
214	109, 166, 158, 205, 213	letrd 9797	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	98, 109, 157, 158, 165, 214	le2addd 10239	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
216		nn0cn 10886	. . . . . . . . . . . . . . . . . 18
217	216	ad2antlr 734	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
218		1cnd 9664	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219	192, 217, 218	adddid 9672	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
220	192	mulid1d 9665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	220	oveq2d 6311	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	219, 221	eqtrd 2487	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
223	222	oveq1d 6310	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
224	192, 217	mulcld 9668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	152	recnd 9674	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	224, 192, 225	adddird 9673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
227	223, 226	eqtrd 2487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
228	215, 227	breqtrrd 4432	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
229		max2 11489	. . . . . . . . . . . . . . . 16 $/\$
230	100, 58, 229	sylancl 669	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	230, 57	syl6breqr 4446	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
232		nn0z 10967	. . . . . . . . . . . . . . . . 17
233	232	ad2antlr 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
234		uzid 11180	. . . . . . . . . . . . . . . 16
235	233, 234	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
236		peano2uz 11219	. . . . . . . . . . . . . . 15
237	235, 236	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
238	116, 231, 237	leexp2ad 12455	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
239	90, 113	nnmulcld 10664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	239	nngt0d 10660	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241		lemul2 10465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
242	152, 119, 115, 240, 241	syl112anc 1273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
243	238, 242	mpbid 214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
244	110, 153, 120, 228, 243	letrd 9797	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	89, 110, 120, 151, 244	letrd 9797	. . . . . . . . . 10 $/\$ $/\$ $/\$
246	245	expr 620	. . . . . . . . 9 $/\$ $/\$
247	246	ralrimdva 2808	. . . . . . . 8 $/\$
248	82, 247	syl5bi 221	. . . . . . 7 $/\$
249	248	expcom 437	. . . . . 6
250	249	a2d 29	. . . . 5
251	9, 18, 27, 36, 79, 250	nn0ind 11037	. . . 4
252	251	impcom 432	. . 3 $/\$
253		fveq2 5870	. . . . 5
254	253	breq1d 4415	. . . 4
255	254	rspccv 3149	. . 3
256	252, 255	syl 17	. 2 $/\$
257	256	3impia 1206	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1446

wcel 1889

wral 2739

cvv 3047

cif 3883 class class class wbr 4405

cmpt 4464

cfv 5585 (class class class)co 6295

cc 9542

cr 9543

cc0 9544

c1 9545

caddc 9547

cmul 9549

clt 9680

cle 9681

cmin 9865

cneg 9866

cdiv 10276

cn 10616

c2 10666

cn0 10876

cz 10944

cuz 11166

cq 11271

crp 11309

cfz 11791

cfl 12033

cmo 12103

cexp 12279

cprime 14634

cpc 14798 ↾_s cress 15134

cplusg 15202

cmulr 15203 AbsValcabv 18056 ℂ_fldccnfld 18982

clog 23516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 ax-pre-sup 9622 ax-addf 9623 ax-mulf 9624

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 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-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-tpos 6978 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-sup 7961 df-inf 7962 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-7 10680 df-8 10681 df-9 10682 df-10 10683 df-n0 10877 df-z 10945 df-dec 11059 df-uz 11167 df-q 11272 df-rp 11310 df-ico 11648 df-fz 11792 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-struct 15135 df-ndx 15136 df-slot 15137 df-base 15138 df-sets 15139 df-ress 15140 df-plusg 15215 df-mulr 15216 df-starv 15217 df-tset 15221 df-ple 15222 df-ds 15224 df-unif 15225 df-0g 15352 df-mgm 16500 df-sgrp 16539 df-mnd 16549 df-grp 16685 df-minusg 16686 df-subg 16826 df-cmn 17444 df-mgp 17736 df-ur 17748 df-ring 17794 df-cring 17795 df-oppr 17863 df-dvdsr 17881 df-unit 17882 df-invr 17912 df-dvr 17923 df-drng 17989 df-subrg 18018 df-abv 18057 df-cnfld 18983

This theorem is referenced by: ostth2lem3 24485

W3C validator