| 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 12924 | . . 3
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) | 
| 6 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 1 → (𝐹‘𝑝) = (𝐹‘1)) | 
| 7 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 1 → (𝐺‘𝑝) = (𝐺‘1)) | 
| 8 | 6, 7 | eqeq12d 2753 | . . . . . 6
⊢ (𝑝 = 1 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘1) = (𝐺‘1))) | 
| 9 | 8 | imbi2d 340 | . . . . 5
⊢ (𝑝 = 1 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘1) = (𝐺‘1)))) | 
| 10 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑦 → (𝐹‘𝑝) = (𝐹‘𝑦)) | 
| 11 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑦 → (𝐺‘𝑝) = (𝐺‘𝑦)) | 
| 12 | 10, 11 | eqeq12d 2753 | . . . . . 6
⊢ (𝑝 = 𝑦 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑦) = (𝐺‘𝑦))) | 
| 13 | 12 | imbi2d 340 | . . . . 5
⊢ (𝑝 = 𝑦 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)))) | 
| 14 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑧 → (𝐹‘𝑝) = (𝐹‘𝑧)) | 
| 15 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑧 → (𝐺‘𝑝) = (𝐺‘𝑧)) | 
| 16 | 14, 15 | eqeq12d 2753 | . . . . . 6
⊢ (𝑝 = 𝑧 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑧) = (𝐺‘𝑧))) | 
| 17 | 16 | imbi2d 340 | . . . . 5
⊢ (𝑝 = 𝑧 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧)))) | 
| 18 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = (𝑦 · 𝑧) → (𝐹‘𝑝) = (𝐹‘(𝑦 · 𝑧))) | 
| 19 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = (𝑦 · 𝑧) → (𝐺‘𝑝) = (𝐺‘(𝑦 · 𝑧))) | 
| 20 | 18, 19 | eqeq12d 2753 | . . . . . 6
⊢ (𝑝 = (𝑦 · 𝑧) → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)))) | 
| 21 | 20 | imbi2d 340 | . . . . 5
⊢ (𝑝 = (𝑦 · 𝑧) → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) | 
| 22 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑛 → (𝐹‘𝑝) = (𝐹‘𝑛)) | 
| 23 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑛 → (𝐺‘𝑝) = (𝐺‘𝑛)) | 
| 24 | 22, 23 | eqeq12d 2753 | . . . . . 6
⊢ (𝑝 = 𝑛 → ((𝐹‘𝑝) = (𝐺‘𝑝) ↔ (𝐹‘𝑛) = (𝐺‘𝑛))) | 
| 25 | 24 | imbi2d 340 | . . . . 5
⊢ (𝑝 = 𝑛 → ((𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ (𝜑 → (𝐹‘𝑛) = (𝐺‘𝑛)))) | 
| 26 |  | ax-1ne0 11224 | . . . . . . 7
⊢ 1 ≠
0 | 
| 27 | 1 | qrng1 27666 | . . . . . . . 8
⊢ 1 =
(1r‘𝑄) | 
| 28 | 1 | qrng0 27665 | . . . . . . . 8
⊢ 0 =
(0g‘𝑄) | 
| 29 | 2, 27, 28 | abv1z 20825 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) | 
| 30 | 3, 26, 29 | sylancl 586 | . . . . . 6
⊢ (𝜑 → (𝐹‘1) = 1) | 
| 31 | 2, 27, 28 | abv1z 20825 | . . . . . . 7
⊢ ((𝐺 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐺‘1) = 1) | 
| 32 | 4, 26, 31 | sylancl 586 | . . . . . 6
⊢ (𝜑 → (𝐺‘1) = 1) | 
| 33 | 30, 32 | eqtr4d 2780 | . . . . 5
⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) | 
| 34 |  | ostthlem2.3 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = (𝐺‘𝑝)) | 
| 35 | 34 | expcom 413 | . . . . 5
⊢ (𝑝 ∈ ℙ → (𝜑 → (𝐹‘𝑝) = (𝐺‘𝑝))) | 
| 36 |  | jcab 517 | . . . . . 6
⊢ ((𝜑 → ((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧))) ↔ ((𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)) ∧ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧)))) | 
| 37 |  | oveq12 7440 | . . . . . . . . 9
⊢ (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) | 
| 38 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝐹 ∈ 𝐴) | 
| 39 |  | eluzelz 12888 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) | 
| 40 | 39 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑦 ∈ ℤ) | 
| 41 |  | zq 12996 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℚ) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑦 ∈ ℚ) | 
| 43 |  | eluzelz 12888 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) | 
| 44 | 43 | ad2antll 729 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑧 ∈ ℤ) | 
| 45 |  | zq 12996 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℚ) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝑧 ∈ ℚ) | 
| 47 | 1 | qrngbas 27663 | . . . . . . . . . . . 12
⊢ ℚ =
(Base‘𝑄) | 
| 48 |  | qex 13003 | . . . . . . . . . . . . 13
⊢ ℚ
∈ V | 
| 49 |  | cnfldmul 21372 | . . . . . . . . . . . . . 14
⊢  ·
= (.r‘ℂfld) | 
| 50 | 1, 49 | ressmulr 17351 | . . . . . . . . . . . . 13
⊢ (ℚ
∈ V → · = (.r‘𝑄)) | 
| 51 | 48, 50 | ax-mp 5 | . . . . . . . . . . . 12
⊢  ·
= (.r‘𝑄) | 
| 52 | 2, 47, 51 | abvmul 20822 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧))) | 
| 53 | 38, 42, 46, 52 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧))) | 
| 54 | 4 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → 𝐺 ∈ 𝐴) | 
| 55 | 2, 47, 51 | abvmul 20822 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐴 ∧ 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝐺‘(𝑦 · 𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) | 
| 56 | 54, 42, 46, 55 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (𝐺‘(𝑦 · 𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧))) | 
| 57 | 53, 56 | eqeq12d 2753 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → ((𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)) ↔ ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝐺‘𝑦) · (𝐺‘𝑧)))) | 
| 58 | 37, 57 | imbitrrid 246 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (ℤ≥‘2)
∧ 𝑧 ∈
(ℤ≥‘2))) → (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧)))) | 
| 59 | 58 | expcom 413 | . . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝜑 → (((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧)) → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) | 
| 60 | 59 | a2d 29 | . . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝜑 → ((𝐹‘𝑦) = (𝐺‘𝑦) ∧ (𝐹‘𝑧) = (𝐺‘𝑧))) → (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) | 
| 61 | 36, 60 | biimtrrid 243 | . . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((𝜑 → (𝐹‘𝑦) = (𝐺‘𝑦)) ∧ (𝜑 → (𝐹‘𝑧) = (𝐺‘𝑧))) → (𝜑 → (𝐹‘(𝑦 · 𝑧)) = (𝐺‘(𝑦 · 𝑧))))) | 
| 62 | 9, 13, 17, 21, 25, 33, 35, 61 | prmind 16723 | . . . 4
⊢ (𝑛 ∈ ℕ → (𝜑 → (𝐹‘𝑛) = (𝐺‘𝑛))) | 
| 63 | 62 | impcom 407 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐺‘𝑛)) | 
| 64 | 5, 63 | sylan2 593 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2))
→ (𝐹‘𝑛) = (𝐺‘𝑛)) | 
| 65 | 1, 2, 3, 4, 64 | ostthlem1 27671 | 1
⊢ (𝜑 → 𝐹 = 𝐺) |