Proof of Theorem prime
Step | Hyp | Ref
| Expression |
1 | | nnz 8679 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
2 | | 1z 8686 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
3 | | zdceq 8732 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 1 ∈
ℤ) → DECID 𝑥 = 1) |
4 | 2, 3 | mpan2 416 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ →
DECID 𝑥 =
1) |
5 | | dfordc 827 |
. . . . . . . 8
⊢
(DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴))) |
6 | | df-ne 2252 |
. . . . . . . . 9
⊢ (𝑥 ≠ 1 ↔ ¬ 𝑥 = 1) |
7 | 6 | imbi1i 236 |
. . . . . . . 8
⊢ ((𝑥 ≠ 1 → 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴)) |
8 | 5, 7 | syl6bbr 196 |
. . . . . . 7
⊢
(DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
9 | 1, 4, 8 | 3syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
10 | 9 | imbi2d 228 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴)))) |
11 | | impexp 259 |
. . . . . 6
⊢ (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴))) |
12 | | bi2.04 246 |
. . . . . 6
⊢ ((𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
13 | 11, 12 | bitri 182 |
. . . . 5
⊢ (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴))) |
14 | 10, 13 | syl6bbr 196 |
. . . 4
⊢ (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
15 | 14 | adantl 271 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
16 | | nngt1ne1 8368 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (1 <
𝑥 ↔ 𝑥 ≠ 1)) |
17 | 16 | adantl 271 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (1 <
𝑥 ↔ 𝑥 ≠ 1)) |
18 | 17 | anbi1d 453 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
19 | | nnz 8679 |
. . . . . . . . 9
⊢ ((𝐴 / 𝑥) ∈ ℕ → (𝐴 / 𝑥) ∈ ℤ) |
20 | | nnre 8341 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
21 | | gtndiv 8751 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ ∧ 𝐴 < 𝑥) → ¬ (𝐴 / 𝑥) ∈ ℤ) |
22 | 21 | 3expia 1143 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ)) |
23 | 20, 22 | sylan 277 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ)) |
24 | 23 | con2d 587 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → ¬ 𝐴 < 𝑥)) |
25 | | nnre 8341 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
26 | | lenlt 7482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
27 | 20, 25, 26 | syl2an 283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
28 | 24, 27 | sylibrd 167 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥 ≤ 𝐴)) |
29 | 28 | ancoms 264 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥 ≤ 𝐴)) |
30 | 19, 29 | syl5 32 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 ≤ 𝐴)) |
31 | 30 | pm4.71rd 386 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ ↔ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
32 | 31 | anbi2d 452 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))) |
33 | | 3anass 926 |
. . . . . 6
⊢ ((1 <
𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
34 | 32, 33 | syl6bbr 196 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 <
𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
35 | 18, 34 | bitr3d 188 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))) |
36 | 35 | imbi1d 229 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
37 | 15, 36 | bitrd 186 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
38 | 37 | ralbidva 2372 |
1
⊢ (𝐴 ∈ ℕ →
(∀𝑥 ∈ ℕ
((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |