Metamath Proof Explorer


Theorem ostth1

Description: - Lemma for ostth : trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If F is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul of the absolute value, F is equal to 1 on all the integers, and ostthlem1 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 𝑄 = ( ℂflds ℚ )
qabsabv.a 𝐴 = ( AbsVal ‘ 𝑄 )
padic.j 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
ostth.k 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
ostth.1 ( 𝜑𝐹𝐴 )
ostth1.2 ( 𝜑 → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹𝑛 ) )
ostth1.3 ( 𝜑 → ∀ 𝑛 ∈ ℙ ¬ ( 𝐹𝑛 ) < 1 )
Assertion ostth1 ( 𝜑𝐹 = 𝐾 )

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
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 ( 𝜑𝐹 = 𝐾 )