Proof of Theorem prime
Step | Hyp | Ref
| Expression |
1 | | nnz 8264 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
2 | | 1z 8271 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
3 | | zdceq 8316 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 1 ∈
ℤ) → DECID 𝑥 = 1) |
4 | 2, 3 | mpan2 401 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ →
DECID 𝑥 =
1) |
5 | | dfordc 791 |
. . . . . . . 8
⊢
(DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴))) |
6 | | df-ne 2206 |
. . . . . . . . 9
⊢ (𝑥 ≠ 1 ↔ ¬ 𝑥 = 1) |
7 | 6 | imbi1i 227 |
. . . . . . . 8
⊢ ((𝑥 ≠ 1 → 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴)) |
8 | 5, 7 | syl6bbr 187 |
. . . . . . 7
⊢
(DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
9 | 1, 4, 8 | 3syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
10 | 9 | imbi2d 219 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴)))) |
11 | | impexp 250 |
. . . . . 6
⊢ (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴))) |
12 | | bi2.04 237 |
. . . . . 6
⊢ ((𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
13 | 11, 12 | bitri 173 |
. . . . 5
⊢ (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
14 | 10, 13 | syl6bbr 187 |
. . . 4
⊢ (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
15 | 14 | adantl 262 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
16 | | nngt1ne1 7948 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (1 <
𝑥 ↔ 𝑥 ≠ 1)) |
17 | 16 | adantl 262 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (1 <
𝑥 ↔ 𝑥 ≠ 1)) |
18 | 17 | anbi1d 438 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
19 | | nnz 8264 |
. . . . . . . . 9
⊢ ((𝐴 / 𝑥) ∈ ℕ → (𝐴 / 𝑥) ∈ ℤ) |
20 | | nnre 7921 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
21 | | gtndiv 8335 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ ∧ 𝐴 < 𝑥) → ¬ (𝐴 / 𝑥) ∈ ℤ) |
22 | 21 | 3expia 1106 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ)) |
23 | 20, 22 | sylan 267 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ)) |
24 | 23 | con2d 554 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → ¬ 𝐴 < 𝑥)) |
25 | | nnre 7921 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
26 | | lenlt 7094 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
27 | 20, 25, 26 | syl2an 273 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
28 | 24, 27 | sylibrd 158 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥 ≤ 𝐴)) |
29 | 28 | ancoms 255 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥 ≤ 𝐴)) |
30 | 19, 29 | syl5 28 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 ≤ 𝐴)) |
31 | 30 | pm4.71rd 374 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ ↔ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
32 | 31 | anbi2d 437 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))) |
33 | | 3anass 889 |
. . . . . 6
⊢ ((1 <
𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
34 | 32, 33 | syl6bbr 187 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
35 | 18, 34 | bitr3d 179 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
36 | 35 | imbi1d 220 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
37 | 15, 36 | bitrd 177 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
38 | 37 | ralbidva 2322 |
1
⊢ (𝐴 ∈ ℕ →
(∀𝑥 ∈ ℕ
((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |