ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 22842

Description: Lemma for ostth2 22845. (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 6098	. . . . . . . . 9
2	1	oveq1d 6105	. . . . . . . 8
3	2	oveq2d 6106	. . . . . . 7
4		oveq2 6098	. . . . . . . . 9
5		oveq2 6098	. . . . . . . . 9
6	4, 5	oveq12d 6108	. . . . . . . 8
7	6	breq2d 4301	. . . . . . 7
8	3, 7	raleqbidv 2929	. . . . . 6
9	8	imbi2d 316	. . . . 5
10		oveq2 6098	. . . . . . . . 9
11	10	oveq1d 6105	. . . . . . . 8
12	11	oveq2d 6106	. . . . . . 7
13		oveq2 6098	. . . . . . . . 9
14		oveq2 6098	. . . . . . . . 9
15	13, 14	oveq12d 6108	. . . . . . . 8
16	15	breq2d 4301	. . . . . . 7
17	12, 16	raleqbidv 2929	. . . . . 6
18	17	imbi2d 316	. . . . 5
19		oveq2 6098	. . . . . . . . 9
20	19	oveq1d 6105	. . . . . . . 8
21	20	oveq2d 6106	. . . . . . 7
22		oveq2 6098	. . . . . . . . 9
23		oveq2 6098	. . . . . . . . 9
24	22, 23	oveq12d 6108	. . . . . . . 8
25	24	breq2d 4301	. . . . . . 7
26	21, 25	raleqbidv 2929	. . . . . 6
27	26	imbi2d 316	. . . . 5
28		oveq2 6098	. . . . . . . . 9
29	28	oveq1d 6105	. . . . . . . 8
30	29	oveq2d 6106	. . . . . . 7
31		oveq2 6098	. . . . . . . . 9
32		oveq2 6098	. . . . . . . . 9
33	31, 32	oveq12d 6108	. . . . . . . 8
34	33	breq2d 4301	. . . . . . 7
35	30, 34	raleqbidv 2929	. . . . . 6
36	35	imbi2d 316	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2b2 10923	. . . . . . . . . . . . . . 15 $/\$
39	38	simplbi 457	. . . . . . . . . . . . . 14
40	37, 39	syl 16	. . . . . . . . . . . . 13
41	40	nncnd 10334	. . . . . . . . . . . 12
42	41	exp0d 11998	. . . . . . . . . . 11
43	42	oveq1d 6105	. . . . . . . . . 10
44		1m1e0 10386	. . . . . . . . . 10
45	43, 44	syl6eq 2489	. . . . . . . . 9
46	45	oveq2d 6106	. . . . . . . 8
47	46	eleq2d 2508	. . . . . . 7
48		0le0 10407	. . . . . . . . . 10
49	48	a1i 11	. . . . . . . . 9
50		ostth.1	. . . . . . . . . 10
51		qabsabv.a	. . . . . . . . . . 11 AbsVal
52		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
53	52	qrng0 22829	. . . . . . . . . . 11
54	51, 53	abv0 16896	. . . . . . . . . 10
55	50, 54	syl 16	. . . . . . . . 9
56	41	mul01d 9564	. . . . . . . . . . 11
57	56	oveq1d 6105	. . . . . . . . . 10
58		ostth2.7	. . . . . . . . . . . . . 14
59		1re 9381	. . . . . . . . . . . . . . 15
60		nnq 10962	. . . . . . . . . . . . . . . . 17
61	40, 60	syl 16	. . . . . . . . . . . . . . . 16
62	52	qrngbas 22827	. . . . . . . . . . . . . . . . 17
63	51, 62	abvcl 16889	. . . . . . . . . . . . . . . 16 $/\$
64	50, 61, 63	syl2anc 656	. . . . . . . . . . . . . . 15
65		ifcl 3828	. . . . . . . . . . . . . . 15 $/\$
66	59, 64, 65	sylancr 658	. . . . . . . . . . . . . 14
67	58, 66	syl5eqel 2525	. . . . . . . . . . . . 13
68	67	recnd 9408	. . . . . . . . . . . 12
69		0nn0 10590	. . . . . . . . . . . 12
70		expcl 11879	. . . . . . . . . . . 12 $/\$
71	68, 69, 70	sylancl 657	. . . . . . . . . . 11
72	71	mul02d 9563	. . . . . . . . . 10
73	57, 72	eqtrd 2473	. . . . . . . . 9
74	49, 55, 73	3brtr4d 4319	. . . . . . . 8
75		elfz1eq 11458	. . . . . . . . . 10
76	75	fveq2d 5692	. . . . . . . . 9
77	76	breq1d 4299	. . . . . . . 8
78	74, 77	syl5ibrcom 222	. . . . . . 7
79	47, 78	sylbid 215	. . . . . 6
80	79	ralrimiv 2796	. . . . 5
81		fveq2 5688	. . . . . . . . . 10
82	81	breq1d 4299	. . . . . . . . 9
83	82	cbvralv 2945	. . . . . . . 8
84	50	ad2antrr 720	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
85		elfzelz 11449	. . . . . . . . . . . . . 14
86	85	ad2antrl 722	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
87		zq 10955	. . . . . . . . . . . . 13
88	86, 87	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
89	51, 62	abvcl 16889	. . . . . . . . . . . 12 $/\$
90	84, 88, 89	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$
91	40	ad2antrr 720	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		simplr 749	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
93	91, 92	nnexpcld 12025	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	86, 93	zmodcld 11724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nn0zd 10741	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		zq 10955	. . . . . . . . . . . . . 14
97	95, 96	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
98	51, 62	abvcl 16889	. . . . . . . . . . . . 13 $/\$
99	84, 97, 98	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	91, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
101	84, 100, 63	syl2anc 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101, 92	reexpcld 12021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
103	86	zred 10743	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
104	103, 93	nndivred 10366	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
105	104	flcld 11644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
106		zq 10955	. . . . . . . . . . . . . . 15
107	105, 106	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	51, 62	abvcl 16889	. . . . . . . . . . . . . 14 $/\$
109	84, 107, 108	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	102, 109	remulcld 9410	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
111	99, 110	readdcld 9409	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	91	nnred 10333	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
113		nn0p1nn 10615	. . . . . . . . . . . . . . 15
114	113	ad2antlr 721	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115	114	nnred 10333	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	112, 115	remulcld 9410	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117	67	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		peano2nn0 10616	. . . . . . . . . . . . . 14
119	118	ad2antlr 721	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	117, 119	reexpcld 12021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	116, 120	remulcld 9410	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122		nnq 10962	. . . . . . . . . . . . . . 15
123	93, 122	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		qmulcl 10967	. . . . . . . . . . . . . 14 $/\$
125	123, 107, 124	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126		qex 10961	. . . . . . . . . . . . . . 15
127		cnfldadd 17782	. . . . . . . . . . . . . . . 16 ℂ_fld
128	52, 127	ressplusg 14276	. . . . . . . . . . . . . . 15
129	126, 128	ax-mp 5	. . . . . . . . . . . . . 14
130	51, 62, 129	abvtri 16895	. . . . . . . . . . . . 13 $/\$ $/\$
131	84, 97, 125, 130	syl3anc 1213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
132	93	nnrpd 11022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
133		modval 11706	. . . . . . . . . . . . . . . 16 $/\$
134	103, 132, 133	syl2anc 656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
135	134	oveq1d 6105	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	103	recnd 9408	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137		qcn 10963	. . . . . . . . . . . . . . . 16
138	125, 137	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	136, 138	npcand 9719	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140	135, 139	eqtrd 2473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
141	140	fveq2d 5692	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
142		cnfldmul 17783	. . . . . . . . . . . . . . . . . 18 ℂ_fld
143	52, 142	ressmulr 14287	. . . . . . . . . . . . . . . . 17
144	126, 143	ax-mp 5	. . . . . . . . . . . . . . . 16
145	51, 62, 144	abvmul 16894	. . . . . . . . . . . . . . 15 $/\$ $/\$
146	84, 123, 107, 145	syl3anc 1213	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147	52, 51	qabvexp 22834	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	84, 100, 92, 147	syl3anc 1213	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	148	oveq1d 6105	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	146, 149	eqtrd 2473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	oveq2d 6106	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	131, 141, 151	3brtr3d 4318	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	117, 92	reexpcld 12021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154	116, 153	remulcld 9410	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
155		nn0re 10584	. . . . . . . . . . . . . . . . 17
156	155	ad2antlr 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
157	112, 156	remulcld 9410	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	157, 153	remulcld 9410	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159	112, 153	remulcld 9410	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160		zmodfz 11725	. . . . . . . . . . . . . . . 16 $/\$
161	86, 93, 160	syl2anc 656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		simprr 751	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163		fveq2 5688	. . . . . . . . . . . . . . . . 17
164	163	breq1d 4299	. . . . . . . . . . . . . . . 16
165	164	rspcv 3066	. . . . . . . . . . . . . . 15
166	161, 162, 165	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	112, 102	remulcld 9410	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
168	102	recnd 9408	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	109	recnd 9408	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
170	168, 169	mulcomd 9403	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
171	51, 62	abvge0 16890	. . . . . . . . . . . . . . . . . . 19 $/\$
172	84, 100, 171	syl2anc 656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173	101, 92, 172	expge0d 12022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
174	105	zred 10743	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175		elfzle1 11450	. . . . . . . . . . . . . . . . . . . . . 22
176	175	ad2antrl 722	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	93	nnred 10333	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178	93	nngt0d 10361	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179		divge0 10194	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
180	103, 176, 177, 178, 179	syl22anc 1214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181		flge0nn0 11662	. . . . . . . . . . . . . . . . . . . 20 $/\$
182	104, 180, 181	syl2anc 656	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
183	52, 51	qabvle 22833	. . . . . . . . . . . . . . . . . . 19 $/\$
184	84, 182, 183	syl2anc 656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185		simprl 750	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
186		0z 10653	. . . . . . . . . . . . . . . . . . . . . . . . 25
187	91, 119	nnexpcld 12025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
188	187	nnzd 10742	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189		elfzm11 11524	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
190	186, 188, 189	sylancr 658	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
191	185, 190	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	simp3d 997	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
193	91	nncnd 10334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
194	193, 92	expp1d 12005	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
195	192, 194	breqtrd 4313	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
196		ltdivmul 10200	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
197	103, 112, 177, 178, 196	syl112anc 1217	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
198	195, 197	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	91	nnzd 10742	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
200		fllt 11652	. . . . . . . . . . . . . . . . . . . . 21 $/\$
201	104, 199, 200	syl2anc 656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
202	198, 201	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
203	174, 112, 202	ltled 9518	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	109, 174, 112, 184, 203	letrd 9524	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
205	109, 112, 102, 173, 204	lemul1ad 10268	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
206	170, 205	eqbrtrd 4309	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
207	91	nnnn0d 10632	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
208	207	nn0ge0d 10635	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209		max1 11153	. . . . . . . . . . . . . . . . . . 19 $/\$
210	101, 59, 209	sylancl 657	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
211	210, 58	syl6breqr 4329	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
212		leexp1a 11918	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
213	101, 117, 92, 172, 211, 212	syl32anc 1221	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	102, 153, 112, 208, 213	lemul2ad 10269	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
215	110, 167, 159, 206, 214	letrd 9524	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
216	99, 110, 158, 159, 166, 215	le2addd 9953	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
217		nn0cn 10585	. . . . . . . . . . . . . . . . . 18
218	217	ad2antlr 721	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219		ax-1cn 9336	. . . . . . . . . . . . . . . . . 18
220	219	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	193, 218, 220	adddid 9406	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	193	mulid1d 9399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	222	oveq2d 6106	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
224	221, 223	eqtrd 2473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	224	oveq1d 6105	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
226	193, 218	mulcld 9402	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
227	153	recnd 9408	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
228	226, 193, 227	adddird 9407	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
229	225, 228	eqtrd 2473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
230	216, 229	breqtrrd 4315	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
231		max2 11155	. . . . . . . . . . . . . . . 16 $/\$
232	101, 59, 231	sylancl 657	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	232, 58	syl6breqr 4329	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
234		nn0z 10665	. . . . . . . . . . . . . . . . 17
235	234	ad2antlr 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
236		uzid 10871	. . . . . . . . . . . . . . . 16
237	235, 236	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
238		peano2uz 10904	. . . . . . . . . . . . . . 15
239	237, 238	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
240	117, 233, 239	leexp2ad 12036	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
241	91, 114	nnmulcld 10365	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
242	241	nngt0d 10361	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
243		lemul2 10178	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	153, 120, 116, 242, 243	syl112anc 1217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
245	240, 244	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
246	111, 154, 121, 230, 245	letrd 9524	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	90, 111, 121, 152, 246	letrd 9524	. . . . . . . . . 10 $/\$ $/\$ $/\$
248	247	expr 612	. . . . . . . . 9 $/\$ $/\$
249	248	ralrimdva 2804	. . . . . . . 8 $/\$
250	83, 249	syl5bi 217	. . . . . . 7 $/\$
251	250	expcom 435	. . . . . 6
252	251	a2d 26	. . . . 5
253	9, 18, 27, 36, 80, 252	nn0ind 10734	. . . 4
254	253	impcom 430	. . 3 $/\$
255		fveq2 5688	. . . . 5
256	255	breq1d 4299	. . . 4
257	256	rspccv 3067	. . 3
258	254, 257	syl 16	. 2 $/\$
259	258	3impia 1179	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

wral 2713

cvv 2970

cif 3788 class class class wbr 4289

cmpt 4347

cfv 5415 (class class class)co 6090

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cmin 9591

cneg 9592

cdiv 9989

cn 10318

c2 10367

cn0 10575

cz 10642

cuz 10857

cq 10949

crp 10987

cfz 11433

cfl 11636

cmo 11704

cexp 11861

cprime 13759

cpc 13899 ↾_s cress 14171

cplusg 14234

cmulr 14235 AbsValcabv 16881 ℂ_fldccnfld 17777

clog 21965

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357 ax-mulf 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-tpos 6744 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-map 7212 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-sup 7687 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-5 10379 df-6 10380 df-7 10381 df-8 10382 df-9 10383 df-10 10384 df-n0 10576 df-z 10643 df-dec 10752 df-uz 10858 df-q 10950 df-rp 10988 df-ico 11302 df-fz 11434 df-fl 11638 df-mod 11705 df-seq 11803 df-exp 11862 df-struct 14172 df-ndx 14173 df-slot 14174 df-base 14175 df-sets 14176 df-ress 14177 df-plusg 14247 df-mulr 14248 df-starv 14249 df-tset 14253 df-ple 14254 df-ds 14256 df-unif 14257 df-0g 14376 df-mnd 15411 df-grp 15538 df-minusg 15539 df-subg 15671 df-cmn 16272 df-mgp 16582 df-ur 16594 df-rng 16637 df-cring 16638 df-oppr 16705 df-dvdsr 16723 df-unit 16724 df-invr 16754 df-dvr 16765 df-drng 16814 df-subrg 16843 df-abv 16882 df-cnfld 17778

This theorem is referenced by: ostth2lem3 22843

W3C validator