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 syl5eq 
 |-  ( ( ( 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 )