Step |
Hyp |
Ref |
Expression |
1 |
|
qrng.q |
|- Q = ( CCfld |`s QQ ) |
2 |
|
qabsabv.a |
|- A = ( AbsVal ` Q ) |
3 |
|
padic.j |
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) ) |
4 |
3
|
padicval |
|- ( ( P e. Prime /\ y e. QQ ) -> ( ( J ` P ) ` y ) = if ( y = 0 , 0 , ( P ^ -u ( P pCnt y ) ) ) ) |
5 |
4
|
adantlr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> ( ( J ` P ) ` y ) = if ( y = 0 , 0 , ( P ^ -u ( P pCnt y ) ) ) ) |
6 |
5
|
oveq1d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> ( ( ( J ` P ) ` y ) ^c R ) = ( if ( y = 0 , 0 , ( P ^ -u ( P pCnt y ) ) ) ^c R ) ) |
7 |
|
ovif |
|- ( if ( y = 0 , 0 , ( P ^ -u ( P pCnt y ) ) ) ^c R ) = if ( y = 0 , ( 0 ^c R ) , ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) |
8 |
|
rpre |
|- ( R e. RR+ -> R e. RR ) |
9 |
8
|
adantl |
|- ( ( P e. Prime /\ R e. RR+ ) -> R e. RR ) |
10 |
9
|
recnd |
|- ( ( P e. Prime /\ R e. RR+ ) -> R e. CC ) |
11 |
|
rpne0 |
|- ( R e. RR+ -> R =/= 0 ) |
12 |
11
|
adantl |
|- ( ( P e. Prime /\ R e. RR+ ) -> R =/= 0 ) |
13 |
10 12
|
0cxpd |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( 0 ^c R ) = 0 ) |
14 |
13
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> ( 0 ^c R ) = 0 ) |
15 |
14
|
ifeq1d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> if ( y = 0 , ( 0 ^c R ) , ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) = if ( y = 0 , 0 , ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) ) |
16 |
7 15
|
eqtrid |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> ( if ( y = 0 , 0 , ( P ^ -u ( P pCnt y ) ) ) ^c R ) = if ( y = 0 , 0 , ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) ) |
17 |
|
df-ne |
|- ( y =/= 0 <-> -. y = 0 ) |
18 |
|
pcqcl |
|- ( ( P e. Prime /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P pCnt y ) e. ZZ ) |
19 |
18
|
adantlr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P pCnt y ) e. ZZ ) |
20 |
19
|
zcnd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P pCnt y ) e. CC ) |
21 |
10
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> R e. CC ) |
22 |
|
mulneg12 |
|- ( ( ( P pCnt y ) e. CC /\ R e. CC ) -> ( -u ( P pCnt y ) x. R ) = ( ( P pCnt y ) x. -u R ) ) |
23 |
20 21 22
|
syl2anc |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( -u ( P pCnt y ) x. R ) = ( ( P pCnt y ) x. -u R ) ) |
24 |
21
|
negcld |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> -u R e. CC ) |
25 |
20 24
|
mulcomd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( ( P pCnt y ) x. -u R ) = ( -u R x. ( P pCnt y ) ) ) |
26 |
23 25
|
eqtrd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( -u ( P pCnt y ) x. R ) = ( -u R x. ( P pCnt y ) ) ) |
27 |
26
|
oveq2d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c ( -u ( P pCnt y ) x. R ) ) = ( P ^c ( -u R x. ( P pCnt y ) ) ) ) |
28 |
|
prmuz2 |
|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) ) |
29 |
28
|
adantr |
|- ( ( P e. Prime /\ R e. RR+ ) -> P e. ( ZZ>= ` 2 ) ) |
30 |
|
eluz2b2 |
|- ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) ) |
31 |
29 30
|
sylib |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P e. NN /\ 1 < P ) ) |
32 |
31
|
simpld |
|- ( ( P e. Prime /\ R e. RR+ ) -> P e. NN ) |
33 |
32
|
nnrpd |
|- ( ( P e. Prime /\ R e. RR+ ) -> P e. RR+ ) |
34 |
33
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> P e. RR+ ) |
35 |
19
|
znegcld |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> -u ( P pCnt y ) e. ZZ ) |
36 |
35
|
zred |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> -u ( P pCnt y ) e. RR ) |
37 |
34 36 21
|
cxpmuld |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c ( -u ( P pCnt y ) x. R ) ) = ( ( P ^c -u ( P pCnt y ) ) ^c R ) ) |
38 |
9
|
renegcld |
|- ( ( P e. Prime /\ R e. RR+ ) -> -u R e. RR ) |
39 |
38
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> -u R e. RR ) |
40 |
34 39 20
|
cxpmuld |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c ( -u R x. ( P pCnt y ) ) ) = ( ( P ^c -u R ) ^c ( P pCnt y ) ) ) |
41 |
27 37 40
|
3eqtr3d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( ( P ^c -u ( P pCnt y ) ) ^c R ) = ( ( P ^c -u R ) ^c ( P pCnt y ) ) ) |
42 |
32
|
nnred |
|- ( ( P e. Prime /\ R e. RR+ ) -> P e. RR ) |
43 |
42
|
recnd |
|- ( ( P e. Prime /\ R e. RR+ ) -> P e. CC ) |
44 |
43
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> P e. CC ) |
45 |
32
|
nnne0d |
|- ( ( P e. Prime /\ R e. RR+ ) -> P =/= 0 ) |
46 |
45
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> P =/= 0 ) |
47 |
44 46 35
|
cxpexpzd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c -u ( P pCnt y ) ) = ( P ^ -u ( P pCnt y ) ) ) |
48 |
47
|
oveq1d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( ( P ^c -u ( P pCnt y ) ) ^c R ) = ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) |
49 |
33 38
|
rpcxpcld |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c -u R ) e. RR+ ) |
50 |
49
|
adantr |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c -u R ) e. RR+ ) |
51 |
50
|
rpcnd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c -u R ) e. CC ) |
52 |
50
|
rpne0d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P ^c -u R ) =/= 0 ) |
53 |
51 52 19
|
cxpexpzd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( ( P ^c -u R ) ^c ( P pCnt y ) ) = ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) |
54 |
41 48 53
|
3eqtr3d |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( ( P ^ -u ( P pCnt y ) ) ^c R ) = ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) |
55 |
54
|
anassrs |
|- ( ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) /\ y =/= 0 ) -> ( ( P ^ -u ( P pCnt y ) ) ^c R ) = ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) |
56 |
17 55
|
sylan2br |
|- ( ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) /\ -. y = 0 ) -> ( ( P ^ -u ( P pCnt y ) ) ^c R ) = ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) |
57 |
56
|
ifeq2da |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> if ( y = 0 , 0 , ( ( P ^ -u ( P pCnt y ) ) ^c R ) ) = if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) |
58 |
6 16 57
|
3eqtrd |
|- ( ( ( P e. Prime /\ R e. RR+ ) /\ y e. QQ ) -> ( ( ( J ` P ) ` y ) ^c R ) = if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) |
59 |
58
|
mpteq2dva |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) = ( y e. QQ |-> if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) ) |
60 |
|
rpre |
|- ( ( P ^c -u R ) e. RR+ -> ( P ^c -u R ) e. RR ) |
61 |
49 60
|
syl |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c -u R ) e. RR ) |
62 |
|
rpgt0 |
|- ( ( P ^c -u R ) e. RR+ -> 0 < ( P ^c -u R ) ) |
63 |
49 62
|
syl |
|- ( ( P e. Prime /\ R e. RR+ ) -> 0 < ( P ^c -u R ) ) |
64 |
|
rpgt0 |
|- ( R e. RR+ -> 0 < R ) |
65 |
64
|
adantl |
|- ( ( P e. Prime /\ R e. RR+ ) -> 0 < R ) |
66 |
9
|
lt0neg2d |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( 0 < R <-> -u R < 0 ) ) |
67 |
65 66
|
mpbid |
|- ( ( P e. Prime /\ R e. RR+ ) -> -u R < 0 ) |
68 |
31
|
simprd |
|- ( ( P e. Prime /\ R e. RR+ ) -> 1 < P ) |
69 |
|
0red |
|- ( ( P e. Prime /\ R e. RR+ ) -> 0 e. RR ) |
70 |
42 68 38 69
|
cxpltd |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( -u R < 0 <-> ( P ^c -u R ) < ( P ^c 0 ) ) ) |
71 |
67 70
|
mpbid |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c -u R ) < ( P ^c 0 ) ) |
72 |
43
|
cxp0d |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c 0 ) = 1 ) |
73 |
71 72
|
breqtrd |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c -u R ) < 1 ) |
74 |
|
0xr |
|- 0 e. RR* |
75 |
|
1xr |
|- 1 e. RR* |
76 |
|
elioo2 |
|- ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( P ^c -u R ) e. ( 0 (,) 1 ) <-> ( ( P ^c -u R ) e. RR /\ 0 < ( P ^c -u R ) /\ ( P ^c -u R ) < 1 ) ) ) |
77 |
74 75 76
|
mp2an |
|- ( ( P ^c -u R ) e. ( 0 (,) 1 ) <-> ( ( P ^c -u R ) e. RR /\ 0 < ( P ^c -u R ) /\ ( P ^c -u R ) < 1 ) ) |
78 |
61 63 73 77
|
syl3anbrc |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( P ^c -u R ) e. ( 0 (,) 1 ) ) |
79 |
|
eqid |
|- ( y e. QQ |-> if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) = ( y e. QQ |-> if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) |
80 |
1 2 79
|
padicabv |
|- ( ( P e. Prime /\ ( P ^c -u R ) e. ( 0 (,) 1 ) ) -> ( y e. QQ |-> if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) e. A ) |
81 |
78 80
|
syldan |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> if ( y = 0 , 0 , ( ( P ^c -u R ) ^ ( P pCnt y ) ) ) ) e. A ) |
82 |
59 81
|
eqeltrd |
|- ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) e. A ) |