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	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
	ostthlem1.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
	ostthlem1.2	⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
	ostthlem2.3	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) )
Assertion	ostthlem2	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		ostthlem1.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
4		ostthlem1.2	⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
5		ostthlem2.3	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) )
6		eluz2nn	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → 𝑛 ∈ ℕ )
7		fveq2	⊢ ( 𝑝 = 1 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 1 ) )
8		fveq2	⊢ ( 𝑝 = 1 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 1 ) )
9	7 8	eqeq12d	⊢ ( 𝑝 = 1 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
10	9	imbi2d	⊢ ( 𝑝 = 1 → ( ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) ) )
11		fveq2	⊢ ( 𝑝 = 𝑦 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑦 ) )
12		fveq2	⊢ ( 𝑝 = 𝑦 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑦 ) )
13	11 12	eqeq12d	⊢ ( 𝑝 = 𝑦 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
14	13	imbi2d	⊢ ( 𝑝 = 𝑦 → ( ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) )
15		fveq2	⊢ ( 𝑝 = 𝑧 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑧 ) )
16		fveq2	⊢ ( 𝑝 = 𝑧 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑧 ) )
17	15 16	eqeq12d	⊢ ( 𝑝 = 𝑧 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
18	17	imbi2d	⊢ ( 𝑝 = 𝑧 → ( ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
19		fveq2	⊢ ( 𝑝 = ( 𝑦 · 𝑧 ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) )
20		fveq2	⊢ ( 𝑝 = ( 𝑦 · 𝑧 ) → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) )
21	19 20	eqeq12d	⊢ ( 𝑝 = ( 𝑦 · 𝑧 ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) )
22	21	imbi2d	⊢ ( 𝑝 = ( 𝑦 · 𝑧 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
23		fveq2	⊢ ( 𝑝 = 𝑛 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑛 ) )
24		fveq2	⊢ ( 𝑝 = 𝑛 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑛 ) )
25	23 24	eqeq12d	⊢ ( 𝑝 = 𝑛 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ) )
26	25	imbi2d	⊢ ( 𝑝 = 𝑛 → ( ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ) ) )
27		ax-1ne0	⊢ 1 ≠ 0
28	1	qrng1	⊢ 1 = ( 1r ‘ 𝑄 )
29	1	qrng0	⊢ 0 = ( 0g ‘ 𝑄 )
30	2 28 29	abv1z	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )
31	3 27 30	sylancl	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 1 )
32	2 28 29	abv1z	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐺 ‘ 1 ) = 1 )
33	4 27 32	sylancl	⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 1 )
34	31 33	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
35	5	expcom	⊢ ( 𝑝 ∈ ℙ → ( 𝜑 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ) )
36		jcab	⊢ ( ( 𝜑 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( ( 𝜑 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ ( 𝜑 → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
37		oveq12	⊢ ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) )
38	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝐹 ∈ 𝐴 )
39		eluzelz	⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → 𝑦 ∈ ℤ )
40	39	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝑦 ∈ ℤ )
41		zq	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℚ )
42	40 41	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝑦 ∈ ℚ )
43		eluzelz	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
44	43	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝑧 ∈ ℤ )
45		zq	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℚ )
46	44 45	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝑧 ∈ ℚ )
47	1	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )
48		qex	⊢ ℚ ∈ V
49		cnfldmul	⊢ · = ( .r ‘ ℂfld )
50	1 49	ressmulr	⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) )
51	48 50	ax-mp	⊢ · = ( .r ‘ 𝑄 )
52	2 47 51	abvmul	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
53	38 42 46 52	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
54	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → 𝐺 ∈ 𝐴 )
55	2 47 51	abvmul	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ ) → ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) )
56	54 42 46 55	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) )
57	53 56	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
58	37 57	imbitrrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) )
59	58	expcom	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝜑 → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
60	59	a2d	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝜑 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
61	36 60	biimtrrid	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝜑 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ ( 𝜑 → ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
62	10 14 18 22 26 34 35 61	prmind	⊢ ( 𝑛 ∈ ℕ → ( 𝜑 → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ) )
63	62	impcom	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
64	6 63	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
65	1 2 3 4 64	ostthlem1	⊢ ( 𝜑 → 𝐹 = 𝐺 )