Metamath Proof Explorer

Theorem padicabvf

Description: The p-adic absolute value is an absolute value. (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 padicabvf 
|- J : Prime --> 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 qex 
 |-  QQ e. _V
5 4 mptex 
 |-  ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) e. _V
6 5 3 fnmpti 
 |-  J Fn Prime
7 3 padicfval 
 |-  ( p e. Prime -> ( J ` p ) = ( x e. QQ |-> if ( x = 0 , 0 , ( p ^ -u ( p pCnt x ) ) ) ) )
8 prmnn 
 |-  ( p e. Prime -> p e. NN )
9 8 ad2antrr 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> p e. NN )
10 9 nncnd 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> p e. CC )
11 9 nnne0d 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> p =/= 0 )
12 df-ne 
 |-  ( x =/= 0 <-> -. x = 0 )
13 pcqcl 
 |-  ( ( p e. Prime /\ ( x e. QQ /\ x =/= 0 ) ) -> ( p pCnt x ) e. ZZ )
14 13 anassrs 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ x =/= 0 ) -> ( p pCnt x ) e. ZZ )
15 12 14 sylan2br 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> ( p pCnt x ) e. ZZ )
16 10 11 15 expnegd 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> ( p ^ -u ( p pCnt x ) ) = ( 1 / ( p ^ ( p pCnt x ) ) ) )
17 10 11 15 exprecd 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> ( ( 1 / p ) ^ ( p pCnt x ) ) = ( 1 / ( p ^ ( p pCnt x ) ) ) )
18 16 17 eqtr4d 
 |-  ( ( ( p e. Prime /\ x e. QQ ) /\ -. x = 0 ) -> ( p ^ -u ( p pCnt x ) ) = ( ( 1 / p ) ^ ( p pCnt x ) ) )
19 18 ifeq2da 
 |-  ( ( p e. Prime /\ x e. QQ ) -> if ( x = 0 , 0 , ( p ^ -u ( p pCnt x ) ) ) = if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) )
20 19 mpteq2dva 
 |-  ( p e. Prime -> ( x e. QQ |-> if ( x = 0 , 0 , ( p ^ -u ( p pCnt x ) ) ) ) = ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) ) )
21 7 20 eqtrd 
 |-  ( p e. Prime -> ( J ` p ) = ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) ) )
22 8 nnrecred 
 |-  ( p e. Prime -> ( 1 / p ) e. RR )
23 8 nnred 
 |-  ( p e. Prime -> p e. RR )
24 prmgt1 
 |-  ( p e. Prime -> 1 < p )
25 recgt1i 
 |-  ( ( p e. RR /\ 1 < p ) -> ( 0 < ( 1 / p ) /\ ( 1 / p ) < 1 ) )
26 23 24 25 syl2anc 
 |-  ( p e. Prime -> ( 0 < ( 1 / p ) /\ ( 1 / p ) < 1 ) )
27 26 simpld 
 |-  ( p e. Prime -> 0 < ( 1 / p ) )
28 26 simprd 
 |-  ( p e. Prime -> ( 1 / p ) < 1 )
29 0xr 
 |-  0 e. RR*
30 1xr 
 |-  1 e. RR*
31 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( 1 / p ) e. ( 0 (,) 1 ) <-> ( ( 1 / p ) e. RR /\ 0 < ( 1 / p ) /\ ( 1 / p ) < 1 ) ) )
32 29 30 31 mp2an 
 |-  ( ( 1 / p ) e. ( 0 (,) 1 ) <-> ( ( 1 / p ) e. RR /\ 0 < ( 1 / p ) /\ ( 1 / p ) < 1 ) )
33 22 27 28 32 syl3anbrc 
 |-  ( p e. Prime -> ( 1 / p ) e. ( 0 (,) 1 ) )
34 eqid 
 |-  ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) ) = ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) )
35 1 2 34 padicabv 
 |-  ( ( p e. Prime /\ ( 1 / p ) e. ( 0 (,) 1 ) ) -> ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) ) e. A )
36 33 35 mpdan 
 |-  ( p e. Prime -> ( x e. QQ |-> if ( x = 0 , 0 , ( ( 1 / p ) ^ ( p pCnt x ) ) ) ) e. A )
37 21 36 eqeltrd 
 |-  ( p e. Prime -> ( J ` p ) e. A )
38 37 rgen 
 |-  A. p e. Prime ( J ` p ) e. A
39 ffnfv 
 |-  ( J : Prime --> A <-> ( J Fn Prime /\ A. p e. Prime ( J ` p ) e. A ) )
40 6 38 39 mpbir2an 
 |-  J : Prime --> A