ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 23684

Description: Lemma for ostth2 23687. (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 6285	. . . . . . . . 9
2	1	oveq1d 6292	. . . . . . . 8
3	2	oveq2d 6293	. . . . . . 7
4		oveq2 6285	. . . . . . . . 9
5		oveq2 6285	. . . . . . . . 9
6	4, 5	oveq12d 6295	. . . . . . . 8
7	6	breq2d 4445	. . . . . . 7
8	3, 7	raleqbidv 3052	. . . . . 6
9	8	imbi2d 316	. . . . 5
10		oveq2 6285	. . . . . . . . 9
11	10	oveq1d 6292	. . . . . . . 8
12	11	oveq2d 6293	. . . . . . 7
13		oveq2 6285	. . . . . . . . 9
14		oveq2 6285	. . . . . . . . 9
15	13, 14	oveq12d 6295	. . . . . . . 8
16	15	breq2d 4445	. . . . . . 7
17	12, 16	raleqbidv 3052	. . . . . 6
18	17	imbi2d 316	. . . . 5
19		oveq2 6285	. . . . . . . . 9
20	19	oveq1d 6292	. . . . . . . 8
21	20	oveq2d 6293	. . . . . . 7
22		oveq2 6285	. . . . . . . . 9
23		oveq2 6285	. . . . . . . . 9
24	22, 23	oveq12d 6295	. . . . . . . 8
25	24	breq2d 4445	. . . . . . 7
26	21, 25	raleqbidv 3052	. . . . . 6
27	26	imbi2d 316	. . . . 5
28		oveq2 6285	. . . . . . . . 9
29	28	oveq1d 6292	. . . . . . . 8
30	29	oveq2d 6293	. . . . . . 7
31		oveq2 6285	. . . . . . . . 9
32		oveq2 6285	. . . . . . . . 9
33	31, 32	oveq12d 6295	. . . . . . . 8
34	33	breq2d 4445	. . . . . . 7
35	30, 34	raleqbidv 3052	. . . . . 6
36	35	imbi2d 316	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2nn 11123	. . . . . . . . . . . . . 14
39	37, 38	syl 16	. . . . . . . . . . . . 13
40	39	nncnd 10553	. . . . . . . . . . . 12
41	40	exp0d 12278	. . . . . . . . . . 11
42	41	oveq1d 6292	. . . . . . . . . 10
43		1m1e0 10605	. . . . . . . . . 10
44	42, 43	syl6eq 2498	. . . . . . . . 9
45	44	oveq2d 6293	. . . . . . . 8
46	45	eleq2d 2511	. . . . . . 7
47		0le0 10626	. . . . . . . . . 10
48	47	a1i 11	. . . . . . . . 9
49		ostth.1	. . . . . . . . . 10
50		qabsabv.a	. . . . . . . . . . 11 AbsVal
51		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
52	51	qrng0 23671	. . . . . . . . . . 11
53	50, 52	abv0 17348	. . . . . . . . . 10
54	49, 53	syl 16	. . . . . . . . 9
55	40	mul01d 9777	. . . . . . . . . . 11
56	55	oveq1d 6292	. . . . . . . . . 10
57		ostth2.7	. . . . . . . . . . . . . 14
58		1re 9593	. . . . . . . . . . . . . . 15
59		nnq 11199	. . . . . . . . . . . . . . . . 17
60	39, 59	syl 16	. . . . . . . . . . . . . . . 16
61	51	qrngbas 23669	. . . . . . . . . . . . . . . . 17
62	50, 61	abvcl 17341	. . . . . . . . . . . . . . . 16 $/\$
63	49, 60, 62	syl2anc 661	. . . . . . . . . . . . . . 15
64		ifcl 3964	. . . . . . . . . . . . . . 15 $/\$
65	58, 63, 64	sylancr 663	. . . . . . . . . . . . . 14
66	57, 65	syl5eqel 2533	. . . . . . . . . . . . 13
67	66	recnd 9620	. . . . . . . . . . . 12
68		0nn0 10811	. . . . . . . . . . . 12
69		expcl 12158	. . . . . . . . . . . 12 $/\$
70	67, 68, 69	sylancl 662	. . . . . . . . . . 11
71	70	mul02d 9776	. . . . . . . . . 10
72	56, 71	eqtrd 2482	. . . . . . . . 9
73	48, 54, 72	3brtr4d 4463	. . . . . . . 8
74		elfz1eq 11701	. . . . . . . . . 10
75	74	fveq2d 5856	. . . . . . . . 9
76	75	breq1d 4443	. . . . . . . 8
77	73, 76	syl5ibrcom 222	. . . . . . 7
78	46, 77	sylbid 215	. . . . . 6
79	78	ralrimiv 2853	. . . . 5
80		fveq2 5852	. . . . . . . . . 10
81	80	breq1d 4443	. . . . . . . . 9
82	81	cbvralv 3068	. . . . . . . 8
83	49	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84		elfzelz 11692	. . . . . . . . . . . . . 14
85	84	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
86		zq 11192	. . . . . . . . . . . . 13
87	85, 86	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88	50, 61	abvcl 17341	. . . . . . . . . . . 12 $/\$
89	83, 87, 88	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90	39	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91		simplr 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92	90, 91	nnexpcld 12305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
93	85, 92	zmodcld 11990	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	93	nn0zd 10967	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
95		zq 11192	. . . . . . . . . . . . . 14
96	94, 95	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	50, 61	abvcl 17341	. . . . . . . . . . . . 13 $/\$
98	83, 96, 97	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	90, 59	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	83, 99, 62	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100, 91	reexpcld 12301	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
102	85	zred 10969	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 92	nndivred 10585	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	103	flcld 11909	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		zq 11192	. . . . . . . . . . . . . . 15
106	104, 105	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	50, 61	abvcl 17341	. . . . . . . . . . . . . 14 $/\$
108	83, 106, 107	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	101, 108	remulcld 9622	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	98, 109	readdcld 9621	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	90	nnred 10552	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
112		nn0p1nn 10836	. . . . . . . . . . . . . . 15
113	112	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	113	nnred 10552	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	111, 114	remulcld 9622	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
116	66	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		peano2nn0 10837	. . . . . . . . . . . . . 14
118	117	ad2antlr 726	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
119	116, 118	reexpcld 12301	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	115, 119	remulcld 9622	. . . . . . . . . . 11 $/\$ $/\$ $/\$
121		nnq 11199	. . . . . . . . . . . . . . 15
122	92, 121	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123		qmulcl 11204	. . . . . . . . . . . . . 14 $/\$
124	122, 106, 123	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125		qex 11198	. . . . . . . . . . . . . . 15
126		cnfldadd 18293	. . . . . . . . . . . . . . . 16 ℂ_fld
127	51, 126	ressplusg 14611	. . . . . . . . . . . . . . 15
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14
129	50, 61, 128	abvtri 17347	. . . . . . . . . . . . 13 $/\$ $/\$
130	83, 96, 124, 129	syl3anc 1227	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	92	nnrpd 11259	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
132		modval 11972	. . . . . . . . . . . . . . . 16 $/\$
133	102, 131, 132	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
134	133	oveq1d 6292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
135	102	recnd 9620	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		qcn 11200	. . . . . . . . . . . . . . . 16
137	124, 136	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	135, 137	npcand 9935	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	134, 138	eqtrd 2482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139	fveq2d 5856	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141		cnfldmul 18294	. . . . . . . . . . . . . . . . . 18 ℂ_fld
142	51, 141	ressmulr 14622	. . . . . . . . . . . . . . . . 17
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16
144	50, 61, 143	abvmul 17346	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	83, 122, 106, 144	syl3anc 1227	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	51, 50	qabvexp 23676	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	83, 99, 91, 146	syl3anc 1227	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148	147	oveq1d 6292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	145, 148	eqtrd 2482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	149	oveq2d 6293	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	130, 140, 150	3brtr3d 4462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	116, 91	reexpcld 12301	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	115, 152	remulcld 9622	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154		nn0re 10805	. . . . . . . . . . . . . . . . 17
155	154	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	111, 155	remulcld 9622	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 152	remulcld 9622	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	111, 152	remulcld 9622	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		zmodfz 11991	. . . . . . . . . . . . . . . 16 $/\$
160	85, 92, 159	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
161		simprr 756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		fveq2 5852	. . . . . . . . . . . . . . . . 17
163	162	breq1d 4443	. . . . . . . . . . . . . . . 16
164	163	rspcv 3190	. . . . . . . . . . . . . . 15
165	160, 161, 164	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166	111, 101	remulcld 9622	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167	101	recnd 9620	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
168	108	recnd 9620	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	167, 168	mulcomd 9615	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
170	50, 61	abvge0 17342	. . . . . . . . . . . . . . . . . . 19 $/\$
171	83, 99, 170	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
172	100, 91, 171	expge0d 12302	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
173	104	zred 10969	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
174		elfzle1 11693	. . . . . . . . . . . . . . . . . . . . . 22
175	174	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
176	92	nnred 10552	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	92	nngt0d 10580	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178		divge0 10412	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179	102, 175, 176, 177, 178	syl22anc 1228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
180		flge0nn0 11928	. . . . . . . . . . . . . . . . . . . 20 $/\$
181	103, 179, 180	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	51, 50	qabvle 23675	. . . . . . . . . . . . . . . . . . 19 $/\$
183	83, 181, 182	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
185		0z 10876	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	90, 118	nnexpcld 12305	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
187	186	nnzd 10968	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188		elfzm11 11753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189	185, 187, 188	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
190	184, 189	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	simp3d 1009	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
192	90	nncnd 10553	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
193	192, 91	expp1d 12285	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
194	191, 193	breqtrd 4457	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
195		ltdivmul 10418	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
196	102, 111, 176, 177, 195	syl112anc 1231	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
197	194, 196	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	90	nnzd 10968	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		fllt 11917	. . . . . . . . . . . . . . . . . . . . 21 $/\$
200	103, 198, 199	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	197, 200	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202	173, 111, 201	ltled 9731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	108, 173, 111, 183, 202	letrd 9737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
204	108, 111, 101, 172, 203	lemul1ad 10486	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
205	169, 204	eqbrtrd 4453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
206	90	nnnn0d 10853	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	nn0ge0d 10856	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208		max1 11390	. . . . . . . . . . . . . . . . . . 19 $/\$
209	100, 58, 208	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
210	209, 57	syl6breqr 4473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211		leexp1a 12198	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	100, 116, 91, 171, 210, 211	syl32anc 1235	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
213	101, 152, 111, 207, 212	lemul2ad 10487	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
214	109, 166, 158, 205, 213	letrd 9737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	98, 109, 157, 158, 165, 214	le2addd 10171	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
216		nn0cn 10806	. . . . . . . . . . . . . . . . . 18
217	216	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
218		1cnd 9610	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219	192, 217, 218	adddid 9618	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
220	192	mulid1d 9611	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	220	oveq2d 6293	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	219, 221	eqtrd 2482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
223	222	oveq1d 6292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
224	192, 217	mulcld 9614	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	152	recnd 9620	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	224, 192, 225	adddird 9619	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
227	223, 226	eqtrd 2482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
228	215, 227	breqtrrd 4459	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
229		max2 11392	. . . . . . . . . . . . . . . 16 $/\$
230	100, 58, 229	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	230, 57	syl6breqr 4473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
232		nn0z 10888	. . . . . . . . . . . . . . . . 17
233	232	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
234		uzid 11099	. . . . . . . . . . . . . . . 16
235	233, 234	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
236		peano2uz 11138	. . . . . . . . . . . . . . 15
237	235, 236	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
238	116, 231, 237	leexp2ad 12316	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
239	90, 113	nnmulcld 10584	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	239	nngt0d 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241		lemul2 10396	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
242	152, 119, 115, 240, 241	syl112anc 1231	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
243	238, 242	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
244	110, 153, 120, 228, 243	letrd 9737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	89, 110, 120, 151, 244	letrd 9737	. . . . . . . . . 10 $/\$ $/\$ $/\$
246	245	expr 615	. . . . . . . . 9 $/\$ $/\$
247	246	ralrimdva 2859	. . . . . . . 8 $/\$
248	82, 247	syl5bi 217	. . . . . . 7 $/\$
249	248	expcom 435	. . . . . 6
250	249	a2d 26	. . . . 5
251	9, 18, 27, 36, 79, 250	nn0ind 10960	. . . 4
252	251	impcom 430	. . 3 $/\$
253		fveq2 5852	. . . . 5
254	253	breq1d 4443	. . . 4
255	254	rspccv 3191	. . 3
256	252, 255	syl 16	. 2 $/\$
257	256	3impia 1192	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1381

wcel 1802

wral 2791

cvv 3093

cif 3922 class class class wbr 4433

cmpt 4491

cfv 5574 (class class class)co 6277

cc 9488

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

clt 9626

cle 9627

cmin 9805

cneg 9806

cdiv 10207

cn 10537

c2 10586

cn0 10796

cz 10865

cuz 11085

cq 11186

crp 11224

cfz 11676

cfl 11901

cmo 11970

cexp 12140

cprime 14089

cpc 14232 ↾_s cress 14505

cplusg 14569

cmulr 14570 AbsValcabv 17333 ℂ_fldccnfld 18288

clog 22807

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568 ax-addf 9569 ax-mulf 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-int 4268 df-iun 4313 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6682 df-1st 6781 df-2nd 6782 df-tpos 6953 df-recs 7040 df-rdg 7074 df-1o 7128 df-oadd 7132 df-er 7309 df-map 7420 df-en 7515 df-dom 7516 df-sdom 7517 df-fin 7518 df-sup 7899 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-4 10597 df-5 10598 df-6 10599 df-7 10600 df-8 10601 df-9 10602 df-10 10603 df-n0 10797 df-z 10866 df-dec 10980 df-uz 11086 df-q 11187 df-rp 11225 df-ico 11539 df-fz 11677 df-fl 11903 df-mod 11971 df-seq 12082 df-exp 12141 df-struct 14506 df-ndx 14507 df-slot 14508 df-base 14509 df-sets 14510 df-ress 14511 df-plusg 14582 df-mulr 14583 df-starv 14584 df-tset 14588 df-ple 14589 df-ds 14591 df-unif 14592 df-0g 14711 df-mgm 15741 df-sgrp 15780 df-mnd 15790 df-grp 15926 df-minusg 15927 df-subg 16067 df-cmn 16669 df-mgp 17010 df-ur 17022 df-ring 17068 df-cring 17069 df-oppr 17140 df-dvdsr 17158 df-unit 17159 df-invr 17189 df-dvr 17200 df-drng 17266 df-subrg 17295 df-abv 17334 df-cnfld 18289

This theorem is referenced by: ostth2lem3 23685

W3C validator