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 ⊢ 𝑄 = ( ℂ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 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) )
59 58 expcom ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝜑 → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
60 59 a2d ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝜑 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 · 𝑧 ) ) ) ) )
61 36 60 syl5bir ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 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 ⊢ ( 𝜑 → 𝐹 = 𝐺 )