Theorem ostthlem2

Description: Lemma for ostth . Refine ostthlem1 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014) (Revised by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
	ostthlem1.1	$$⊢\phi \to F\in A$$
	ostthlem1.2	$$⊢\phi \to G\in A$$
	ostthlem2.3	$$⊢\left(\phi \wedge p\in \mathbb{P}\right)\to F\left(p\right)=G\left(p\right)$$
Assertion	ostthlem2	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
3		ostthlem1.1	$$⊢\phi \to F\in A$$
4		ostthlem1.2	$$⊢\phi \to G\in A$$
5		ostthlem2.3	$$⊢\left(\phi \wedge p\in \mathbb{P}\right)\to F\left(p\right)=G\left(p\right)$$
6		eluz2nn	$$⊢n\in {\mathbb{Z}}_{\ge 2}\to n\in \mathbb{N}$$
7		fveq2	$$⊢p=1\to F\left(p\right)=F\left(1\right)$$
8		fveq2	$$⊢p=1\to G\left(p\right)=G\left(1\right)$$
9	7 8	eqeq12d	$$⊢p=1\to \left(F\left(p\right)=G\left(p\right)\leftrightarrow F\left(1\right)=G\left(1\right)\right)$$
10	9	imbi2d	$$⊢p=1\to \left(\left(\phi \to F\left(p\right)=G\left(p\right)\right)\leftrightarrow \left(\phi \to F\left(1\right)=G\left(1\right)\right)\right)$$
11		fveq2	$$⊢p=y\to F\left(p\right)=F\left(y\right)$$
12		fveq2	$$⊢p=y\to G\left(p\right)=G\left(y\right)$$
13	11 12	eqeq12d	$$⊢p=y\to \left(F\left(p\right)=G\left(p\right)\leftrightarrow F\left(y\right)=G\left(y\right)\right)$$
14	13	imbi2d	$$⊢p=y\to \left(\left(\phi \to F\left(p\right)=G\left(p\right)\right)\leftrightarrow \left(\phi \to F\left(y\right)=G\left(y\right)\right)\right)$$
15		fveq2	$$⊢p=z\to F\left(p\right)=F\left(z\right)$$
16		fveq2	$$⊢p=z\to G\left(p\right)=G\left(z\right)$$
17	15 16	eqeq12d	$$⊢p=z\to \left(F\left(p\right)=G\left(p\right)\leftrightarrow F\left(z\right)=G\left(z\right)\right)$$
18	17	imbi2d	$$⊢p=z\to \left(\left(\phi \to F\left(p\right)=G\left(p\right)\right)\leftrightarrow \left(\phi \to F\left(z\right)=G\left(z\right)\right)\right)$$
19		fveq2	$$⊢p=yz\to F\left(p\right)=F\left(yz\right)$$
20		fveq2	$$⊢p=yz\to G\left(p\right)=G\left(yz\right)$$
21	19 20	eqeq12d	$$⊢p=yz\to \left(F\left(p\right)=G\left(p\right)\leftrightarrow F\left(yz\right)=G\left(yz\right)\right)$$
22	21	imbi2d	$$⊢p=yz\to \left(\left(\phi \to F\left(p\right)=G\left(p\right)\right)\leftrightarrow \left(\phi \to F\left(yz\right)=G\left(yz\right)\right)\right)$$
23		fveq2	$$⊢p=n\to F\left(p\right)=F\left(n\right)$$
24		fveq2	$$⊢p=n\to G\left(p\right)=G\left(n\right)$$
25	23 24	eqeq12d	$$⊢p=n\to \left(F\left(p\right)=G\left(p\right)\leftrightarrow F\left(n\right)=G\left(n\right)\right)$$
26	25	imbi2d	$$⊢p=n\to \left(\left(\phi \to F\left(p\right)=G\left(p\right)\right)\leftrightarrow \left(\phi \to F\left(n\right)=G\left(n\right)\right)\right)$$
27		ax-1ne0	$$⊢1\ne 0$$
28	1	qrng1	$$⊢1=1_Q$$
29	1	qrng0	$$⊢0=0_Q$$
30	2 28 29	abv1z	$$⊢\left(F\in A\wedge 1\ne 0\right)\to F\left(1\right)=1$$
31	3 27 30	sylancl	$$⊢\phi \to F\left(1\right)=1$$
32	2 28 29	abv1z	$$⊢\left(G\in A\wedge 1\ne 0\right)\to G\left(1\right)=1$$
33	4 27 32	sylancl	$$⊢\phi \to G\left(1\right)=1$$
34	31 33	eqtr4d	$$⊢\phi \to F\left(1\right)=G\left(1\right)$$
35	5	expcom	$$⊢p\in \mathbb{P}\to \left(\phi \to F\left(p\right)=G\left(p\right)\right)$$
36		jcab	$$⊢\left(\phi \to \left(F\left(y\right)=G\left(y\right)\wedge F\left(z\right)=G\left(z\right)\right)\right)\leftrightarrow \left(\left(\phi \to F\left(y\right)=G\left(y\right)\right)\wedge \left(\phi \to F\left(z\right)=G\left(z\right)\right)\right)$$
37		oveq12	$$⊢\left(F\left(y\right)=G\left(y\right)\wedge F\left(z\right)=G\left(z\right)\right)\to F\left(y\right)F\left(z\right)=G\left(y\right)G\left(z\right)$$
38	3	adantr	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to F\in A$$
39		eluzelz	$$⊢y\in {\mathbb{Z}}_{\ge 2}\to y\in \mathbb{Z}$$
40	39	ad2antrl	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to y\in \mathbb{Z}$$
41		zq	$$⊢y\in \mathbb{Z}\to y\in \mathbb{Q}$$
42	40 41	syl	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to y\in \mathbb{Q}$$
43		eluzelz	$$⊢z\in {\mathbb{Z}}_{\ge 2}\to z\in \mathbb{Z}$$
44	43	ad2antll	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to z\in \mathbb{Z}$$
45		zq	$$⊢z\in \mathbb{Z}\to z\in \mathbb{Q}$$
46	44 45	syl	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to z\in \mathbb{Q}$$
47	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
48		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
49		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
50	1 49	ressmulr	$$⊢\mathbb{Q}\in \mathrm{V}\to \times ={\cdot }_Q$$
51	48 50	ax-mp	$$⊢\times ={\cdot }_Q$$
52	2 47 51	abvmul	$$⊢\left(F\in A\wedge y\in \mathbb{Q}\wedge z\in \mathbb{Q}\right)\to F\left(yz\right)=F\left(y\right)F\left(z\right)$$
53	38 42 46 52	syl3anc	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to F\left(yz\right)=F\left(y\right)F\left(z\right)$$
54	4	adantr	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to G\in A$$
55	2 47 51	abvmul	$$⊢\left(G\in A\wedge y\in \mathbb{Q}\wedge z\in \mathbb{Q}\right)\to G\left(yz\right)=G\left(y\right)G\left(z\right)$$
56	54 42 46 55	syl3anc	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to G\left(yz\right)=G\left(y\right)G\left(z\right)$$
57	53 56	eqeq12d	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to \left(F\left(yz\right)=G\left(yz\right)\leftrightarrow F\left(y\right)F\left(z\right)=G\left(y\right)G\left(z\right)\right)$$
58	37 57	imbitrrid	$$⊢\left(\phi \wedge \left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\right)\to \left(\left(F\left(y\right)=G\left(y\right)\wedge F\left(z\right)=G\left(z\right)\right)\to F\left(yz\right)=G\left(yz\right)\right)$$
59	58	expcom	$$⊢\left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\to \left(\phi \to \left(\left(F\left(y\right)=G\left(y\right)\wedge F\left(z\right)=G\left(z\right)\right)\to F\left(yz\right)=G\left(yz\right)\right)\right)$$
60	59	a2d	$$⊢\left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\to \left(\left(\phi \to \left(F\left(y\right)=G\left(y\right)\wedge F\left(z\right)=G\left(z\right)\right)\right)\to \left(\phi \to F\left(yz\right)=G\left(yz\right)\right)\right)$$
61	36 60	biimtrrid	$$⊢\left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\to \left(\left(\left(\phi \to F\left(y\right)=G\left(y\right)\right)\wedge \left(\phi \to F\left(z\right)=G\left(z\right)\right)\right)\to \left(\phi \to F\left(yz\right)=G\left(yz\right)\right)\right)$$
62	10 14 18 22 26 34 35 61	prmind	$$⊢n\in \mathbb{N}\to \left(\phi \to F\left(n\right)=G\left(n\right)\right)$$
63	62	impcom	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to F\left(n\right)=G\left(n\right)$$
64	6 63	sylan2	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge 2}\right)\to F\left(n\right)=G\left(n\right)$$
65	1 2 3 4 64	ostthlem1	$$⊢\phi \to F=G$$