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=ℂfld↾𝑠ℚ
qabsabv.a ⊢A=AbsVal⁡Q
padic.j ⊢J=q∈ℙ⟼x∈ℚ⟼ifx=00q−qpCntx
Assertion padicabvf ⊢J:ℙ⟶A

Proof

Step Hyp Ref Expression
1 qrng.q ⊢Q=ℂfld↾𝑠ℚ
2 qabsabv.a ⊢A=AbsVal⁡Q
3 padic.j ⊢J=q∈ℙ⟼x∈ℚ⟼ifx=00q−qpCntx
4 qex ⊢ℚ∈V
5 4 mptex ⊢x∈ℚ⟼ifx=00q−qpCntx∈V
6 5 3 fnmpti ⊢JFnℙ
7 3 padicfval ⊢p∈ℙ→J⁡p=x∈ℚ⟼ifx=00p−ppCntx
8 prmnn ⊢p∈ℙ→p∈ℕ
9 8 ad2antrr ⊢p∈ℙ∧x∈ℚ∧¬x=0→p∈ℕ
10 9 nncnd ⊢p∈ℙ∧x∈ℚ∧¬x=0→p∈ℂ
11 9 nnne0d ⊢p∈ℙ∧x∈ℚ∧¬x=0→p≠0
12 df-ne ⊢x≠0↔¬x=0
13 pcqcl ⊢p∈ℙ∧x∈ℚ∧x≠0→ppCntx∈ℤ
14 13 anassrs ⊢p∈ℙ∧x∈ℚ∧x≠0→ppCntx∈ℤ
15 12 14 sylan2br ⊢p∈ℙ∧x∈ℚ∧¬x=0→ppCntx∈ℤ
16 10 11 15 expnegd ⊢p∈ℙ∧x∈ℚ∧¬x=0→p−ppCntx=1pppCntx
17 10 11 15 exprecd ⊢p∈ℙ∧x∈ℚ∧¬x=0→1pppCntx=1pppCntx
18 16 17 eqtr4d ⊢p∈ℙ∧x∈ℚ∧¬x=0→p−ppCntx=1pppCntx
19 18 ifeq2da ⊢p∈ℙ∧x∈ℚ→ifx=00p−ppCntx=ifx=001pppCntx
20 19 mpteq2dva ⊢p∈ℙ→x∈ℚ⟼ifx=00p−ppCntx=x∈ℚ⟼ifx=001pppCntx
21 7 20 eqtrd ⊢p∈ℙ→J⁡p=x∈ℚ⟼ifx=001pppCntx
22 8 nnrecred ⊢p∈ℙ→1p∈ℝ
23 8 nnred ⊢p∈ℙ→p∈ℝ
24 prmgt1 ⊢p∈ℙ→1<p
25 recgt1i ⊢p∈ℝ∧1<p→0<1p∧1p<1
26 23 24 25 syl2anc ⊢p∈ℙ→0<1p∧1p<1
27 26 simpld ⊢p∈ℙ→0<1p
28 26 simprd ⊢p∈ℙ→1p<1
29 0xr ⊢0∈ℝ*
30 1xr ⊢1∈ℝ*
31 elioo2 ⊢0∈ℝ*∧1∈ℝ*→1p∈01↔1p∈ℝ∧0<1p∧1p<1
32 29 30 31 mp2an ⊢1p∈01↔1p∈ℝ∧0<1p∧1p<1
33 22 27 28 32 syl3anbrc ⊢p∈ℙ→1p∈01
34 eqid ⊢x∈ℚ⟼ifx=001pppCntx=x∈ℚ⟼ifx=001pppCntx
35 1 2 34 padicabv ⊢p∈ℙ∧1p∈01→x∈ℚ⟼ifx=001pppCntx∈A
36 33 35 mpdan ⊢p∈ℙ→x∈ℚ⟼ifx=001pppCntx∈A
37 21 36 eqeltrd ⊢p∈ℙ→J⁡p∈A
38 37 rgen ⊢∀p∈ℙJ⁡p∈A
39 ffnfv ⊢J:ℙ⟶A↔JFnℙ∧∀p∈ℙJ⁡p∈A
40 6 38 39 mpbir2an ⊢J:ℙ⟶A