Step | Hyp | Ref
| Expression |
1 | | qrng.q |
. 2
⊢ 𝑄 = (ℂfld
↾s ℚ) |
2 | | qabsabv.a |
. 2
⊢ 𝐴 = (AbsVal‘𝑄) |
3 | | ostthlem1.1 |
. 2
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
4 | | ostthlem1.2 |
. 2
⊢ (𝜑 → 𝐺 ∈ 𝐴) |
5 | | eluz2nn 12378 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) |
6 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 1 → (𝐹‘𝑝) = (𝐹‘1)) |
7 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 1 → (𝐺‘𝑝) = (𝐺‘1)) |
8 | 6, 7 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑝 = 1 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘1) = (𝐺‘1))) |
9 | 8 | imbi2d 344 |
. . . . 5
⊢ (𝑝 = 1 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘1) = (𝐺‘1)))) |
10 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑦 → (𝐹‘𝑝) = (𝐹‘𝑦)) |
11 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑦 → (𝐺‘𝑝) = (𝐺‘𝑦)) |
12 | 10, 11 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑝 = 𝑦 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑦) = (𝐺‘𝑦))) |
13 | 12 | imbi2d 344 |
. . . . 5
⊢ (𝑝 = 𝑦 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)))) |
14 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑧 → (𝐹‘𝑝) = (𝐹‘𝑧)) |
15 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑧 → (𝐺‘𝑝) = (𝐺‘𝑧)) |
16 | 14, 15 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑝 = 𝑧 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑧) = (𝐺‘𝑧))) |
17 | 16 | imbi2d 344 |
. . . . 5
⊢ (𝑝 = 𝑧 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧)))) |
18 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = (𝑦 · 𝑧) → (𝐹‘𝑝) = (𝐹‘(𝑦 · 𝑧))) |
19 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = (𝑦 · 𝑧) → (𝐺‘𝑝) = (𝐺‘(𝑦 · 𝑧))) |
20 | 18, 19 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑝 = (𝑦 · 𝑧) → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)))) |
21 | 20 | imbi2d 344 |
. . . . 5
⊢ (𝑝 = (𝑦 · 𝑧) → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) |
22 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑛 → (𝐹‘𝑝) = (𝐹‘𝑛)) |
23 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑝 = 𝑛 → (𝐺‘𝑝) = (𝐺‘𝑛)) |
24 | 22, 23 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑝 = 𝑛 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑛) = (𝐺‘𝑛))) |
25 | 24 | imbi2d 344 |
. . . . 5
⊢ (𝑝 = 𝑛 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑛) = (𝐺‘𝑛)))) |
26 | | ax-1ne0 10696 |
. . . . . . 7
⊢ 1 ≠
0 |
27 | 1 | qrng1 26370 |
. . . . . . . 8
⊢ 1 =
(1r‘𝑄) |
28 | 1 | qrng0 26369 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑄) |
29 | 2, 27, 28 | abv1z 19734 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) |
30 | 3, 26, 29 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) = 1) |
31 | 2, 27, 28 | abv1z 19734 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐺‘1) = 1) |
32 | 4, 26, 31 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝐺‘1) = 1) |
33 | 30, 32 | eqtr4d 2777 |
. . . . 5
⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) |
34 | | ostthlem2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = (𝐺‘𝑝)) |
35 | 34 | expcom 417 |
. . . . 5
⊢ (𝑝 ∈ ℙ → (𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝))) |
36 | | jcab 521 |
. . . . . 6
⊢ ((𝜑 → ((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧))) ↔ ((𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)) ∧ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧)))) |
37 | | oveq12 7191 |
. . . . . . . . 9
⊢ (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) |
38 | 3 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝐹 ∈ 𝐴) |
39 | | eluzelz 12346 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
40 | 39 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑦 ∈ ℤ) |
41 | | zq 12448 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℚ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑦 ∈ ℚ) |
43 | | eluzelz 12346 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
44 | 43 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑧 ∈ ℤ) |
45 | | zq 12448 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℚ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑧 ∈ ℚ) |
47 | 1 | qrngbas 26367 |
. . . . . . . . . . . 12
⊢ ℚ =
(Base‘𝑄) |
48 | | qex 12455 |
. . . . . . . . . . . . 13
⊢ ℚ
∈ V |
49 | | cnfldmul 20235 |
. . . . . . . . . . . . . 14
⊢ ·
= (.r‘ℂfld) |
50 | 1, 49 | ressmulr 16740 |
. . . . . . . . . . . . 13
⊢ (ℚ
∈ V → · = (.r‘𝑄)) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘𝑄) |
52 | 2, 47, 51 | abvmul 19731 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧))) |
53 | 38, 42, 46, 52 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧))) |
54 | 4 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝐺 ∈ 𝐴) |
55 | 2, 47, 51 | abvmul 19731 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝐺‘(𝑦 · 𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) |
56 | 54, 42, 46, 55 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (𝐺‘(𝑦 · 𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) |
57 | 53, 56 | eqeq12d 2755 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → ((𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)) ↔ ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧)))) |
58 | 37, 57 | syl5ibr 249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)))) |
59 | 58 | expcom 417 |
. . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝜑 → (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) |
60 | 59 | a2d 29 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝜑 → ((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧))) → (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) |
61 | 36, 60 | syl5bir 246 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)) ∧ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧))) → (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) |
62 | 9, 13, 17, 21, 25, 33, 35, 61 | prmind 16139 |
. . . 4
⊢ (𝑛 ∈ ℕ → (𝜑 → (𝐹‘𝑛) = (𝐺‘𝑛))) |
63 | 62 | impcom 411 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
64 | 5, 63 | sylan2 596 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2))
→ (𝐹‘𝑛) = (𝐺‘𝑛)) |
65 | 1, 2, 3, 4, 64 | ostthlem1 26375 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |