Step |
Hyp |
Ref |
Expression |
1 |
|
qrng.q |
⊢ 𝑄 = ( ℂfld ↾s ℚ ) |
2 |
|
qabsabv.a |
⊢ 𝐴 = ( AbsVal ‘ 𝑄 ) |
3 |
|
padic.j |
⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) ) |
4 |
|
ostth.k |
⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) ) |
5 |
|
ostth.1 |
⊢ ( 𝜑 → 𝐹 ∈ 𝐴 ) |
6 |
|
ostth1.2 |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) |
7 |
|
ostth1.3 |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ ¬ ( 𝐹 ‘ 𝑛 ) < 1 ) |
8 |
1
|
qdrng |
⊢ 𝑄 ∈ DivRing |
9 |
1
|
qrngbas |
⊢ ℚ = ( Base ‘ 𝑄 ) |
10 |
1
|
qrng0 |
⊢ 0 = ( 0g ‘ 𝑄 ) |
11 |
2 9 10 4
|
abvtriv |
⊢ ( 𝑄 ∈ DivRing → 𝐾 ∈ 𝐴 ) |
12 |
8 11
|
mp1i |
⊢ ( 𝜑 → 𝐾 ∈ 𝐴 ) |
13 |
7
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ¬ ( 𝐹 ‘ 𝑛 ) < 1 ) |
14 |
|
prmnn |
⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℕ ) |
15 |
6
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) |
16 |
14 15
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) |
17 |
|
nnq |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℚ ) |
18 |
14 17
|
syl |
⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℚ ) |
19 |
2 9
|
abvcl |
⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) |
20 |
5 18 19
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) |
21 |
|
1re |
⊢ 1 ∈ ℝ |
22 |
|
lttri3 |
⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) = 1 ↔ ( ¬ ( 𝐹 ‘ 𝑛 ) < 1 ∧ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ) ) |
23 |
20 21 22
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( ( 𝐹 ‘ 𝑛 ) = 1 ↔ ( ¬ ( 𝐹 ‘ 𝑛 ) < 1 ∧ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ) ) |
24 |
13 16 23
|
mpbir2and |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝐹 ‘ 𝑛 ) = 1 ) |
25 |
14
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ℕ ) |
26 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑛 → ( 𝑥 = 0 ↔ 𝑛 = 0 ) ) |
27 |
26
|
ifbid |
⊢ ( 𝑥 = 𝑛 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑛 = 0 , 0 , 1 ) ) |
28 |
|
c0ex |
⊢ 0 ∈ V |
29 |
|
1ex |
⊢ 1 ∈ V |
30 |
28 29
|
ifex |
⊢ if ( 𝑛 = 0 , 0 , 1 ) ∈ V |
31 |
27 4 30
|
fvmpt |
⊢ ( 𝑛 ∈ ℚ → ( 𝐾 ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , 1 ) ) |
32 |
17 31
|
syl |
⊢ ( 𝑛 ∈ ℕ → ( 𝐾 ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , 1 ) ) |
33 |
|
nnne0 |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 ) |
34 |
33
|
neneqd |
⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 ) |
35 |
34
|
iffalsed |
⊢ ( 𝑛 ∈ ℕ → if ( 𝑛 = 0 , 0 , 1 ) = 1 ) |
36 |
32 35
|
eqtrd |
⊢ ( 𝑛 ∈ ℕ → ( 𝐾 ‘ 𝑛 ) = 1 ) |
37 |
25 36
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝐾 ‘ 𝑛 ) = 1 ) |
38 |
24 37
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑛 ) ) |
39 |
1 2 5 12 38
|
ostthlem2 |
⊢ ( 𝜑 → 𝐹 = 𝐾 ) |