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 |
⊢ 𝐽 : ℙ ⟶ 𝐴 |