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	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
	padic.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
	ostth.k	$$⊢K=\left(x\in \mathbb{Q}⟼if\left(x=0,0,1\right)\right)$$
	ostth.1	$$⊢\phi \to F\in A$$
	ostth1.2	$$⊢\phi \to \forall n\in \mathbb{N}\neg 1<F\left(n\right)$$
	ostth1.3	$$⊢\phi \to \forall n\in \mathbb{P}\neg F\left(n\right)<1$$
Assertion	ostth1	$$⊢\phi \to F=K$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
3		padic.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
4		ostth.k	$$⊢K=\left(x\in \mathbb{Q}⟼if\left(x=0,0,1\right)\right)$$
5		ostth.1	$$⊢\phi \to F\in A$$
6		ostth1.2	$$⊢\phi \to \forall n\in \mathbb{N}\neg 1<F\left(n\right)$$
7		ostth1.3	$$⊢\phi \to \forall n\in \mathbb{P}\neg F\left(n\right)<1$$
8	1	qdrng	$$⊢Q\in \mathrm{DivRing}$$
9	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
10	1	qrng0	$$⊢0=0_Q$$
11	2 9 10 4	abvtriv	$$⊢Q\in \mathrm{DivRing}\to K\in A$$
12	8 11	mp1i	$$⊢\phi \to K\in A$$
13	7	r19.21bi	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to \neg F\left(n\right)<1$$
14		prmnn	$$⊢n\in \mathbb{P}\to n\in \mathbb{N}$$
15	6	r19.21bi	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \neg 1<F\left(n\right)$$
16	14 15	sylan2	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to \neg 1<F\left(n\right)$$
17		nnq	$$⊢n\in \mathbb{N}\to n\in \mathbb{Q}$$
18	14 17	syl	$$⊢n\in \mathbb{P}\to n\in \mathbb{Q}$$
19	2 9	abvcl	$$⊢\left(F\in A\wedge n\in \mathbb{Q}\right)\to F\left(n\right)\in ℝ$$
20	5 18 19	syl2an	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to F\left(n\right)\in ℝ$$
21		1re	$$⊢1\in ℝ$$
22		lttri3	$$⊢\left(F\left(n\right)\in ℝ\wedge 1\in ℝ\right)\to \left(F\left(n\right)=1\leftrightarrow \left(\neg F\left(n\right)<1\wedge \neg 1<F\left(n\right)\right)\right)$$
23	20 21 22	sylancl	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to \left(F\left(n\right)=1\leftrightarrow \left(\neg F\left(n\right)<1\wedge \neg 1<F\left(n\right)\right)\right)$$
24	13 16 23	mpbir2and	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to F\left(n\right)=1$$
25	14	adantl	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to n\in \mathbb{N}$$
26		eqeq1	$$⊢x=n\to \left(x=0\leftrightarrow n=0\right)$$
27	26	ifbid	$$⊢x=n\to if\left(x=0,0,1\right)=if\left(n=0,0,1\right)$$
28		c0ex	$$⊢0\in \mathrm{V}$$
29		1ex	$$⊢1\in \mathrm{V}$$
30	28 29	ifex	$$⊢if\left(n=0,0,1\right)\in \mathrm{V}$$
31	27 4 30	fvmpt	$$⊢n\in \mathbb{Q}\to K\left(n\right)=if\left(n=0,0,1\right)$$
32	17 31	syl	$$⊢n\in \mathbb{N}\to K\left(n\right)=if\left(n=0,0,1\right)$$
33		nnne0	$$⊢n\in \mathbb{N}\to n\ne 0$$
34	33	neneqd	$$⊢n\in \mathbb{N}\to \neg n=0$$
35	34	iffalsed	$$⊢n\in \mathbb{N}\to if\left(n=0,0,1\right)=1$$
36	32 35	eqtrd	$$⊢n\in \mathbb{N}\to K\left(n\right)=1$$
37	25 36	syl	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to K\left(n\right)=1$$
38	24 37	eqtr4d	$$⊢\left(\phi \wedge n\in \mathbb{P}\right)\to F\left(n\right)=K\left(n\right)$$
39	1 2 5 12 38	ostthlem2	$$⊢\phi \to F=K$$