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 24551

Description: Lemma for ostth2 24554. (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 6316	. . . . . . . . 9
2	1	oveq1d 6323	. . . . . . . 8
3	2	oveq2d 6324	. . . . . . 7
4		oveq2 6316	. . . . . . . . 9
5		oveq2 6316	. . . . . . . . 9
6	4, 5	oveq12d 6326	. . . . . . . 8
7	6	breq2d 4407	. . . . . . 7
8	3, 7	raleqbidv 2987	. . . . . 6
9	8	imbi2d 323	. . . . 5
10		oveq2 6316	. . . . . . . . 9
11	10	oveq1d 6323	. . . . . . . 8
12	11	oveq2d 6324	. . . . . . 7
13		oveq2 6316	. . . . . . . . 9
14		oveq2 6316	. . . . . . . . 9
15	13, 14	oveq12d 6326	. . . . . . . 8
16	15	breq2d 4407	. . . . . . 7
17	12, 16	raleqbidv 2987	. . . . . 6
18	17	imbi2d 323	. . . . 5
19		oveq2 6316	. . . . . . . . 9
20	19	oveq1d 6323	. . . . . . . 8
21	20	oveq2d 6324	. . . . . . 7
22		oveq2 6316	. . . . . . . . 9
23		oveq2 6316	. . . . . . . . 9
24	22, 23	oveq12d 6326	. . . . . . . 8
25	24	breq2d 4407	. . . . . . 7
26	21, 25	raleqbidv 2987	. . . . . 6
27	26	imbi2d 323	. . . . 5
28		oveq2 6316	. . . . . . . . 9
29	28	oveq1d 6323	. . . . . . . 8
30	29	oveq2d 6324	. . . . . . 7
31		oveq2 6316	. . . . . . . . 9
32		oveq2 6316	. . . . . . . . 9
33	31, 32	oveq12d 6326	. . . . . . . 8
34	33	breq2d 4407	. . . . . . 7
35	30, 34	raleqbidv 2987	. . . . . 6
36	35	imbi2d 323	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2nn 11221	. . . . . . . . . . . . . 14
39	37, 38	syl 17	. . . . . . . . . . . . 13
40	39	nncnd 10647	. . . . . . . . . . . 12
41	40	exp0d 12448	. . . . . . . . . . 11
42	41	oveq1d 6323	. . . . . . . . . 10
43		1m1e0 10700	. . . . . . . . . 10
44	42, 43	syl6eq 2521	. . . . . . . . 9
45	44	oveq2d 6324	. . . . . . . 8
46	45	eleq2d 2534	. . . . . . 7
47		0le0 10721	. . . . . . . . . 10
48	47	a1i 11	. . . . . . . . 9
49		ostth.1	. . . . . . . . . 10
50		qabsabv.a	. . . . . . . . . . 11 AbsVal
51		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
52	51	qrng0 24538	. . . . . . . . . . 11
53	50, 52	abv0 18137	. . . . . . . . . 10
54	49, 53	syl 17	. . . . . . . . 9
55	40	mul01d 9850	. . . . . . . . . . 11
56	55	oveq1d 6323	. . . . . . . . . 10
57		ostth2.7	. . . . . . . . . . . . . 14
58		1re 9660	. . . . . . . . . . . . . . 15
59		nnq 11300	. . . . . . . . . . . . . . . . 17
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16
61	51	qrngbas 24536	. . . . . . . . . . . . . . . . 17
62	50, 61	abvcl 18130	. . . . . . . . . . . . . . . 16 $/\$
63	49, 60, 62	syl2anc 673	. . . . . . . . . . . . . . 15
64		ifcl 3914	. . . . . . . . . . . . . . 15 $/\$
65	58, 63, 64	sylancr 676	. . . . . . . . . . . . . 14
66	57, 65	syl5eqel 2553	. . . . . . . . . . . . 13
67	66	recnd 9687	. . . . . . . . . . . 12
68		0nn0 10908	. . . . . . . . . . . 12
69		expcl 12328	. . . . . . . . . . . 12 $/\$
70	67, 68, 69	sylancl 675	. . . . . . . . . . 11
71	70	mul02d 9849	. . . . . . . . . 10
72	56, 71	eqtrd 2505	. . . . . . . . 9
73	48, 54, 72	3brtr4d 4426	. . . . . . . 8
74		elfz1eq 11836	. . . . . . . . . 10
75	74	fveq2d 5883	. . . . . . . . 9
76	75	breq1d 4405	. . . . . . . 8
77	73, 76	syl5ibrcom 230	. . . . . . 7
78	46, 77	sylbid 223	. . . . . 6
79	78	ralrimiv 2808	. . . . 5
80		fveq2 5879	. . . . . . . . . 10
81	80	breq1d 4405	. . . . . . . . 9
82	81	cbvralv 3005	. . . . . . . 8
83	49	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84		elfzelz 11826	. . . . . . . . . . . . . 14
85	84	ad2antrl 742	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
86		zq 11293	. . . . . . . . . . . . 13
87	85, 86	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88	50, 61	abvcl 18130	. . . . . . . . . . . 12 $/\$
89	83, 87, 88	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90	39	ad2antrr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91		simplr 770	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92	90, 91	nnexpcld 12475	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
93	85, 92	zmodcld 12150	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	93	nn0zd 11061	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
95		zq 11293	. . . . . . . . . . . . . 14
96	94, 95	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
97	50, 61	abvcl 18130	. . . . . . . . . . . . 13 $/\$
98	83, 96, 97	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	83, 99, 62	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100, 91	reexpcld 12471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
102	85	zred 11063	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 92	nndivred 10680	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	103	flcld 12067	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		zq 11293	. . . . . . . . . . . . . . 15
106	104, 105	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	50, 61	abvcl 18130	. . . . . . . . . . . . . 14 $/\$
108	83, 106, 107	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	101, 108	remulcld 9689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	98, 109	readdcld 9688	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	90	nnred 10646	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
112		nn0p1nn 10933	. . . . . . . . . . . . . . 15
113	112	ad2antlr 741	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	113	nnred 10646	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	111, 114	remulcld 9689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
116	66	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		peano2nn0 10934	. . . . . . . . . . . . . 14
118	117	ad2antlr 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
119	116, 118	reexpcld 12471	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	115, 119	remulcld 9689	. . . . . . . . . . 11 $/\$ $/\$ $/\$
121		nnq 11300	. . . . . . . . . . . . . . 15
122	92, 121	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123		qmulcl 11305	. . . . . . . . . . . . . 14 $/\$
124	122, 106, 123	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125		qex 11299	. . . . . . . . . . . . . . 15
126		cnfldadd 19052	. . . . . . . . . . . . . . . 16 ℂ_fld
127	51, 126	ressplusg 15317	. . . . . . . . . . . . . . 15
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14
129	50, 61, 128	abvtri 18136	. . . . . . . . . . . . 13 $/\$ $/\$
130	83, 96, 124, 129	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	92	nnrpd 11362	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
132		modval 12131	. . . . . . . . . . . . . . . 16 $/\$
133	102, 131, 132	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
134	133	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
135	102	recnd 9687	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		qcn 11301	. . . . . . . . . . . . . . . 16
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	135, 137	npcand 10009	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	134, 138	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139	fveq2d 5883	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141		cnfldmul 19053	. . . . . . . . . . . . . . . . . 18 ℂ_fld
142	51, 141	ressmulr 15328	. . . . . . . . . . . . . . . . 17
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16
144	50, 61, 143	abvmul 18135	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	83, 122, 106, 144	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	51, 50	qabvexp 24543	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	83, 99, 91, 146	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148	147	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	145, 148	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	149	oveq2d 6324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	130, 140, 150	3brtr3d 4425	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	116, 91	reexpcld 12471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	115, 152	remulcld 9689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154		nn0re 10902	. . . . . . . . . . . . . . . . 17
155	154	ad2antlr 741	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	111, 155	remulcld 9689	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 152	remulcld 9689	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	111, 152	remulcld 9689	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		zmodfz 12151	. . . . . . . . . . . . . . . 16 $/\$
160	85, 92, 159	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
161		simprr 774	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		fveq2 5879	. . . . . . . . . . . . . . . . 17
163	162	breq1d 4405	. . . . . . . . . . . . . . . 16
164	163	rspcv 3132	. . . . . . . . . . . . . . 15
165	160, 161, 164	sylc 61	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
166	111, 101	remulcld 9689	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167	101	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
168	108	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	167, 168	mulcomd 9682	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
170	50, 61	abvge0 18131	. . . . . . . . . . . . . . . . . . 19 $/\$
171	83, 99, 170	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
172	100, 91, 171	expge0d 12472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
173	104	zred 11063	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
174		elfzle1 11828	. . . . . . . . . . . . . . . . . . . . . 22
175	174	ad2antrl 742	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
176	92	nnred 10646	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	92	nngt0d 10675	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178		divge0 10496	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179	102, 175, 176, 177, 178	syl22anc 1293	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
180		flge0nn0 12087	. . . . . . . . . . . . . . . . . . . 20 $/\$
181	103, 179, 180	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	51, 50	qabvle 24542	. . . . . . . . . . . . . . . . . . 19 $/\$
183	83, 181, 182	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
185		0z 10972	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	90, 118	nnexpcld 12475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
187	186	nnzd 11062	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188		elfzm11 11891	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189	185, 187, 188	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
190	184, 189	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	simp3d 1044	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
192	90	nncnd 10647	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
193	192, 91	expp1d 12455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
194	191, 193	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
195		ltdivmul 10502	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
196	102, 111, 176, 177, 195	syl112anc 1296	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
197	194, 196	mpbird 240	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	90	nnzd 11062	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		fllt 12075	. . . . . . . . . . . . . . . . . . . . 21 $/\$
200	103, 198, 199	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	197, 200	mpbid 215	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202	173, 111, 201	ltled 9800	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	108, 173, 111, 183, 202	letrd 9809	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
204	108, 111, 101, 172, 203	lemul1ad 10568	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
205	169, 204	eqbrtrd 4416	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
206	90	nnnn0d 10949	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	nn0ge0d 10952	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208		max1 11503	. . . . . . . . . . . . . . . . . . 19 $/\$
209	100, 58, 208	sylancl 675	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
210	209, 57	syl6breqr 4436	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211		leexp1a 12369	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	100, 116, 91, 171, 210, 211	syl32anc 1300	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
213	101, 152, 111, 207, 212	lemul2ad 10569	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
214	109, 166, 158, 205, 213	letrd 9809	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	98, 109, 157, 158, 165, 214	le2addd 10253	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
216		nn0cn 10903	. . . . . . . . . . . . . . . . . 18
217	216	ad2antlr 741	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
218		1cnd 9677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219	192, 217, 218	adddid 9685	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
220	192	mulid1d 9678	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	220	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	219, 221	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
223	222	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
224	192, 217	mulcld 9681	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	152	recnd 9687	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	224, 192, 225	adddird 9686	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
227	223, 226	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
228	215, 227	breqtrrd 4422	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
229		max2 11505	. . . . . . . . . . . . . . . 16 $/\$
230	100, 58, 229	sylancl 675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	230, 57	syl6breqr 4436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
232		nn0z 10984	. . . . . . . . . . . . . . . . 17
233	232	ad2antlr 741	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
234		uzid 11197	. . . . . . . . . . . . . . . 16
235	233, 234	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
236		peano2uz 11235	. . . . . . . . . . . . . . 15
237	235, 236	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
238	116, 231, 237	leexp2ad 12486	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
239	90, 113	nnmulcld 10679	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	239	nngt0d 10675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241		lemul2 10480	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
242	152, 119, 115, 240, 241	syl112anc 1296	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
243	238, 242	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
244	110, 153, 120, 228, 243	letrd 9809	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	89, 110, 120, 151, 244	letrd 9809	. . . . . . . . . 10 $/\$ $/\$ $/\$
246	245	expr 626	. . . . . . . . 9 $/\$ $/\$
247	246	ralrimdva 2812	. . . . . . . 8 $/\$
248	82, 247	syl5bi 225	. . . . . . 7 $/\$
249	248	expcom 442	. . . . . 6
250	249	a2d 28	. . . . 5
251	9, 18, 27, 36, 79, 250	nn0ind 11053	. . . 4
252	251	impcom 437	. . 3 $/\$
253		fveq2 5879	. . . . 5
254	253	breq1d 4405	. . . 4
255	254	rspccv 3133	. . 3
256	252, 255	syl 17	. 2 $/\$
257	256	3impia 1228	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

cvv 3031

cif 3872 class class class wbr 4395

cmpt 4454

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

cq 11287

crp 11325

cfz 11810

cfl 12059

cmo 12129

cexp 12310

cprime 14701

cpc 14865 ↾_s cress 15200

cplusg 15268

cmulr 15269 AbsValcabv 18122 ℂ_fldccnfld 19047

clog 23583

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-tpos 6991 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-ico 11666 df-fz 11811 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-0g 15418 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-grp 16751 df-minusg 16752 df-subg 16892 df-cmn 17510 df-mgp 17802 df-ur 17814 df-ring 17860 df-cring 17861 df-oppr 17929 df-dvdsr 17947 df-unit 17948 df-invr 17978 df-dvr 17989 df-drng 18055 df-subrg 18084 df-abv 18123 df-cnfld 19048

This theorem is referenced by: ostth2lem3 24552

W3C validator