Proof of Theorem isprm2lem
| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 𝑃 ≠ 1) |
| 2 | 1 | necomd 2996 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 1 ≠ 𝑃) |
| 3 | | simpr 484 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) |
| 4 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
| 5 | | 1dvds 16308 |
. . . . . . . 8
⊢ (𝑃 ∈ ℤ → 1 ∥
𝑃) |
| 6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → 1 ∥
𝑃) |
| 7 | 6 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 1 ∥
𝑃) |
| 8 | | 1nn 12277 |
. . . . . . 7
⊢ 1 ∈
ℕ |
| 9 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑛 ∥ 𝑃 ↔ 1 ∥ 𝑃)) |
| 10 | 9 | elrab3 3693 |
. . . . . . 7
⊢ (1 ∈
ℕ → (1 ∈ {𝑛
∈ ℕ ∣ 𝑛
∥ 𝑃} ↔ 1 ∥
𝑃)) |
| 11 | 8, 10 | ax-mp 5 |
. . . . . 6
⊢ (1 ∈
{𝑛 ∈ ℕ ∣
𝑛 ∥ 𝑃} ↔ 1 ∥ 𝑃) |
| 12 | 7, 11 | sylibr 234 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 1 ∈
{𝑛 ∈ ℕ ∣
𝑛 ∥ 𝑃}) |
| 13 | | iddvds 16307 |
. . . . . . . 8
⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 𝑃) |
| 14 | 4, 13 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → 𝑃 ∥ 𝑃) |
| 15 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 𝑃 ∥ 𝑃) |
| 16 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑛 = 𝑃 → (𝑛 ∥ 𝑃 ↔ 𝑃 ∥ 𝑃)) |
| 17 | 16 | elrab3 3693 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → (𝑃 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ↔ 𝑃 ∥ 𝑃)) |
| 18 | 17 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → (𝑃 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ↔ 𝑃 ∥ 𝑃)) |
| 19 | 15, 18 | mpbird 257 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → 𝑃 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃}) |
| 20 | | en2eqpr 10047 |
. . . . 5
⊢ (({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ∧ 1 ∈
{𝑛 ∈ ℕ ∣
𝑛 ∥ 𝑃} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃}) → (1 ≠ 𝑃 → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃})) |
| 21 | 3, 12, 19, 20 | syl3anc 1373 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → (1 ≠
𝑃 → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃})) |
| 22 | 2, 21 | mpd 15 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}) |
| 23 | 22 | ex 412 |
. 2
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃})) |
| 24 | | necom 2994 |
. . . 4
⊢ (1 ≠
𝑃 ↔ 𝑃 ≠ 1) |
| 25 | | pr2ne 10044 |
. . . . . 6
⊢ ((1
∈ ℕ ∧ 𝑃
∈ ℕ) → ({1, 𝑃} ≈ 2o ↔ 1 ≠ 𝑃)) |
| 26 | 8, 25 | mpan 690 |
. . . . 5
⊢ (𝑃 ∈ ℕ → ({1,
𝑃} ≈ 2o
↔ 1 ≠ 𝑃)) |
| 27 | 26 | biimpar 477 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 1 ≠
𝑃) → {1, 𝑃} ≈
2o) |
| 28 | 24, 27 | sylan2br 595 |
. . 3
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → {1, 𝑃} ≈
2o) |
| 29 | | breq1 5146 |
. . 3
⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃} → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {1, 𝑃} ≈
2o)) |
| 30 | 28, 29 | syl5ibrcom 247 |
. 2
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃} → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o)) |
| 31 | 23, 30 | impbid 212 |
1
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃})) |