# Metamath Proof Explorer

## 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}}{↾}_{𝑠}ℚ$
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 ℙ\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}}{↾}_{𝑠}ℚ$
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 ℙ\right)\to {F}\left({p}\right)={G}\left({p}\right)$
6 eluz2nn ${⊢}{n}\in {ℤ}_{\ge 2}\to {n}\in ℕ$
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)↔{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)↔\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)↔{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)↔\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)↔{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)↔\left({\phi }\to {F}\left({z}\right)={G}\left({z}\right)\right)\right)$
19 fveq2 ${⊢}{p}={y}{z}\to {F}\left({p}\right)={F}\left({y}{z}\right)$
20 fveq2 ${⊢}{p}={y}{z}\to {G}\left({p}\right)={G}\left({y}{z}\right)$
21 19 20 eqeq12d ${⊢}{p}={y}{z}\to \left({F}\left({p}\right)={G}\left({p}\right)↔{F}\left({y}{z}\right)={G}\left({y}{z}\right)\right)$
22 21 imbi2d ${⊢}{p}={y}{z}\to \left(\left({\phi }\to {F}\left({p}\right)={G}\left({p}\right)\right)↔\left({\phi }\to {F}\left({y}{z}\right)={G}\left({y}{z}\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)↔{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)↔\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 ℙ\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)↔\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 {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {F}\in {A}$
39 eluzelz ${⊢}{y}\in {ℤ}_{\ge 2}\to {y}\in ℤ$
40 39 ad2antrl ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {y}\in ℤ$
41 zq ${⊢}{y}\in ℤ\to {y}\in ℚ$
42 40 41 syl ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {y}\in ℚ$
43 eluzelz ${⊢}{z}\in {ℤ}_{\ge 2}\to {z}\in ℤ$
44 43 ad2antll ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {z}\in ℤ$
45 zq ${⊢}{z}\in ℤ\to {z}\in ℚ$
46 44 45 syl ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {z}\in ℚ$
47 1 qrngbas ${⊢}ℚ={\mathrm{Base}}_{{Q}}$
48 qex ${⊢}ℚ\in \mathrm{V}$
49 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
50 1 49 ressmulr ${⊢}ℚ\in \mathrm{V}\to ×={\cdot }_{{Q}}$
51 48 50 ax-mp ${⊢}×={\cdot }_{{Q}}$
52 2 47 51 abvmul ${⊢}\left({F}\in {A}\wedge {y}\in ℚ\wedge {z}\in ℚ\right)\to {F}\left({y}{z}\right)={F}\left({y}\right){F}\left({z}\right)$
53 38 42 46 52 syl3anc ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {F}\left({y}{z}\right)={F}\left({y}\right){F}\left({z}\right)$
54 4 adantr ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {G}\in {A}$
55 2 47 51 abvmul ${⊢}\left({G}\in {A}\wedge {y}\in ℚ\wedge {z}\in ℚ\right)\to {G}\left({y}{z}\right)={G}\left({y}\right){G}\left({z}\right)$
56 54 42 46 55 syl3anc ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to {G}\left({y}{z}\right)={G}\left({y}\right){G}\left({z}\right)$
57 53 56 eqeq12d ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\ge 2}\right)\right)\to \left({F}\left({y}{z}\right)={G}\left({y}{z}\right)↔{F}\left({y}\right){F}\left({z}\right)={G}\left({y}\right){G}\left({z}\right)\right)$
58 37 57 syl5ibr ${⊢}\left({\phi }\wedge \left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\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({y}{z}\right)={G}\left({y}{z}\right)\right)$
59 58 expcom ${⊢}\left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\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({y}{z}\right)={G}\left({y}{z}\right)\right)\right)$
60 59 a2d ${⊢}\left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\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({y}{z}\right)={G}\left({y}{z}\right)\right)\right)$
61 36 60 syl5bir ${⊢}\left({y}\in {ℤ}_{\ge 2}\wedge {z}\in {ℤ}_{\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({y}{z}\right)={G}\left({y}{z}\right)\right)\right)$
62 10 14 18 22 26 34 35 61 prmind ${⊢}{n}\in ℕ\to \left({\phi }\to {F}\left({n}\right)={G}\left({n}\right)\right)$
63 62 impcom ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)={G}\left({n}\right)$
64 6 63 sylan2 ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge 2}\right)\to {F}\left({n}\right)={G}\left({n}\right)$
65 1 2 3 4 64 ostthlem1 ${⊢}{\phi }\to {F}={G}$