Metamath Proof Explorer


Theorem padicabvcxp

Description: All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses qrng.q
|- Q = ( CCfld |`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 ) ) ) ) )
Assertion padicabvcxp
|- ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) e. A )

Proof

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 )