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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
padic.j ⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
Assertion padicabvf 𝐽 : ℙ ⟶ 𝐴

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3 padic.j ⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4 qex ⊢ ℚ ∈ V
5 4 mptex ⊢ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) ∈ V
6 5 3 fnmpti ⊢ 𝐽 Fn ℙ
7 3 padicfval ⊢ ( 𝑝 ∈ ℙ → ( 𝐽 ‘ 𝑝 ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑝 ↑ - ( 𝑝 pCnt 𝑥 ) ) ) ) )
8 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
9 8 ad2antrr ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → 𝑝 ∈ ℕ )
10 9 nncnd ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → 𝑝 ∈ ℂ )
11 9 nnne0d ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → 𝑝 ≠ 0 )
12 df-ne ⊢ ( 𝑥 ≠ 0 ↔ ¬ 𝑥 = 0 )
13 pcqcl ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑥 ∈ ℚ ∧ 𝑥 ≠ 0 ) ) → ( 𝑝 pCnt 𝑥 ) ∈ ℤ )
14 13 anassrs ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ 𝑥 ≠ 0 ) → ( 𝑝 pCnt 𝑥 ) ∈ ℤ )
15 12 14 sylan2br ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑝 pCnt 𝑥 ) ∈ ℤ )
16 10 11 15 expnegd ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑝 ↑ - ( 𝑝 pCnt 𝑥 ) ) = ( 1 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑥 ) ) ) )
17 10 11 15 exprecd ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) = ( 1 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑥 ) ) ) )
18 16 17 eqtr4d ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑝 ↑ - ( 𝑝 pCnt 𝑥 ) ) = ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) )
19 18 ifeq2da ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑥 ∈ ℚ ) → if ( 𝑥 = 0 , 0 , ( 𝑝 ↑ - ( 𝑝 pCnt 𝑥 ) ) ) = if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) )
20 19 mpteq2dva ⊢ ( 𝑝 ∈ ℙ → ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑝 ↑ - ( 𝑝 pCnt 𝑥 ) ) ) ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) ) )
21 7 20 eqtrd ⊢ ( 𝑝 ∈ ℙ → ( 𝐽 ‘ 𝑝 ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) ) )
22 8 nnrecred ⊢ ( 𝑝 ∈ ℙ → ( 1 / 𝑝 ) ∈ ℝ )
23 8 nnred ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
24 prmgt1 ⊢ ( 𝑝 ∈ ℙ → 1 < 𝑝 )
25 recgt1i ⊢ ( ( 𝑝 ∈ ℝ ∧ 1 < 𝑝 ) → ( 0 < ( 1 / 𝑝 ) ∧ ( 1 / 𝑝 ) < 1 ) )
26 23 24 25 syl2anc ⊢ ( 𝑝 ∈ ℙ → ( 0 < ( 1 / 𝑝 ) ∧ ( 1 / 𝑝 ) < 1 ) )
27 26 simpld ⊢ ( 𝑝 ∈ ℙ → 0 < ( 1 / 𝑝 ) )
28 26 simprd ⊢ ( 𝑝 ∈ ℙ → ( 1 / 𝑝 ) < 1 )
29 0xr ⊢ 0 ∈ ℝ*
30 1xr ⊢ 1 ∈ ℝ*
31 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 1 / 𝑝 ) ∈ ( 0 (,) 1 ) ↔ ( ( 1 / 𝑝 ) ∈ ℝ ∧ 0 < ( 1 / 𝑝 ) ∧ ( 1 / 𝑝 ) < 1 ) ) )
32 29 30 31 mp2an ⊢ ( ( 1 / 𝑝 ) ∈ ( 0 (,) 1 ) ↔ ( ( 1 / 𝑝 ) ∈ ℝ ∧ 0 < ( 1 / 𝑝 ) ∧ ( 1 / 𝑝 ) < 1 ) )
33 22 27 28 32 syl3anbrc ⊢ ( 𝑝 ∈ ℙ → ( 1 / 𝑝 ) ∈ ( 0 (,) 1 ) )
34 eqid ⊢ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) )
35 1 2 34 padicabv ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 1 / 𝑝 ) ∈ ( 0 (,) 1 ) ) → ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) ) ∈ 𝐴 )
36 33 35 mpdan ⊢ ( 𝑝 ∈ ℙ → ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( ( 1 / 𝑝 ) ↑ ( 𝑝 pCnt 𝑥 ) ) ) ) ∈ 𝐴 )
37 21 36 eqeltrd ⊢ ( 𝑝 ∈ ℙ → ( 𝐽 ‘ 𝑝 ) ∈ 𝐴 )
38 37 rgen ⊢ ∀ 𝑝 ∈ ℙ ( 𝐽 ‘ 𝑝 ) ∈ 𝐴
39 ffnfv ⊢ ( 𝐽 : ℙ ⟶ 𝐴 ↔ ( 𝐽 Fn ℙ ∧ ∀ 𝑝 ∈ ℙ ( 𝐽 ‘ 𝑝 ) ∈ 𝐴 ) )
40 6 38 39 mpbir2an ⊢ 𝐽 : ℙ ⟶ 𝐴