Theorem ostth2 24486

Description: - Lemma for ostth 24488: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.)

Hypotheses

Ref	Expression
qrng.q	|- Q = (ℂfld ↾s QQ )
qabsabv.a	|- A = (AbsVal ` Q )
padic.j	|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
ostth.k	|- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
ostth.1	|- ( ph -> F e. A )
ostth2.2	|- ( ph -> N e. ( ZZ>= ` 2 ) )
ostth2.3	|- ( ph -> 1 < ( F ` N ) )
ostth2.4	|- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )

Assertion

Ref	Expression
ostth2	|- ( ph -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )

Distinct variable groups:   q, a, x, y, ph   J, a, y   A, a, q, x, y   x, N, y   x, Q, y   F, a, q, y   R, a, q, y   x, F

Allowed substitution hints:   Q( q, a)   R( x)   J( x, q)   K( x, y, q, a)   N( q, a)

Proof of Theorem ostth2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ostth2.4	. . . . 5 |- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )
2		ostth.1	. . . . . . . 8 |- ( ph -> F e. A )
3		ostth2.2	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` 2 ) )
4		eluz2b2 11220	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
5	3, 4	sylib 201	. . . . . . . . . 10 |- ( ph -> ( N e. NN /\ 1 < N ) )
6	5	simpld 465	. . . . . . . . 9 |- ( ph -> N e. NN )
7		nnq 11266	. . . . . . . . 9 |- ( N e. NN -> N e. QQ )
8	6, 7	syl 17	. . . . . . . 8 |- ( ph -> N e. QQ )
9		qabsabv.a	. . . . . . . . 9 |- A = (AbsVal ` Q )
10		qrng.q	. . . . . . . . . 10 |- Q = (ℂfld ↾s QQ )
11	10	qrngbas 24468	. . . . . . . . 9 |- QQ = ( Base ` Q )
12	9, 11	abvcl 18062	. . . . . . . 8 |- ( ( F e. A /\ N e. QQ ) -> ( F ` N ) e. RR )
13	2, 8, 12	syl2anc 671	. . . . . . 7 |- ( ph -> ( F ` N ) e. RR )
14		ostth2.3	. . . . . . 7 |- ( ph -> 1 < ( F ` N ) )
15	13, 14	rplogcld 23589	. . . . . 6 |- ( ph -> ( log ` ( F ` N ) ) e. RR+ )
16	6	nnred 10612	. . . . . . 7 |- ( ph -> N e. RR )
17	5	simprd 469	. . . . . . 7 |- ( ph -> 1 < N )
18	16, 17	rplogcld 23589	. . . . . 6 |- ( ph -> ( log ` N ) e. RR+ )
19	15, 18	rpdivcld 11347	. . . . 5 |- ( ph -> ( ( log ` ( F ` N ) ) / ( log ` N ) ) e. RR+ )
20	1, 19	syl5eqel 2533	. . . 4 |- ( ph -> R e. RR+ )
21	20	rpred 11330	. . 3 |- ( ph -> R e. RR )
22	20	rpgt0d 11333	. . 3 |- ( ph -> 0 < R )
23	6	nnnn0d 10914	. . . . . . . . 9 |- ( ph -> N e. NN0 )
24	10, 9	qabvle 24474	. . . . . . . . 9 |- ( ( F e. A /\ N e. NN0 ) -> ( F ` N ) <_ N )
25	2, 23, 24	syl2anc 671	. . . . . . . 8 |- ( ph -> ( F ` N ) <_ N )
26	6	nnne0d 10642	. . . . . . . . . . 11 |- ( ph -> N =/= 0 )
27	10	qrng0 24470	. . . . . . . . . . . 12 |- 0 = ( 0g ` Q )
28	9, 11, 27	abvgt0 18066	. . . . . . . . . . 11 |- ( ( F e. A /\ N e. QQ /\ N =/= 0 ) -> 0 < ( F ` N ) )
29	2, 8, 26, 28	syl3anc 1271	. . . . . . . . . 10 |- ( ph -> 0 < ( F ` N ) )
30	13, 29	elrpd 11327	. . . . . . . . 9 |- ( ph -> ( F ` N ) e. RR+ )
31	30	reeflogd 23584	. . . . . . . 8 |- ( ph -> ( exp ` ( log ` ( F ` N ) ) ) = ( F ` N ) )
32	6	nnrpd 11328	. . . . . . . . 9 |- ( ph -> N e. RR+ )
33	32	reeflogd 23584	. . . . . . . 8 |- ( ph -> ( exp ` ( log ` N ) ) = N )
34	25, 31, 33	3brtr4d 4404	. . . . . . 7 |- ( ph -> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) )
35	15	rpred 11330	. . . . . . . 8 |- ( ph -> ( log ` ( F ` N ) ) e. RR )
36	32	relogcld 23583	. . . . . . . 8 |- ( ph -> ( log ` N ) e. RR )
37		efle 14182	. . . . . . . 8 |- ( ( ( log ` ( F ` N ) ) e. RR /\ ( log ` N ) e. RR ) -> ( ( log ` ( F ` N ) ) <_ ( log ` N ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) ) )
38	35, 36, 37	syl2anc 671	. . . . . . 7 |- ( ph -> ( ( log ` ( F ` N ) ) <_ ( log ` N ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) ) )
39	34, 38	mpbird 240	. . . . . 6 |- ( ph -> ( log ` ( F ` N ) ) <_ ( log ` N ) )
40	18	rpcnd 11332	. . . . . . 7 |- ( ph -> ( log ` N ) e. CC )
41	40	mulid1d 9646	. . . . . 6 |- ( ph -> ( ( log ` N ) x. 1 ) = ( log ` N ) )
42	39, 41	breqtrrd 4400	. . . . 5 |- ( ph -> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. 1 ) )
43		1red 9644	. . . . . 6 |- ( ph -> 1 e. RR )
44	35, 43, 18	ledivmuld 11380	. . . . 5 |- ( ph -> ( ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ 1 <-> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. 1 ) ) )
45	42, 44	mpbird 240	. . . 4 |- ( ph -> ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ 1 )
46	1, 45	syl5eqbr 4407	. . 3 |- ( ph -> R <_ 1 )
47		0xr 9673	. . . 4 |- 0 e. RR*
48		1re 9628	. . . 4 |- 1 e. RR
49		elioc2 11686	. . . 4 |- ( ( 0 e. RR* /\ 1 e. RR ) -> ( R e. ( 0 (,] 1 ) <-> ( R e. RR /\ 0 < R /\ R <_ 1 ) ) )
50	47, 48, 49	mp2an 683	. . 3 |- ( R e. ( 0 (,] 1 ) <-> ( R e. RR /\ 0 < R /\ R <_ 1 ) )
51	21, 22, 46, 50	syl3anbrc 1193	. 2 |- ( ph -> R e. ( 0 (,] 1 ) )
52	10, 9	qabsabv 24478	. . . 4 |- ( abs |` QQ ) e. A
53		fvres 5861	. . . . . . . 8 |- ( y e. QQ -> ( ( abs |` QQ ) ` y ) = ( abs ` y ) )
54	53	oveq1d 6290	. . . . . . 7 |- ( y e. QQ -> ( ( ( abs |` QQ ) ` y ) ^c R ) = ( ( abs ` y ) ^c R ) )
55	54	mpteq2ia 4456	. . . . . 6 |- ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c R ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) )
56	55	eqcomi 2460	. . . . 5 |- ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) = ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c R ) )
57	9, 11, 56	abvcxp 24464	. . . 4 |- ( ( ( abs |` QQ ) e. A /\ R e. ( 0 (,] 1 ) ) -> ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) e. A )
58	52, 51, 57	sylancr 674	. . 3 |- ( ph -> ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) e. A )
59		eluzelz 11157	. . . . . 6 |- ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
60		zq 11259	. . . . . 6 |- ( z e. ZZ -> z e. QQ )
61		fveq2 5847	. . . . . . . 8 |- ( y = z -> ( abs ` y ) = ( abs ` z ) )
62	61	oveq1d 6290	. . . . . . 7 |- ( y = z -> ( ( abs ` y ) ^c R ) = ( ( abs ` z ) ^c R ) )
63		eqid 2451	. . . . . . 7 |- ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) )
64		ovex 6303	. . . . . . 7 |- ( ( abs ` z ) ^c R ) e. _V
65	62, 63, 64	fvmpt 5931	. . . . . 6 |- ( z e. QQ -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
66	59, 60, 65	3syl 18	. . . . 5 |- ( z e. ( ZZ>= ` 2 ) -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
67	66	adantl 472	. . . 4 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
68		simpr 467	. . . . . . . . 9 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. ( ZZ>= ` 2 ) )
69		eluz2b2 11220	. . . . . . . . 9 |- ( z e. ( ZZ>= ` 2 ) <-> ( z e. NN /\ 1 < z ) )
70	68, 69	sylib 201	. . . . . . . 8 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z e. NN /\ 1 < z ) )
71	70	simpld 465	. . . . . . 7 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. NN )
72	71	nnred 10612	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. RR )
73	71	nnnn0d 10914	. . . . . . 7 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. NN0 )
74	73	nn0ge0d 10917	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 <_ z )
75	72, 74	absidd 13494	. . . . 5 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( abs ` z ) = z )
76	75	oveq1d 6290	. . . 4 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( abs ` z ) ^c R ) = ( z ^c R ) )
77	72	recnd 9655	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. CC )
78	71	nnne0d 10642	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z =/= 0 )
79	20	rpcnd 11332	. . . . . . 7 |- ( ph -> R e. CC )
80	79	adantr 471	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R e. CC )
81	77, 78, 80	cxpefd 23668	. . . . 5 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z ^c R ) = ( exp ` ( R x. ( log ` z ) ) ) )
82		padic.j	. . . . . . . . . . 11 |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
83		ostth.k	. . . . . . . . . . 11 |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
84	2	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> F e. A )
85	3	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> N e. ( ZZ>= ` 2 ) )
86	14	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( F ` N ) )
87		eqid 2451	. . . . . . . . . . 11 |- ( ( log ` ( F ` z ) ) / ( log ` z ) ) = ( ( log ` ( F ` z ) ) / ( log ` z ) )
88		eqid 2451	. . . . . . . . . . 11 |- if ( ( F ` z ) <_ 1 , 1 , ( F ` z ) ) = if ( ( F ` z ) <_ 1 , 1 , ( F ` z ) )
89		eqid 2451	. . . . . . . . . . 11 |- ( ( log ` N ) / ( log ` z ) ) = ( ( log ` N ) / ( log ` z ) )
90	10, 9, 82, 83, 84, 85, 86, 1, 68, 87, 88, 89	ostth2lem4 24485	. . . . . . . . . 10 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 1 < ( F ` z ) /\ R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) ) )
91	90	simprd 469	. . . . . . . . 9 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) )
92	90	simpld 465	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( F ` z ) )
93		eqid 2451	. . . . . . . . . . 11 |- if ( ( F ` N ) <_ 1 , 1 , ( F ` N ) ) = if ( ( F ` N ) <_ 1 , 1 , ( F ` N ) )
94		eqid 2451	. . . . . . . . . . 11 |- ( ( log ` z ) / ( log ` N ) ) = ( ( log ` z ) / ( log ` N ) )
95	10, 9, 82, 83, 84, 68, 92, 87, 85, 1, 93, 94	ostth2lem4 24485	. . . . . . . . . 10 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 1 < ( F ` N ) /\ ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R ) )
96	95	simprd 469	. . . . . . . . 9 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R )
97	21	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R e. RR )
98	59	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. ZZ )
99	98, 60	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. QQ )
100	9, 11	abvcl 18062	. . . . . . . . . . . . . 14 |- ( ( F e. A /\ z e. QQ ) -> ( F ` z ) e. RR )
101	84, 99, 100	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) e. RR )
102	9, 11, 27	abvgt0 18066	. . . . . . . . . . . . . 14 |- ( ( F e. A /\ z e. QQ /\ z =/= 0 ) -> 0 < ( F ` z ) )
103	84, 99, 78, 102	syl3anc 1271	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 < ( F ` z ) )
104	101, 103	elrpd 11327	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) e. RR+ )
105	104	relogcld 23583	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` ( F ` z ) ) e. RR )
106	71	nnrpd 11328	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. RR+ )
107	106	relogcld 23583	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) e. RR )
108		ef0 14155	. . . . . . . . . . . . . 14 |- ( exp ` 0 ) = 1
109	70	simprd 469	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < z )
110	106	reeflogd 23584	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( log ` z ) ) = z )
111	109, 110	breqtrrd 4400	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( exp ` ( log ` z ) ) )
112	108, 111	syl5eqbr 4407	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` 0 ) < ( exp ` ( log ` z ) ) )
113		0re 9629	. . . . . . . . . . . . . 14 |- 0 e. RR
114		eflt 14181	. . . . . . . . . . . . . 14 |- ( ( 0 e. RR /\ ( log ` z ) e. RR ) -> ( 0 < ( log ` z ) <-> ( exp ` 0 ) < ( exp ` ( log ` z ) ) ) )
115	113, 107, 114	sylancr 674	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 0 < ( log ` z ) <-> ( exp ` 0 ) < ( exp ` ( log ` z ) ) ) )
116	112, 115	mpbird 240	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 < ( log ` z ) )
117	116	gt0ne0d 10166	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) =/= 0 )
118	105, 107, 117	redivcld 10423	. . . . . . . . . 10 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( log ` ( F ` z ) ) / ( log ` z ) ) e. RR )
119	97, 118	letri3d 9763	. . . . . . . . 9 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R = ( ( log ` ( F ` z ) ) / ( log ` z ) ) <-> ( R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) /\ ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R ) ) )
120	91, 96, 119	mpbir2and 933	. . . . . . . 8 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R = ( ( log ` ( F ` z ) ) / ( log ` z ) ) )
121	120	oveq1d 6290	. . . . . . 7 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R x. ( log ` z ) ) = ( ( ( log ` ( F ` z ) ) / ( log ` z ) ) x. ( log ` z ) ) )
122	105	recnd 9655	. . . . . . . 8 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` ( F ` z ) ) e. CC )
123	107	recnd 9655	. . . . . . . 8 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) e. CC )
124	122, 123, 117	divcan1d 10372	. . . . . . 7 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( log ` ( F ` z ) ) / ( log ` z ) ) x. ( log ` z ) ) = ( log ` ( F ` z ) ) )
125	121, 124	eqtrd 2485	. . . . . 6 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R x. ( log ` z ) ) = ( log ` ( F ` z ) ) )
126	125	fveq2d 5851	. . . . 5 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( R x. ( log ` z ) ) ) = ( exp ` ( log ` ( F ` z ) ) ) )
127	104	reeflogd 23584	. . . . 5 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( log ` ( F ` z ) ) ) = ( F ` z ) )
128	81, 126, 127	3eqtrd 2489	. . . 4 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z ^c R ) = ( F ` z ) )
129	67, 76, 128	3eqtrrd 2490	. . 3 |- ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) = ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) )
130	10, 9, 2, 58, 129	ostthlem1 24476	. 2 |- ( ph -> F = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) )
131		oveq2 6283	. . . . 5 |- ( a = R -> ( ( abs ` y ) ^c a ) = ( ( abs ` y ) ^c R ) )
132	131	mpteq2dv 4461	. . . 4 |- ( a = R -> ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) )
133	132	eqeq2d 2461	. . 3 |- ( a = R -> ( F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) <-> F = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ) )
134	133	rspcev 3117	. 2 |- ( ( R e. ( 0 (,] 1 ) /\ F = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ) -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )
135	51, 130, 134	syl2anc 671	1 |- ( ph -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 986   = wceq 1447   e. wcel 1890   =/= wne 2621   E.wrex 2737   ifcif 3848   class class class wbr 4373   |-> cmpt 4432   |` cres 4813   ` cfv 5560  (class class class)co 6275   CCcc 9523   RRcr 9524   0cc0 9525   1c1 9526   x. cmul 9530   RR*cxr 9660   < clt 9661   <_ cle 9662   -ucneg 9847   / cdiv 10257   NNcn 10597   2c2 10647   NN0cn0 10858   ZZcz 10926   ZZ>=cuz 11148   QQcq 11253   RR+crp 11291   (,]cioc 11625   ^cexp 12265   abscabs 13307   expce 14124   Primecprime 14632   pCnt cpc 14796   ↾_s cress 15132  AbsValcabv 18054  ℂ_fldccnfld 18980   logclog 23515   ^c ccxp 23516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-inf2 8132  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602  ax-pre-sup 9603  ax-addf 9604  ax-mulf 9605

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-fal 1453  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-iin 4250  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-se 4771  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-isom 5569  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6518  df-om 6680  df-1st 6780  df-2nd 6781  df-supp 6902  df-tpos 6959  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-1o 7168  df-2o 7169  df-oadd 7172  df-er 7349  df-map 7460  df-pm 7461  df-ixp 7509  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-fsupp 7870  df-fi 7911  df-sup 7942  df-inf 7943  df-oi 8011  df-card 8359  df-cda 8584  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-5 10659  df-6 10660  df-7 10661  df-8 10662  df-9 10663  df-10 10664  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-ioo 11628  df-ioc 11629  df-ico 11630  df-icc 11631  df-fz 11775  df-fzo 11908  df-fl 12021  df-mod 12090  df-seq 12207  df-exp 12266  df-fac 12453  df-bc 12481  df-hash 12509  df-shft 13140  df-cj 13172  df-re 13173  df-im 13174  df-sqrt 13308  df-abs 13309  df-limsup 13536  df-clim 13562  df-rlim 13563  df-sum 13763  df-ef 14131  df-sin 14133  df-cos 14134  df-pi 14136  df-struct 15133  df-ndx 15134  df-slot 15135  df-base 15136  df-sets 15137  df-ress 15138  df-plusg 15213  df-mulr 15214  df-starv 15215  df-sca 15216  df-vsca 15217  df-ip 15218  df-tset 15219  df-ple 15220  df-ds 15222  df-unif 15223  df-hom 15224  df-cco 15225  df-rest 15331  df-topn 15332  df-0g 15350  df-gsum 15351  df-topgen 15352  df-pt 15353  df-prds 15356  df-xrs 15410  df-qtop 15416  df-imas 15417  df-xps 15420  df-mre 15502  df-mrc 15503  df-acs 15505  df-mgm 16498  df-sgrp 16537  df-mnd 16547  df-submnd 16593  df-grp 16683  df-minusg 16684  df-mulg 16686  df-subg 16824  df-cntz 16981  df-cmn 17442  df-mgp 17734  df-ur 17746  df-ring 17792  df-cring 17793  df-oppr 17861  df-dvdsr 17879  df-unit 17880  df-invr 17910  df-dvr 17921  df-drng 17987  df-subrg 18016  df-abv 18055  df-psmet 18972  df-xmet 18973  df-met 18974  df-bl 18975  df-mopn 18976  df-fbas 18977  df-fg 18978  df-cnfld 18981  df-top 19931  df-bases 19932  df-topon 19933  df-topsp 19934  df-cld 20044  df-ntr 20045  df-cls 20046  df-nei 20124  df-lp 20162  df-perf 20163  df-cn 20253  df-cnp 20254  df-haus 20341  df-tx 20587  df-hmeo 20780  df-fil 20871  df-fm 20963  df-flim 20964  df-flf 20965  df-xms 21345  df-ms 21346  df-tms 21347  df-cncf 21920  df-limc 22832  df-dv 22833  df-log 23517  df-cxp 23518

This theorem is referenced by:  ostth  24488