ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 22895

Description: Lemma for ostth2 22898. (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 6111	. . . . . . . . 9
2	1	oveq1d 6118	. . . . . . . 8
3	2	oveq2d 6119	. . . . . . 7
4		oveq2 6111	. . . . . . . . 9
5		oveq2 6111	. . . . . . . . 9
6	4, 5	oveq12d 6121	. . . . . . . 8
7	6	breq2d 4316	. . . . . . 7
8	3, 7	raleqbidv 2943	. . . . . 6
9	8	imbi2d 316	. . . . 5
10		oveq2 6111	. . . . . . . . 9
11	10	oveq1d 6118	. . . . . . . 8
12	11	oveq2d 6119	. . . . . . 7
13		oveq2 6111	. . . . . . . . 9
14		oveq2 6111	. . . . . . . . 9
15	13, 14	oveq12d 6121	. . . . . . . 8
16	15	breq2d 4316	. . . . . . 7
17	12, 16	raleqbidv 2943	. . . . . 6
18	17	imbi2d 316	. . . . 5
19		oveq2 6111	. . . . . . . . 9
20	19	oveq1d 6118	. . . . . . . 8
21	20	oveq2d 6119	. . . . . . 7
22		oveq2 6111	. . . . . . . . 9
23		oveq2 6111	. . . . . . . . 9
24	22, 23	oveq12d 6121	. . . . . . . 8
25	24	breq2d 4316	. . . . . . 7
26	21, 25	raleqbidv 2943	. . . . . 6
27	26	imbi2d 316	. . . . 5
28		oveq2 6111	. . . . . . . . 9
29	28	oveq1d 6118	. . . . . . . 8
30	29	oveq2d 6119	. . . . . . 7
31		oveq2 6111	. . . . . . . . 9
32		oveq2 6111	. . . . . . . . 9
33	31, 32	oveq12d 6121	. . . . . . . 8
34	33	breq2d 4316	. . . . . . 7
35	30, 34	raleqbidv 2943	. . . . . 6
36	35	imbi2d 316	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2b2 10939	. . . . . . . . . . . . . . 15 $/\$
39	38	simplbi 460	. . . . . . . . . . . . . 14
40	37, 39	syl 16	. . . . . . . . . . . . 13
41	40	nncnd 10350	. . . . . . . . . . . 12
42	41	exp0d 12014	. . . . . . . . . . 11
43	42	oveq1d 6118	. . . . . . . . . 10
44		1m1e0 10402	. . . . . . . . . 10
45	43, 44	syl6eq 2491	. . . . . . . . 9
46	45	oveq2d 6119	. . . . . . . 8
47	46	eleq2d 2510	. . . . . . 7
48		0le0 10423	. . . . . . . . . 10
49	48	a1i 11	. . . . . . . . 9
50		ostth.1	. . . . . . . . . 10
51		qabsabv.a	. . . . . . . . . . 11 AbsVal
52		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
53	52	qrng0 22882	. . . . . . . . . . 11
54	51, 53	abv0 16928	. . . . . . . . . 10
55	50, 54	syl 16	. . . . . . . . 9
56	41	mul01d 9580	. . . . . . . . . . 11
57	56	oveq1d 6118	. . . . . . . . . 10
58		ostth2.7	. . . . . . . . . . . . . 14
59		1re 9397	. . . . . . . . . . . . . . 15
60		nnq 10978	. . . . . . . . . . . . . . . . 17
61	40, 60	syl 16	. . . . . . . . . . . . . . . 16
62	52	qrngbas 22880	. . . . . . . . . . . . . . . . 17
63	51, 62	abvcl 16921	. . . . . . . . . . . . . . . 16 $/\$
64	50, 61, 63	syl2anc 661	. . . . . . . . . . . . . . 15
65		ifcl 3843	. . . . . . . . . . . . . . 15 $/\$
66	59, 64, 65	sylancr 663	. . . . . . . . . . . . . 14
67	58, 66	syl5eqel 2527	. . . . . . . . . . . . 13
68	67	recnd 9424	. . . . . . . . . . . 12
69		0nn0 10606	. . . . . . . . . . . 12
70		expcl 11895	. . . . . . . . . . . 12 $/\$
71	68, 69, 70	sylancl 662	. . . . . . . . . . 11
72	71	mul02d 9579	. . . . . . . . . 10
73	57, 72	eqtrd 2475	. . . . . . . . 9
74	49, 55, 73	3brtr4d 4334	. . . . . . . 8
75		elfz1eq 11474	. . . . . . . . . 10
76	75	fveq2d 5707	. . . . . . . . 9
77	76	breq1d 4314	. . . . . . . 8
78	74, 77	syl5ibrcom 222	. . . . . . 7
79	47, 78	sylbid 215	. . . . . 6
80	79	ralrimiv 2810	. . . . 5
81		fveq2 5703	. . . . . . . . . 10
82	81	breq1d 4314	. . . . . . . . 9
83	82	cbvralv 2959	. . . . . . . 8
84	50	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
85		elfzelz 11465	. . . . . . . . . . . . . 14
86	85	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
87		zq 10971	. . . . . . . . . . . . 13
88	86, 87	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
89	51, 62	abvcl 16921	. . . . . . . . . . . 12 $/\$
90	84, 88, 89	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
91	40	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		simplr 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
93	91, 92	nnexpcld 12041	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	86, 93	zmodcld 11740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nn0zd 10757	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		zq 10971	. . . . . . . . . . . . . 14
97	95, 96	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
98	51, 62	abvcl 16921	. . . . . . . . . . . . 13 $/\$
99	84, 97, 98	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	91, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
101	84, 100, 63	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101, 92	reexpcld 12037	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
103	86	zred 10759	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
104	103, 93	nndivred 10382	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
105	104	flcld 11660	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
106		zq 10971	. . . . . . . . . . . . . . 15
107	105, 106	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	51, 62	abvcl 16921	. . . . . . . . . . . . . 14 $/\$
109	84, 107, 108	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	102, 109	remulcld 9426	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
111	99, 110	readdcld 9425	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	91	nnred 10349	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
113		nn0p1nn 10631	. . . . . . . . . . . . . . 15
114	113	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115	114	nnred 10349	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	112, 115	remulcld 9426	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117	67	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		peano2nn0 10632	. . . . . . . . . . . . . 14
119	118	ad2antlr 726	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	117, 119	reexpcld 12037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	116, 120	remulcld 9426	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122		nnq 10978	. . . . . . . . . . . . . . 15
123	93, 122	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		qmulcl 10983	. . . . . . . . . . . . . 14 $/\$
125	123, 107, 124	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126		qex 10977	. . . . . . . . . . . . . . 15
127		cnfldadd 17835	. . . . . . . . . . . . . . . 16 ℂ_fld
128	52, 127	ressplusg 14292	. . . . . . . . . . . . . . 15
129	126, 128	ax-mp 5	. . . . . . . . . . . . . 14
130	51, 62, 129	abvtri 16927	. . . . . . . . . . . . 13 $/\$ $/\$
131	84, 97, 125, 130	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
132	93	nnrpd 11038	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
133		modval 11722	. . . . . . . . . . . . . . . 16 $/\$
134	103, 132, 133	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
135	134	oveq1d 6118	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	103	recnd 9424	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137		qcn 10979	. . . . . . . . . . . . . . . 16
138	125, 137	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	136, 138	npcand 9735	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140	135, 139	eqtrd 2475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
141	140	fveq2d 5707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
142		cnfldmul 17836	. . . . . . . . . . . . . . . . . 18 ℂ_fld
143	52, 142	ressmulr 14303	. . . . . . . . . . . . . . . . 17
144	126, 143	ax-mp 5	. . . . . . . . . . . . . . . 16
145	51, 62, 144	abvmul 16926	. . . . . . . . . . . . . . 15 $/\$ $/\$
146	84, 123, 107, 145	syl3anc 1218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147	52, 51	qabvexp 22887	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	84, 100, 92, 147	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	148	oveq1d 6118	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	146, 149	eqtrd 2475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	oveq2d 6119	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	131, 141, 151	3brtr3d 4333	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	117, 92	reexpcld 12037	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154	116, 153	remulcld 9426	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
155		nn0re 10600	. . . . . . . . . . . . . . . . 17
156	155	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
157	112, 156	remulcld 9426	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	157, 153	remulcld 9426	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159	112, 153	remulcld 9426	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160		zmodfz 11741	. . . . . . . . . . . . . . . 16 $/\$
161	86, 93, 160	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		simprr 756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163		fveq2 5703	. . . . . . . . . . . . . . . . 17
164	163	breq1d 4314	. . . . . . . . . . . . . . . 16
165	164	rspcv 3081	. . . . . . . . . . . . . . 15
166	161, 162, 165	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	112, 102	remulcld 9426	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
168	102	recnd 9424	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	109	recnd 9424	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
170	168, 169	mulcomd 9419	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
171	51, 62	abvge0 16922	. . . . . . . . . . . . . . . . . . 19 $/\$
172	84, 100, 171	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173	101, 92, 172	expge0d 12038	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
174	105	zred 10759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175		elfzle1 11466	. . . . . . . . . . . . . . . . . . . . . 22
176	175	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	93	nnred 10349	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178	93	nngt0d 10377	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179		divge0 10210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
180	103, 176, 177, 178, 179	syl22anc 1219	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181		flge0nn0 11678	. . . . . . . . . . . . . . . . . . . 20 $/\$
182	104, 180, 181	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
183	52, 51	qabvle 22886	. . . . . . . . . . . . . . . . . . 19 $/\$
184	84, 182, 183	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
186		0z 10669	. . . . . . . . . . . . . . . . . . . . . . . . 25
187	91, 119	nnexpcld 12041	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
188	187	nnzd 10758	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189		elfzm11 11540	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
190	186, 188, 189	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
191	185, 190	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	simp3d 1002	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
193	91	nncnd 10350	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
194	193, 92	expp1d 12021	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
195	192, 194	breqtrd 4328	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
196		ltdivmul 10216	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
197	103, 112, 177, 178, 196	syl112anc 1222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
198	195, 197	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	91	nnzd 10758	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
200		fllt 11668	. . . . . . . . . . . . . . . . . . . . 21 $/\$
201	104, 199, 200	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
202	198, 201	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
203	174, 112, 202	ltled 9534	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	109, 174, 112, 184, 203	letrd 9540	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
205	109, 112, 102, 173, 204	lemul1ad 10284	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
206	170, 205	eqbrtrd 4324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
207	91	nnnn0d 10648	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
208	207	nn0ge0d 10651	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209		max1 11169	. . . . . . . . . . . . . . . . . . 19 $/\$
210	101, 59, 209	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
211	210, 58	syl6breqr 4344	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
212		leexp1a 11934	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
213	101, 117, 92, 172, 211, 212	syl32anc 1226	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	102, 153, 112, 208, 213	lemul2ad 10285	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
215	110, 167, 159, 206, 214	letrd 9540	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
216	99, 110, 158, 159, 166, 215	le2addd 9969	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
217		nn0cn 10601	. . . . . . . . . . . . . . . . . 18
218	217	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219		ax-1cn 9352	. . . . . . . . . . . . . . . . . 18
220	219	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	193, 218, 220	adddid 9422	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	193	mulid1d 9415	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	222	oveq2d 6119	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
224	221, 223	eqtrd 2475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	224	oveq1d 6118	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
226	193, 218	mulcld 9418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
227	153	recnd 9424	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
228	226, 193, 227	adddird 9423	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
229	225, 228	eqtrd 2475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
230	216, 229	breqtrrd 4330	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
231		max2 11171	. . . . . . . . . . . . . . . 16 $/\$
232	101, 59, 231	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	232, 58	syl6breqr 4344	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
234		nn0z 10681	. . . . . . . . . . . . . . . . 17
235	234	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
236		uzid 10887	. . . . . . . . . . . . . . . 16
237	235, 236	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
238		peano2uz 10920	. . . . . . . . . . . . . . 15
239	237, 238	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
240	117, 233, 239	leexp2ad 12052	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
241	91, 114	nnmulcld 10381	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
242	241	nngt0d 10377	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
243		lemul2 10194	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	153, 120, 116, 242, 243	syl112anc 1222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
245	240, 244	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
246	111, 154, 121, 230, 245	letrd 9540	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	90, 111, 121, 152, 246	letrd 9540	. . . . . . . . . 10 $/\$ $/\$ $/\$
248	247	expr 615	. . . . . . . . 9 $/\$ $/\$
249	248	ralrimdva 2818	. . . . . . . 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 10750	. . . 4
254	253	impcom 430	. . 3 $/\$
255		fveq2 5703	. . . . 5
256	255	breq1d 4314	. . . 4
257	256	rspccv 3082	. . 3
258	254, 257	syl 16	. 2 $/\$
259	258	3impia 1184	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2727

cvv 2984

cif 3803 class class class wbr 4304

cmpt 4362

cfv 5430 (class class class)co 6103

cc 9292

cr 9293

cc0 9294

c1 9295

caddc 9297

cmul 9299

clt 9430

cle 9431

cmin 9607

cneg 9608

cdiv 10005

cn 10334

c2 10383

cn0 10591

cz 10658

cuz 10873

cq 10965

crp 11003

cfz 11449

cfl 11652

cmo 11720

cexp 11877

cprime 13775

cpc 13915 ↾_s cress 14187

cplusg 14250

cmulr 14251 AbsValcabv 16913 ℂ_fldccnfld 17830

clog 22018

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4415 ax-sep 4425 ax-nul 4433 ax-pow 4482 ax-pr 4543 ax-un 6384 ax-cnex 9350 ax-resscn 9351 ax-1cn 9352 ax-icn 9353 ax-addcl 9354 ax-addrcl 9355 ax-mulcl 9356 ax-mulrcl 9357 ax-mulcom 9358 ax-addass 9359 ax-mulass 9360 ax-distr 9361 ax-i2m1 9362 ax-1ne0 9363 ax-1rid 9364 ax-rnegex 9365 ax-rrecex 9366 ax-cnre 9367 ax-pre-lttri 9368 ax-pre-lttrn 9369 ax-pre-ltadd 9370 ax-pre-mulgt0 9371 ax-pre-sup 9372 ax-addf 9373 ax-mulf 9374

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2620 df-nel 2621 df-ral 2732 df-rex 2733 df-reu 2734 df-rmo 2735 df-rab 2736 df-v 2986 df-sbc 3199 df-csb 3301 df-dif 3343 df-un 3345 df-in 3347 df-ss 3354 df-pss 3356 df-nul 3650 df-if 3804 df-pw 3874 df-sn 3890 df-pr 3892 df-tp 3894 df-op 3896 df-uni 4104 df-int 4141 df-iun 4185 df-br 4305 df-opab 4363 df-mpt 4364 df-tr 4398 df-eprel 4644 df-id 4648 df-po 4653 df-so 4654 df-fr 4691 df-we 4693 df-ord 4734 df-on 4735 df-lim 4736 df-suc 4737 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5393 df-fun 5432 df-fn 5433 df-f 5434 df-f1 5435 df-fo 5436 df-f1o 5437 df-fv 5438 df-riota 6064 df-ov 6106 df-oprab 6107 df-mpt2 6108 df-om 6489 df-1st 6589 df-2nd 6590 df-tpos 6757 df-recs 6844 df-rdg 6878 df-1o 6932 df-oadd 6936 df-er 7113 df-map 7228 df-en 7323 df-dom 7324 df-sdom 7325 df-fin 7326 df-sup 7703 df-pnf 9432 df-mnf 9433 df-xr 9434 df-ltxr 9435 df-le 9436 df-sub 9609 df-neg 9610 df-div 10006 df-nn 10335 df-2 10392 df-3 10393 df-4 10394 df-5 10395 df-6 10396 df-7 10397 df-8 10398 df-9 10399 df-10 10400 df-n0 10592 df-z 10659 df-dec 10768 df-uz 10874 df-q 10966 df-rp 11004 df-ico 11318 df-fz 11450 df-fl 11654 df-mod 11721 df-seq 11819 df-exp 11878 df-struct 14188 df-ndx 14189 df-slot 14190 df-base 14191 df-sets 14192 df-ress 14193 df-plusg 14263 df-mulr 14264 df-starv 14265 df-tset 14269 df-ple 14270 df-ds 14272 df-unif 14273 df-0g 14392 df-mnd 15427 df-grp 15557 df-minusg 15558 df-subg 15690 df-cmn 16291 df-mgp 16604 df-ur 16616 df-rng 16659 df-cring 16660 df-oppr 16727 df-dvdsr 16745 df-unit 16746 df-invr 16776 df-dvr 16787 df-drng 16846 df-subrg 16875 df-abv 16914 df-cnfld 17831

This theorem is referenced by: ostth2lem3 22896

W3C validator