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	⊢ 𝑄 = ( ℂ_fld ↾_s ℚ )
	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	⊢ 𝑄 = ( ℂ_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 = ( 0_g ‘ 𝑄 )
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	⊢ ( 𝜑 → 𝐹 = 𝐾 )

Metamath Proof Explorer

Theorem ostth1

Proof