ostth2lem2 - Metamath Proof Explorer

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

Theorem ostth2lem2 23563

Description: Lemma for ostth2 23566. (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 6291	. . . . . . . . 9
2	1	oveq1d 6298	. . . . . . . 8
3	2	oveq2d 6299	. . . . . . 7
4		oveq2 6291	. . . . . . . . 9
5		oveq2 6291	. . . . . . . . 9
6	4, 5	oveq12d 6301	. . . . . . . 8
7	6	breq2d 4459	. . . . . . 7
8	3, 7	raleqbidv 3072	. . . . . 6
9	8	imbi2d 316	. . . . 5
10		oveq2 6291	. . . . . . . . 9
11	10	oveq1d 6298	. . . . . . . 8
12	11	oveq2d 6299	. . . . . . 7
13		oveq2 6291	. . . . . . . . 9
14		oveq2 6291	. . . . . . . . 9
15	13, 14	oveq12d 6301	. . . . . . . 8
16	15	breq2d 4459	. . . . . . 7
17	12, 16	raleqbidv 3072	. . . . . 6
18	17	imbi2d 316	. . . . 5
19		oveq2 6291	. . . . . . . . 9
20	19	oveq1d 6298	. . . . . . . 8
21	20	oveq2d 6299	. . . . . . 7
22		oveq2 6291	. . . . . . . . 9
23		oveq2 6291	. . . . . . . . 9
24	22, 23	oveq12d 6301	. . . . . . . 8
25	24	breq2d 4459	. . . . . . 7
26	21, 25	raleqbidv 3072	. . . . . 6
27	26	imbi2d 316	. . . . 5
28		oveq2 6291	. . . . . . . . 9
29	28	oveq1d 6298	. . . . . . . 8
30	29	oveq2d 6299	. . . . . . 7
31		oveq2 6291	. . . . . . . . 9
32		oveq2 6291	. . . . . . . . 9
33	31, 32	oveq12d 6301	. . . . . . . 8
34	33	breq2d 4459	. . . . . . 7
35	30, 34	raleqbidv 3072	. . . . . 6
36	35	imbi2d 316	. . . . 5
37		ostth2.5	. . . . . . . . . . . . . 14
38		eluz2b2 11153	. . . . . . . . . . . . . . 15 $/\$
39	38	simplbi 460	. . . . . . . . . . . . . 14
40	37, 39	syl 16	. . . . . . . . . . . . 13
41	40	nncnd 10551	. . . . . . . . . . . 12
42	41	exp0d 12271	. . . . . . . . . . 11
43	42	oveq1d 6298	. . . . . . . . . 10
44		1m1e0 10603	. . . . . . . . . 10
45	43, 44	syl6eq 2524	. . . . . . . . 9
46	45	oveq2d 6299	. . . . . . . 8
47	46	eleq2d 2537	. . . . . . 7
48		0le0 10624	. . . . . . . . . 10
49	48	a1i 11	. . . . . . . . 9
50		ostth.1	. . . . . . . . . 10
51		qabsabv.a	. . . . . . . . . . 11 AbsVal
52		qrng.q	. . . . . . . . . . . 12 ℂ_fld ↾_s
53	52	qrng0 23550	. . . . . . . . . . 11
54	51, 53	abv0 17275	. . . . . . . . . 10
55	50, 54	syl 16	. . . . . . . . 9
56	41	mul01d 9777	. . . . . . . . . . 11
57	56	oveq1d 6298	. . . . . . . . . 10
58		ostth2.7	. . . . . . . . . . . . . 14
59		1re 9594	. . . . . . . . . . . . . . 15
60		nnq 11194	. . . . . . . . . . . . . . . . 17
61	40, 60	syl 16	. . . . . . . . . . . . . . . 16
62	52	qrngbas 23548	. . . . . . . . . . . . . . . . 17
63	51, 62	abvcl 17268	. . . . . . . . . . . . . . . 16 $/\$
64	50, 61, 63	syl2anc 661	. . . . . . . . . . . . . . 15
65		ifcl 3981	. . . . . . . . . . . . . . 15 $/\$
66	59, 64, 65	sylancr 663	. . . . . . . . . . . . . 14
67	58, 66	syl5eqel 2559	. . . . . . . . . . . . 13
68	67	recnd 9621	. . . . . . . . . . . 12
69		0nn0 10809	. . . . . . . . . . . 12
70		expcl 12151	. . . . . . . . . . . 12 $/\$
71	68, 69, 70	sylancl 662	. . . . . . . . . . 11
72	71	mul02d 9776	. . . . . . . . . 10
73	57, 72	eqtrd 2508	. . . . . . . . 9
74	49, 55, 73	3brtr4d 4477	. . . . . . . 8
75		elfz1eq 11696	. . . . . . . . . 10
76	75	fveq2d 5869	. . . . . . . . 9
77	76	breq1d 4457	. . . . . . . 8
78	74, 77	syl5ibrcom 222	. . . . . . 7
79	47, 78	sylbid 215	. . . . . 6
80	79	ralrimiv 2876	. . . . 5
81		fveq2 5865	. . . . . . . . . 10
82	81	breq1d 4457	. . . . . . . . 9
83	82	cbvralv 3088	. . . . . . . 8
84	50	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
85		elfzelz 11687	. . . . . . . . . . . . . 14
86	85	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
87		zq 11187	. . . . . . . . . . . . 13
88	86, 87	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
89	51, 62	abvcl 17268	. . . . . . . . . . . 12 $/\$
90	84, 88, 89	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
91	40	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		simplr 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
93	91, 92	nnexpcld 12298	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	86, 93	zmodcld 11983	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nn0zd 10963	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		zq 11187	. . . . . . . . . . . . . 14
97	95, 96	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
98	51, 62	abvcl 17268	. . . . . . . . . . . . 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 12294	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
103	86	zred 10965	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
104	103, 93	nndivred 10583	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
105	104	flcld 11902	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
106		zq 11187	. . . . . . . . . . . . . . 15
107	105, 106	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	51, 62	abvcl 17268	. . . . . . . . . . . . . 14 $/\$
109	84, 107, 108	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	102, 109	remulcld 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
111	99, 110	readdcld 9622	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	91	nnred 10550	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
113		nn0p1nn 10834	. . . . . . . . . . . . . . 15
114	113	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115	114	nnred 10550	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	112, 115	remulcld 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117	67	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		peano2nn0 10835	. . . . . . . . . . . . . 14
119	118	ad2antlr 726	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	117, 119	reexpcld 12294	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	116, 120	remulcld 9623	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122		nnq 11194	. . . . . . . . . . . . . . 15
123	93, 122	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		qmulcl 11199	. . . . . . . . . . . . . 14 $/\$
125	123, 107, 124	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126		qex 11193	. . . . . . . . . . . . . . 15
127		cnfldadd 18212	. . . . . . . . . . . . . . . 16 ℂ_fld
128	52, 127	ressplusg 14596	. . . . . . . . . . . . . . 15
129	126, 128	ax-mp 5	. . . . . . . . . . . . . 14
130	51, 62, 129	abvtri 17274	. . . . . . . . . . . . 13 $/\$ $/\$
131	84, 97, 125, 130	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
132	93	nnrpd 11254	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
133		modval 11965	. . . . . . . . . . . . . . . 16 $/\$
134	103, 132, 133	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
135	134	oveq1d 6298	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	103	recnd 9621	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137		qcn 11195	. . . . . . . . . . . . . . . 16
138	125, 137	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	136, 138	npcand 9933	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140	135, 139	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
141	140	fveq2d 5869	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
142		cnfldmul 18213	. . . . . . . . . . . . . . . . . 18 ℂ_fld
143	52, 142	ressmulr 14607	. . . . . . . . . . . . . . . . 17
144	126, 143	ax-mp 5	. . . . . . . . . . . . . . . 16
145	51, 62, 144	abvmul 17273	. . . . . . . . . . . . . . 15 $/\$ $/\$
146	84, 123, 107, 145	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147	52, 51	qabvexp 23555	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	84, 100, 92, 147	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	148	oveq1d 6298	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	146, 149	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	oveq2d 6299	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	131, 141, 151	3brtr3d 4476	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	117, 92	reexpcld 12294	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154	116, 153	remulcld 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
155		nn0re 10803	. . . . . . . . . . . . . . . . 17
156	155	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
157	112, 156	remulcld 9623	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	157, 153	remulcld 9623	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159	112, 153	remulcld 9623	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160		zmodfz 11984	. . . . . . . . . . . . . . . 16 $/\$
161	86, 93, 160	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162		simprr 756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163		fveq2 5865	. . . . . . . . . . . . . . . . 17
164	163	breq1d 4457	. . . . . . . . . . . . . . . 16
165	164	rspcv 3210	. . . . . . . . . . . . . . 15
166	161, 162, 165	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	112, 102	remulcld 9623	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
168	102	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
169	109	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
170	168, 169	mulcomd 9616	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
171	51, 62	abvge0 17269	. . . . . . . . . . . . . . . . . . 19 $/\$
172	84, 100, 171	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173	101, 92, 172	expge0d 12295	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
174	105	zred 10965	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175		elfzle1 11688	. . . . . . . . . . . . . . . . . . . . . 22
176	175	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
177	93	nnred 10550	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
178	93	nngt0d 10578	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
179		divge0 10410	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
180	103, 176, 177, 178, 179	syl22anc 1229	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181		flge0nn0 11921	. . . . . . . . . . . . . . . . . . . 20 $/\$
182	104, 180, 181	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
183	52, 51	qabvle 23554	. . . . . . . . . . . . . . . . . . 19 $/\$
184	84, 182, 183	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
186		0z 10874	. . . . . . . . . . . . . . . . . . . . . . . . 25
187	91, 119	nnexpcld 12298	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
188	187	nnzd 10964	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
189		elfzm11 11748	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
190	186, 188, 189	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
191	185, 190	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	simp3d 1010	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
193	91	nncnd 10551	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
194	193, 92	expp1d 12278	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
195	192, 194	breqtrd 4471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
196		ltdivmul 10416	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
197	103, 112, 177, 178, 196	syl112anc 1232	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
198	195, 197	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	91	nnzd 10964	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
200		fllt 11910	. . . . . . . . . . . . . . . . . . . . 21 $/\$
201	104, 199, 200	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
202	198, 201	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
203	174, 112, 202	ltled 9731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	109, 174, 112, 184, 203	letrd 9737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
205	109, 112, 102, 173, 204	lemul1ad 10484	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
206	170, 205	eqbrtrd 4467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
207	91	nnnn0d 10851	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
208	207	nn0ge0d 10854	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209		max1 11385	. . . . . . . . . . . . . . . . . . 19 $/\$
210	101, 59, 209	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
211	210, 58	syl6breqr 4487	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
212		leexp1a 12191	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
213	101, 117, 92, 172, 211, 212	syl32anc 1236	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	102, 153, 112, 208, 213	lemul2ad 10485	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
215	110, 167, 159, 206, 214	letrd 9737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
216	99, 110, 158, 159, 166, 215	le2addd 10169	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
217		nn0cn 10804	. . . . . . . . . . . . . . . . . 18
218	217	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
219		ax-1cn 9549	. . . . . . . . . . . . . . . . . 18
220	219	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
221	193, 218, 220	adddid 9619	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
222	193	mulid1d 9612	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	222	oveq2d 6299	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
224	221, 223	eqtrd 2508	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
225	224	oveq1d 6298	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
226	193, 218	mulcld 9615	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
227	153	recnd 9621	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
228	226, 193, 227	adddird 9620	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
229	225, 228	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
230	216, 229	breqtrrd 4473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
231		max2 11387	. . . . . . . . . . . . . . . 16 $/\$
232	101, 59, 231	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	232, 58	syl6breqr 4487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
234		nn0z 10886	. . . . . . . . . . . . . . . . 17
235	234	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
236		uzid 11095	. . . . . . . . . . . . . . . 16
237	235, 236	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
238		peano2uz 11133	. . . . . . . . . . . . . . 15
239	237, 238	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
240	117, 233, 239	leexp2ad 12309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
241	91, 114	nnmulcld 10582	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
242	241	nngt0d 10578	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
243		lemul2 10394	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	153, 120, 116, 242, 243	syl112anc 1232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
245	240, 244	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
246	111, 154, 121, 230, 245	letrd 9737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	90, 111, 121, 152, 246	letrd 9737	. . . . . . . . . 10 $/\$ $/\$ $/\$
248	247	expr 615	. . . . . . . . 9 $/\$ $/\$
249	248	ralrimdva 2882	. . . . . . . 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 10956	. . . 4
254	253	impcom 430	. . 3 $/\$
255		fveq2 5865	. . . . 5
256	255	breq1d 4457	. . . 4
257	256	rspccv 3211	. . 3
258	254, 257	syl 16	. 2 $/\$
259	258	3impia 1193	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2814

cvv 3113

cif 3939 class class class wbr 4447

cmpt 4505

cfv 5587 (class class class)co 6283

cc 9489

cr 9490

cc0 9491

c1 9492

caddc 9494

cmul 9496

clt 9627

cle 9628

cmin 9804

cneg 9805

cdiv 10205

cn 10535

c2 10584

cn0 10794

cz 10863

cuz 11081

cq 11181

crp 11219

cfz 11671

cfl 11894

cmo 11963

cexp 12133

cprime 14075

cpc 14218 ↾_s cress 14490

cplusg 14554

cmulr 14555 AbsValcabv 17260 ℂ_fldccnfld 18207

clog 22686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6575 ax-cnex 9547 ax-resscn 9548 ax-1cn 9549 ax-icn 9550 ax-addcl 9551 ax-addrcl 9552 ax-mulcl 9553 ax-mulrcl 9554 ax-mulcom 9555 ax-addass 9556 ax-mulass 9557 ax-distr 9558 ax-i2m1 9559 ax-1ne0 9560 ax-1rid 9561 ax-rnegex 9562 ax-rrecex 9563 ax-cnre 9564 ax-pre-lttri 9565 ax-pre-lttrn 9566 ax-pre-ltadd 9567 ax-pre-mulgt0 9568 ax-pre-sup 9569 ax-addf 9570 ax-mulf 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288 df-om 6680 df-1st 6784 df-2nd 6785 df-tpos 6955 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7900 df-pnf 9629 df-mnf 9630 df-xr 9631 df-ltxr 9632 df-le 9633 df-sub 9806 df-neg 9807 df-div 10206 df-nn 10536 df-2 10593 df-3 10594 df-4 10595 df-5 10596 df-6 10597 df-7 10598 df-8 10599 df-9 10600 df-10 10601 df-n0 10795 df-z 10864 df-dec 10976 df-uz 11082 df-q 11182 df-rp 11220 df-ico 11534 df-fz 11672 df-fl 11896 df-mod 11964 df-seq 12075 df-exp 12134 df-struct 14491 df-ndx 14492 df-slot 14493 df-base 14494 df-sets 14495 df-ress 14496 df-plusg 14567 df-mulr 14568 df-starv 14569 df-tset 14573 df-ple 14574 df-ds 14576 df-unif 14577 df-0g 14696 df-mnd 15731 df-grp 15864 df-minusg 15865 df-subg 16000 df-cmn 16603 df-mgp 16941 df-ur 16953 df-rng 16997 df-cring 16998 df-oppr 17068 df-dvdsr 17086 df-unit 17087 df-invr 17117 df-dvr 17128 df-drng 17193 df-subrg 17222 df-abv 17261 df-cnfld 18208

This theorem is referenced by: ostth2lem3 23564

W3C validator