| Step | Hyp | Ref
| Expression |
| 1 | | prmuz2 16733 |
. . 3
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
| 2 | | euclemma 16750 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑃 ∥ (𝑥 · 𝑦) ↔ (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) |
| 3 | 2 | 3expb 1121 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑃 ∥ (𝑥 · 𝑦) ↔ (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) |
| 4 | 3 | biimpd 229 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) |
| 5 | 4 | ralrimivva 3202 |
. . 3
⊢ (𝑃 ∈ ℙ →
∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
(𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) |
| 6 | 1, 5 | jca 511 |
. 2
⊢ (𝑃 ∈ ℙ → (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦)))) |
| 7 | | simpl 482 |
. . 3
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → 𝑃 ∈
(ℤ≥‘2)) |
| 8 | | eluz2nn 12924 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∈ ℕ) |
| 10 | 9 | nnzd 12640 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∈ ℤ) |
| 11 | | iddvds 16307 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 𝑃) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∥ 𝑃) |
| 13 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
| 14 | 9, 13 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∈ ℂ) |
| 15 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℂ) |
| 16 | 15 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ∈ ℂ) |
| 17 | | nnne0 12300 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ≠ 0) |
| 18 | 17 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ≠ 0) |
| 19 | 14, 16, 18 | divcan1d 12044 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → ((𝑃 / 𝑧) · 𝑧) = 𝑃) |
| 20 | 12, 19 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∥ ((𝑃 / 𝑧) · 𝑧)) |
| 21 | 20 | adantr 480 |
. . . . . . . 8
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → 𝑃 ∥ ((𝑃 / 𝑧) · 𝑧)) |
| 22 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ∥ 𝑃) |
| 23 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ∈ ℕ) |
| 24 | | nndivdvds 16299 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℕ)) |
| 25 | 9, 23, 24 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℕ)) |
| 26 | 22, 25 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 / 𝑧) ∈ ℕ) |
| 27 | 26 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 / 𝑧) ∈ ℤ) |
| 28 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
| 29 | 28 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ∈ ℤ) |
| 30 | 27, 29 | jca 511 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → ((𝑃 / 𝑧) ∈ ℤ ∧ 𝑧 ∈ ℤ)) |
| 31 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑃 / 𝑧) → (𝑥 · 𝑦) = ((𝑃 / 𝑧) · 𝑦)) |
| 32 | 31 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑃 / 𝑧) → (𝑃 ∥ (𝑥 · 𝑦) ↔ 𝑃 ∥ ((𝑃 / 𝑧) · 𝑦))) |
| 33 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑃 / 𝑧) → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ (𝑃 / 𝑧))) |
| 34 | 33 | orbi1d 917 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑃 / 𝑧) → ((𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦) ↔ (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑦))) |
| 35 | 32, 34 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑃 / 𝑧) → ((𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦)) ↔ (𝑃 ∥ ((𝑃 / 𝑧) · 𝑦) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑦)))) |
| 36 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → ((𝑃 / 𝑧) · 𝑦) = ((𝑃 / 𝑧) · 𝑧)) |
| 37 | 36 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑃 ∥ ((𝑃 / 𝑧) · 𝑦) ↔ 𝑃 ∥ ((𝑃 / 𝑧) · 𝑧))) |
| 38 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑃 ∥ 𝑦 ↔ 𝑃 ∥ 𝑧)) |
| 39 | 38 | orbi2d 916 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑦) ↔ (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧))) |
| 40 | 37, 39 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝑃 ∥ ((𝑃 / 𝑧) · 𝑦) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑦)) ↔ (𝑃 ∥ ((𝑃 / 𝑧) · 𝑧) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧)))) |
| 41 | 35, 40 | rspc2va 3634 |
. . . . . . . . 9
⊢ ((((𝑃 / 𝑧) ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → (𝑃 ∥ ((𝑃 / 𝑧) · 𝑧) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧))) |
| 42 | 30, 41 | sylan 580 |
. . . . . . . 8
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → (𝑃 ∥ ((𝑃 / 𝑧) · 𝑧) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧))) |
| 43 | 21, 42 | mpd 15 |
. . . . . . 7
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧)) |
| 44 | | dvdsle 16347 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧ (𝑃 / 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑃 / 𝑧) → 𝑃 ≤ (𝑃 / 𝑧))) |
| 45 | 10, 26, 44 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∥ (𝑃 / 𝑧) → 𝑃 ≤ (𝑃 / 𝑧))) |
| 46 | 14 | div1d 12035 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 / 1) = 𝑃) |
| 47 | 46 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → ((𝑃 / 1) ≤ (𝑃 / 𝑧) ↔ 𝑃 ≤ (𝑃 / 𝑧))) |
| 48 | 45, 47 | sylibrd 259 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∥ (𝑃 / 𝑧) → (𝑃 / 1) ≤ (𝑃 / 𝑧))) |
| 49 | | nnrp 13046 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ+) |
| 50 | 49 | rpregt0d 13083 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ → (𝑧 ∈ ℝ ∧ 0 <
𝑧)) |
| 51 | 50 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑧 ∈ ℝ ∧ 0 < 𝑧)) |
| 52 | | 1rp 13038 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
| 53 | | rpregt0 13049 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ+ → (1 ∈ ℝ ∧ 0 < 1)) |
| 54 | 52, 53 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (1 ∈ ℝ ∧ 0 <
1)) |
| 55 | | nnrp 13046 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) |
| 56 | 9, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∈
ℝ+) |
| 57 | 56 | rpregt0d 13083 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∈ ℝ ∧ 0 < 𝑃)) |
| 58 | | lediv2 12158 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ∧ 0 <
𝑧) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ (𝑃
∈ ℝ ∧ 0 < 𝑃)) → (𝑧 ≤ 1 ↔ (𝑃 / 1) ≤ (𝑃 / 𝑧))) |
| 59 | 51, 54, 57, 58 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑧 ≤ 1 ↔ (𝑃 / 1) ≤ (𝑃 / 𝑧))) |
| 60 | 48, 59 | sylibrd 259 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∥ (𝑃 / 𝑧) → 𝑧 ≤ 1)) |
| 61 | | nnle1eq1 12296 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → (𝑧 ≤ 1 ↔ 𝑧 = 1)) |
| 62 | 61 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑧 ≤ 1 ↔ 𝑧 = 1)) |
| 63 | 60, 62 | sylibd 239 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∥ (𝑃 / 𝑧) → 𝑧 = 1)) |
| 64 | | nnnn0 12533 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ0) |
| 65 | 64 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑧 ∈ ℕ0) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ 𝑃 ∥ 𝑧) → 𝑧 ∈ ℕ0) |
| 67 | | nnnn0 12533 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) |
| 68 | 9, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → 𝑃 ∈
ℕ0) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ 𝑃 ∥ 𝑧) → 𝑃 ∈
ℕ0) |
| 70 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ 𝑃 ∥ 𝑧) → 𝑧 ∥ 𝑃) |
| 71 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ 𝑃 ∥ 𝑧) → 𝑃 ∥ 𝑧) |
| 72 | | dvdseq 16351 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℕ0
∧ 𝑃 ∈
ℕ0) ∧ (𝑧 ∥ 𝑃 ∧ 𝑃 ∥ 𝑧)) → 𝑧 = 𝑃) |
| 73 | 66, 69, 70, 71, 72 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ 𝑃 ∥ 𝑧) → 𝑧 = 𝑃) |
| 74 | 73 | ex 412 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑃 ∥ 𝑧 → 𝑧 = 𝑃)) |
| 75 | 63, 74 | orim12d 967 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → ((𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧) → (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
| 76 | 75 | imp 406 |
. . . . . . 7
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ (𝑃 ∥ (𝑃 / 𝑧) ∨ 𝑃 ∥ 𝑧)) → (𝑧 = 1 ∨ 𝑧 = 𝑃)) |
| 77 | 43, 76 | syldan 591 |
. . . . . 6
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → (𝑧 = 1 ∨ 𝑧 = 𝑃)) |
| 78 | 77 | an32s 652 |
. . . . 5
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) ∧ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃)) → (𝑧 = 1 ∨ 𝑧 = 𝑃)) |
| 79 | 78 | expr 456 |
. . . 4
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) ∧ 𝑧 ∈ ℕ) → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
| 80 | 79 | ralrimiva 3146 |
. . 3
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
| 81 | | isprm2 16719 |
. . 3
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
| 82 | 7, 80, 81 | sylanbrc 583 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))) → 𝑃 ∈ ℙ) |
| 83 | 6, 82 | impbii 209 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦)))) |