ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 23936

Description: Lemma for ostth2 23939. (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 6204	. . . . . . . . 9
2	1	oveq1d 6211	. . . . . . . 8
3	2	oveq2d 6212	. . . . . . 7
4		oveq2 6204	. . . . . . . . 9
5		oveq2 6204	. . . . . . . . 9
6	4, 5	oveq12d 6214	. . . . . . . 8
7	6	breq2d 4379	. . . . . . 7
8	3, 7	raleqbidv 2993	. . . . . 6
9	8	imbi2d 314	. . . . 5
10		oveq2 6204	. . . . . . . . 9
11	10	oveq1d 6211	. . . . . . . 8
12	11	oveq2d 6212	. . . . . . 7
13		oveq2 6204	. . . . . . . . 9
14		oveq2 6204	. . . . . . . . 9
15	13, 14	oveq12d 6214	. . . . . . . 8
16	15	breq2d 4379	. . . . . . 7
17	12, 16	raleqbidv 2993	. . . . . 6
18	17	imbi2d 314	. . . . 5
19		oveq2 6204	. . . . . . . . 9
20	19	oveq1d 6211	. . . . . . . 8
21	20	oveq2d 6212	. . . . . . 7
22		oveq2 6204	. . . . . . . . 9
23		oveq2 6204	. . . . . . . . 9
24	22, 23	oveq12d 6214	. . . . . . . 8
25	24	breq2d 4379	. . . . . . 7
26	21, 25	raleqbidv 2993	. . . . . 6
27	26	imbi2d 314	. . . . 5
28		oveq2 6204	. . . . . . . . 9
29	28	oveq1d 6211	. . . . . . . 8
30	29	oveq2d 6212	. . . . . . 7
31		oveq2 6204	. . . . . . . . 9
32		oveq2 6204	. . . . . . . . 9
33	31, 32	oveq12d 6214	. . . . . . . 8
34	33	breq2d 4379	. . . . . . 7
35	30, 34	raleqbidv 2993	. . . . . 6
36	35	imbi2d 314	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2nn 11039	. . . . . . . . . . . . . 14
39	37, 38	syl 16	. . . . . . . . . . . . 13
40	39	nncnd 10468	. . . . . . . . . . . 12
41	40	exp0d 12206	. . . . . . . . . . 11
42	41	oveq1d 6211	. . . . . . . . . 10
43		1m1e0 10521	. . . . . . . . . 10
44	42, 43	syl6eq 2439	. . . . . . . . 9
45	44	oveq2d 6212	. . . . . . . 8
46	45	eleq2d 2452	. . . . . . 7
47		0le0 10542	. . . . . . . . . 10
48	47	a1i 11	. . . . . . . . 9
49		ostth.1	. . . . . . . . . 10
50		qabsabv.a	. . . . . . . . . . 11 AbsVal
51		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
52	51	qrng0 23923	. . . . . . . . . . 11
53	50, 52	abv0 17593	. . . . . . . . . 10
54	49, 53	syl 16	. . . . . . . . 9
55	40	mul01d 9690	. . . . . . . . . . 11
56	55	oveq1d 6211	. . . . . . . . . 10
57		ostth2.7	. . . . . . . . . . . . . 14
58		1re 9506	. . . . . . . . . . . . . . 15
59		nnq 11114	. . . . . . . . . . . . . . . . 17
60	39, 59	syl 16	. . . . . . . . . . . . . . . 16
61	51	qrngbas 23921	. . . . . . . . . . . . . . . . 17
62	50, 61	abvcl 17586	. . . . . . . . . . . . . . . 16 $/\$
63	49, 60, 62	syl2anc 659	. . . . . . . . . . . . . . 15
64		ifcl 3899	. . . . . . . . . . . . . . 15 $/\$
65	58, 63, 64	sylancr 661	. . . . . . . . . . . . . 14
66	57, 65	syl5eqel 2474	. . . . . . . . . . . . 13
67	66	recnd 9533	. . . . . . . . . . . 12
68		0nn0 10727	. . . . . . . . . . . 12
69		expcl 12087	. . . . . . . . . . . 12 $/\$
70	67, 68, 69	sylancl 660	. . . . . . . . . . 11
71	70	mul02d 9689	. . . . . . . . . 10
72	56, 71	eqtrd 2423	. . . . . . . . 9
73	48, 54, 72	3brtr4d 4397	. . . . . . . 8
74		elfz1eq 11618	. . . . . . . . . 10
75	74	fveq2d 5778	. . . . . . . . 9
76	75	breq1d 4377	. . . . . . . 8
77	73, 76	syl5ibrcom 222	. . . . . . 7
78	46, 77	sylbid 215	. . . . . 6
79	78	ralrimiv 2794	. . . . 5
80		fveq2 5774	. . . . . . . . . 10
81	80	breq1d 4377	. . . . . . . . 9
82	81	cbvralv 3009	. . . . . . . 8
83	49	ad2antrr 723	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84		elfzelz 11609	. . . . . . . . . . . . . 14
85	84	ad2antrl 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
86		zq 11107	. . . . . . . . . . . . 13
87	85, 86	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88	50, 61	abvcl 17586	. . . . . . . . . . . 12 $/\$
89	83, 87, 88	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90	39	ad2antrr 723	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91		simplr 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92	90, 91	nnexpcld 12233	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
93	85, 92	zmodcld 11917	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	93	nn0zd 10882	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
95		zq 11107	. . . . . . . . . . . . . 14
96	94, 95	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	50, 61	abvcl 17586	. . . . . . . . . . . . 13 $/\$
98	83, 96, 97	syl2anc 659	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	90, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	83, 99, 62	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100, 91	reexpcld 12229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
102	85	zred 10884	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 92	nndivred 10501	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	103	flcld 11834	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		zq 11107	. . . . . . . . . . . . . . 15
106	104, 105	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	50, 61	abvcl 17586	. . . . . . . . . . . . . 14 $/\$
108	83, 106, 107	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	101, 108	remulcld 9535	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	98, 109	readdcld 9534	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	90	nnred 10467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
112		nn0p1nn 10752	. . . . . . . . . . . . . . 15
113	112	ad2antlr 724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	113	nnred 10467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	111, 114	remulcld 9535	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
116	66	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		peano2nn0 10753	. . . . . . . . . . . . . 14
118	117	ad2antlr 724	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
119	116, 118	reexpcld 12229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	115, 119	remulcld 9535	. . . . . . . . . . 11 $/\$ $/\$ $/\$
121		nnq 11114	. . . . . . . . . . . . . . 15
122	92, 121	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123		qmulcl 11119	. . . . . . . . . . . . . 14 $/\$
124	122, 106, 123	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125		qex 11113	. . . . . . . . . . . . . . 15
126		cnfldadd 18538	. . . . . . . . . . . . . . . 16 ℂ_fld
127	51, 126	ressplusg 14748	. . . . . . . . . . . . . . 15
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14
129	50, 61, 128	abvtri 17592	. . . . . . . . . . . . 13 $/\$ $/\$
130	83, 96, 124, 129	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	92	nnrpd 11175	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
132		modval 11898	. . . . . . . . . . . . . . . 16 $/\$
133	102, 131, 132	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
134	133	oveq1d 6211	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
135	102	recnd 9533	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		qcn 11115	. . . . . . . . . . . . . . . 16
137	124, 136	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	135, 137	npcand 9848	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	134, 138	eqtrd 2423	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139	fveq2d 5778	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141		cnfldmul 18539	. . . . . . . . . . . . . . . . . 18 ℂ_fld
142	51, 141	ressmulr 14759	. . . . . . . . . . . . . . . . 17
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16
144	50, 61, 143	abvmul 17591	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	83, 122, 106, 144	syl3anc 1226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	51, 50	qabvexp 23928	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	83, 99, 91, 146	syl3anc 1226	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148	147	oveq1d 6211	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	145, 148	eqtrd 2423	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	149	oveq2d 6212	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	130, 140, 150	3brtr3d 4396	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	116, 91	reexpcld 12229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	115, 152	remulcld 9535	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154		nn0re 10721	. . . . . . . . . . . . . . . . 17
155	154	ad2antlr 724	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	111, 155	remulcld 9535	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 152	remulcld 9535	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	111, 152	remulcld 9535	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		zmodfz 11918	. . . . . . . . . . . . . . . 16 $/\$
160	85, 92, 159	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
161		simprr 755	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		fveq2 5774	. . . . . . . . . . . . . . . . 17
163	162	breq1d 4377	. . . . . . . . . . . . . . . 16
164	163	rspcv 3131	. . . . . . . . . . . . . . 15
165	160, 161, 164	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166	111, 101	remulcld 9535	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167	101	recnd 9533	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
168	108	recnd 9533	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	167, 168	mulcomd 9528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
170	50, 61	abvge0 17587	. . . . . . . . . . . . . . . . . . 19 $/\$
171	83, 99, 170	syl2anc 659	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
172	100, 91, 171	expge0d 12230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
173	104	zred 10884	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
174		elfzle1 11610	. . . . . . . . . . . . . . . . . . . . . 22
175	174	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
176	92	nnred 10467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	92	nngt0d 10496	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178		divge0 10328	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179	102, 175, 176, 177, 178	syl22anc 1227	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
180		flge0nn0 11854	. . . . . . . . . . . . . . . . . . . 20 $/\$
181	103, 179, 180	syl2anc 659	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	51, 50	qabvle 23927	. . . . . . . . . . . . . . . . . . 19 $/\$
183	83, 181, 182	syl2anc 659	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184		simprl 754	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
185		0z 10792	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	90, 118	nnexpcld 12233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
187	186	nnzd 10883	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188		elfzm11 11671	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189	185, 187, 188	sylancr 661	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
190	184, 189	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	simp3d 1008	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
192	90	nncnd 10468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
193	192, 91	expp1d 12213	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
194	191, 193	breqtrd 4391	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
195		ltdivmul 10334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
196	102, 111, 176, 177, 195	syl112anc 1230	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
197	194, 196	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	90	nnzd 10883	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		fllt 11842	. . . . . . . . . . . . . . . . . . . . 21 $/\$
200	103, 198, 199	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	197, 200	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202	173, 111, 201	ltled 9644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	108, 173, 111, 183, 202	letrd 9650	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
204	108, 111, 101, 172, 203	lemul1ad 10401	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
205	169, 204	eqbrtrd 4387	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
206	90	nnnn0d 10769	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	nn0ge0d 10772	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208		max1 11307	. . . . . . . . . . . . . . . . . . 19 $/\$
209	100, 58, 208	sylancl 660	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
210	209, 57	syl6breqr 4407	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211		leexp1a 12127	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	100, 116, 91, 171, 210, 211	syl32anc 1234	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
213	101, 152, 111, 207, 212	lemul2ad 10402	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
214	109, 166, 158, 205, 213	letrd 9650	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	98, 109, 157, 158, 165, 214	le2addd 10087	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
216		nn0cn 10722	. . . . . . . . . . . . . . . . . 18
217	216	ad2antlr 724	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
218		1cnd 9523	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219	192, 217, 218	adddid 9531	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
220	192	mulid1d 9524	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	220	oveq2d 6212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	219, 221	eqtrd 2423	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
223	222	oveq1d 6211	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
224	192, 217	mulcld 9527	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	152	recnd 9533	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	224, 192, 225	adddird 9532	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
227	223, 226	eqtrd 2423	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
228	215, 227	breqtrrd 4393	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
229		max2 11309	. . . . . . . . . . . . . . . 16 $/\$
230	100, 58, 229	sylancl 660	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	230, 57	syl6breqr 4407	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
232		nn0z 10804	. . . . . . . . . . . . . . . . 17
233	232	ad2antlr 724	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
234		uzid 11015	. . . . . . . . . . . . . . . 16
235	233, 234	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
236		peano2uz 11054	. . . . . . . . . . . . . . 15
237	235, 236	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
238	116, 231, 237	leexp2ad 12244	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
239	90, 113	nnmulcld 10500	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	239	nngt0d 10496	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241		lemul2 10312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
242	152, 119, 115, 240, 241	syl112anc 1230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
243	238, 242	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
244	110, 153, 120, 228, 243	letrd 9650	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	89, 110, 120, 151, 244	letrd 9650	. . . . . . . . . 10 $/\$ $/\$ $/\$
246	245	expr 613	. . . . . . . . 9 $/\$ $/\$
247	246	ralrimdva 2800	. . . . . . . 8 $/\$
248	82, 247	syl5bi 217	. . . . . . 7 $/\$
249	248	expcom 433	. . . . . 6
250	249	a2d 26	. . . . 5
251	9, 18, 27, 36, 79, 250	nn0ind 10874	. . . 4
252	251	impcom 428	. . 3 $/\$
253		fveq2 5774	. . . . 5
254	253	breq1d 4377	. . . 4
255	254	rspccv 3132	. . 3
256	252, 255	syl 16	. 2 $/\$
257	256	3impia 1191	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wral 2732

cvv 3034

cif 3857 class class class wbr 4367

cmpt 4425

cfv 5496 (class class class)co 6196

cc 9401

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

clt 9539

cle 9540

cmin 9718

cneg 9719

cdiv 10123

cn 10452

c2 10502

cn0 10712

cz 10781

cuz 11001

cq 11101

crp 11139

cfz 11593

cfl 11826

cmo 11896

cexp 12069

cprime 14219

cpc 14362 ↾_s cress 14635

cplusg 14702

cmulr 14703 AbsValcabv 17578 ℂ_fldccnfld 18533

clog 23027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481 ax-addf 9482 ax-mulf 9483

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-tpos 6873 df-recs 6960 df-rdg 6994 df-1o 7048 df-oadd 7052 df-er 7229 df-map 7340 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-sup 7816 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-5 10514 df-6 10515 df-7 10516 df-8 10517 df-9 10518 df-10 10519 df-n0 10713 df-z 10782 df-dec 10896 df-uz 11002 df-q 11102 df-rp 11140 df-ico 11456 df-fz 11594 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-struct 14636 df-ndx 14637 df-slot 14638 df-base 14639 df-sets 14640 df-ress 14641 df-plusg 14715 df-mulr 14716 df-starv 14717 df-tset 14721 df-ple 14722 df-ds 14724 df-unif 14725 df-0g 14849 df-mgm 15989 df-sgrp 16028 df-mnd 16038 df-grp 16174 df-minusg 16175 df-subg 16315 df-cmn 16917 df-mgp 17255 df-ur 17267 df-ring 17313 df-cring 17314 df-oppr 17385 df-dvdsr 17403 df-unit 17404 df-invr 17434 df-dvr 17445 df-drng 17511 df-subrg 17540 df-abv 17579 df-cnfld 18534

This theorem is referenced by: ostth2lem3 23937

W3C validator