| Step | Hyp | Ref
| Expression |
| 1 | | 2sqlem6.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 2 | | 2sqlem6.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℕ) |
| 3 | | 2sqlem6.3 |
. . 3
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)) |
| 4 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1)) |
| 5 | 4 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆))) |
| 6 | 5 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 1 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆))) |
| 7 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑚 · 𝑥) = (𝑚 · 1)) |
| 8 | 7 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 1) ∈ 𝑆)) |
| 9 | 8 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 1 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 10 | 9 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 1 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 11 | 6, 10 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 1 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 12 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦)) |
| 13 | 12 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆))) |
| 14 | 13 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆))) |
| 15 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑚 · 𝑥) = (𝑚 · 𝑦)) |
| 16 | 15 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑦) ∈ 𝑆)) |
| 17 | 16 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 18 | 17 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 19 | 14, 18 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑦 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 20 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧)) |
| 21 | 20 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))) |
| 22 | 21 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))) |
| 23 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑚 · 𝑥) = (𝑚 · 𝑧)) |
| 24 | 23 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆)) |
| 25 | 24 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 26 | 25 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 27 | 22, 26 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑧 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 28 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧))) |
| 29 | 28 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆))) |
| 30 | 29 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆))) |
| 31 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑚 · 𝑥) = (𝑚 · (𝑦 · 𝑧))) |
| 32 | 31 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆)) |
| 33 | 32 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 34 | 33 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 35 | 30, 34 | imbi12d 344 |
. . . 4
⊢ (𝑥 = (𝑦 · 𝑧) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 36 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵)) |
| 37 | 36 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆))) |
| 38 | 37 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆))) |
| 39 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑚 · 𝑥) = (𝑚 · 𝐵)) |
| 40 | 39 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝐵) ∈ 𝑆)) |
| 41 | 40 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 42 | 41 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 43 | 38, 42 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝐵 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 44 | | nncn 12274 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
| 45 | 44 | mulridd 11278 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → (𝑚 · 1) = 𝑚) |
| 46 | 45 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆)) |
| 47 | 46 | biimpd 229 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)) |
| 48 | 47 | rgen 3063 |
. . . . 5
⊢
∀𝑚 ∈
ℕ ((𝑚 · 1)
∈ 𝑆 → 𝑚 ∈ 𝑆) |
| 49 | 48 | a1i 11 |
. . . 4
⊢
(∀𝑝 ∈
ℙ (𝑝 ∥ 1 →
𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)) |
| 50 | | breq1 5146 |
. . . . . . 7
⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥)) |
| 51 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑝 = 𝑥 → (𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆)) |
| 52 | 50, 51 | imbi12d 344 |
. . . . . 6
⊢ (𝑝 = 𝑥 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆))) |
| 53 | 52 | rspcv 3618 |
. . . . 5
⊢ (𝑥 ∈ ℙ →
(∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆))) |
| 54 | | prmz 16712 |
. . . . . . 7
⊢ (𝑥 ∈ ℙ → 𝑥 ∈
ℤ) |
| 55 | | iddvds 16307 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥) |
| 56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥) |
| 57 | | 2sq.1 |
. . . . . . . . . 10
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
| 58 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ ℕ) |
| 59 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ ℙ) |
| 60 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → (𝑚 · 𝑥) ∈ 𝑆) |
| 61 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
| 62 | 57, 58, 59, 60, 61 | 2sqlem5 27466 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ 𝑆) |
| 63 | 62 | expr 456 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) |
| 64 | 63 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) |
| 65 | 64 | ex 412 |
. . . . . 6
⊢ (𝑥 ∈ ℙ → (𝑥 ∈ 𝑆 → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 66 | 56, 65 | embantd 59 |
. . . . 5
⊢ (𝑥 ∈ ℙ → ((𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 67 | 53, 66 | syld 47 |
. . . 4
⊢ (𝑥 ∈ ℙ →
(∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 68 | | anim12 809 |
. . . . 5
⊢
(((∀𝑝 ∈
ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 69 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑝 ∈
ℙ) |
| 70 | | eluzelz 12888 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
| 71 | 70 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑦 ∈
ℤ) |
| 72 | | eluzelz 12888 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
| 73 | 72 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑧 ∈
ℤ) |
| 74 | | euclemma 16750 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧))) |
| 75 | 69, 71, 73, 74 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧))) |
| 76 | 75 | imbi1d 341 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆))) |
| 77 | | jaob 964 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))) |
| 78 | 76, 77 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))) |
| 79 | 78 | ralbidva 3176 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))) |
| 80 | | r19.26 3111 |
. . . . . . . . . 10
⊢
(∀𝑝 ∈
ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))) |
| 81 | 79, 80 | bitrdi 287 |
. . . . . . . . 9
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))) |
| 82 | 81 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))) |
| 83 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑚 · 𝑦) = (𝑛 · 𝑦)) |
| 84 | 83 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑚 · 𝑦) ∈ 𝑆 ↔ (𝑛 · 𝑦) ∈ 𝑆)) |
| 85 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆)) |
| 86 | 84, 85 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))) |
| 87 | 86 | cbvralvw 3237 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) |
| 88 | 44 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
| 89 | | uzssz 12899 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘2) ⊆ ℤ |
| 90 | | zsscn 12621 |
. . . . . . . . . . . . . . . . 17
⊢ ℤ
⊆ ℂ |
| 91 | 89, 90 | sstri 3993 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘2) ⊆ ℂ |
| 92 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑦 ∈
(ℤ≥‘2)) |
| 93 | 92 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈
(ℤ≥‘2)) |
| 94 | 91, 93 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℂ) |
| 95 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑧 ∈
(ℤ≥‘2)) |
| 96 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈
(ℤ≥‘2)) |
| 97 | 91, 96 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℂ) |
| 98 | | mul32 11427 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = ((𝑚 · 𝑧) · 𝑦)) |
| 99 | | mulass 11243 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = (𝑚 · (𝑦 · 𝑧))) |
| 100 | 98, 99 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧))) |
| 101 | 88, 94, 97, 100 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧))) |
| 102 | 101 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆)) |
| 103 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
| 104 | | eluz2nn 12924 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℕ) |
| 105 | 96, 104 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℕ) |
| 106 | 103, 105 | nnmulcld 12319 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑧) ∈ ℕ) |
| 107 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) |
| 108 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 · 𝑦) = ((𝑚 · 𝑧) · 𝑦)) |
| 109 | 108 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑚 · 𝑧) → ((𝑛 · 𝑦) ∈ 𝑆 ↔ ((𝑚 · 𝑧) · 𝑦) ∈ 𝑆)) |
| 110 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆)) |
| 111 | 109, 110 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 · 𝑧) → (((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) ↔ (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))) |
| 112 | 111 | rspcv 3618 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 · 𝑧) ∈ ℕ → (∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))) |
| 113 | 106, 107,
112 | sylc 65 |
. . . . . . . . . . . . 13
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)) |
| 114 | 102, 113 | sylbird 260 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)) |
| 115 | 114 | imim1d 82 |
. . . . . . . . . . 11
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 116 | 115 | ralimdva 3167 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 117 | 87, 116 | sylan2b 594 |
. . . . . . . . 9
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 118 | 117 | expimpd 453 |
. . . . . . . 8
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → ((∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 119 | 82, 118 | embantd 59 |
. . . . . . 7
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ ∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 120 | 119 | ex 412 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (∀𝑝 ∈
ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 121 | 120 | com23 86 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((∀𝑝 ∈
ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 122 | 68, 121 | syl5 34 |
. . . 4
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((∀𝑝 ∈
ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))) |
| 123 | 11, 19, 27, 35, 43, 49, 67, 122 | prmind 16723 |
. . 3
⊢ (𝐵 ∈ ℕ →
(∀𝑝 ∈ ℙ
(𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))) |
| 124 | 2, 3, 123 | sylc 65 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)) |
| 125 | | 2sqlem6.4 |
. 2
⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆) |
| 126 | | oveq1 7438 |
. . . . 5
⊢ (𝑚 = 𝐴 → (𝑚 · 𝐵) = (𝐴 · 𝐵)) |
| 127 | 126 | eleq1d 2826 |
. . . 4
⊢ (𝑚 = 𝐴 → ((𝑚 · 𝐵) ∈ 𝑆 ↔ (𝐴 · 𝐵) ∈ 𝑆)) |
| 128 | | eleq1 2829 |
. . . 4
⊢ (𝑚 = 𝐴 → (𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆)) |
| 129 | 127, 128 | imbi12d 344 |
. . 3
⊢ (𝑚 = 𝐴 → (((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆))) |
| 130 | 129 | rspcv 3618 |
. 2
⊢ (𝐴 ∈ ℕ →
(∀𝑚 ∈ ℕ
((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆))) |
| 131 | 1, 124, 125, 130 | syl3c 66 |
1
⊢ (𝜑 → 𝐴 ∈ 𝑆) |