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

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
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 𝐽 : ℙ ⟶ 𝐴