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 = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	ostthlem1.1	$⊢ φ \to F \in A$
	ostthlem1.2	$⊢ φ \to G \in A$
	ostthlem2.3	$⊢ (φ \land p \in ℙ) \to F (p) = G (p)$
Assertion	ostthlem2	$⊢ φ \to F = G$

Proof

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

Metamath Proof Explorer

Theorem ostthlem2

Proof