Proof of Theorem nn01to3
Step | Hyp | Ref
| Expression |
1 | | 3mix3 1225 |
. . 3
⊢ (𝑁 = 3 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
2 | 1 | a1d 25 |
. 2
⊢ (𝑁 = 3 → ((𝑁 ∈ ℕ0 ∧ 1 ≤
𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
3 | | nn0re 11178 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
4 | 3 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 𝑁 ∈
ℝ) |
5 | | 3re 10971 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 3 ∈
ℝ) |
7 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 𝑁 ≤ 3) |
8 | 4, 6, 7 | leltned 10069 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 < 3 ↔ 3 ≠ 𝑁)) |
9 | | nesym 2838 |
. . . . . . . 8
⊢ (3 ≠
𝑁 ↔ ¬ 𝑁 = 3) |
10 | 8, 9 | syl6rbb 276 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (¬ 𝑁 = 3 ↔ 𝑁 < 3)) |
11 | | elnnnn0c 11215 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁)) |
12 | | orc 399 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → (𝑁 = 1 ∨ 𝑁 = 2)) |
13 | 12 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
14 | 13 | a1d 25 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → (𝑁 ∈ ℕ → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2)))) |
15 | | eluz2b3 11638 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
16 | | eluz2 11569 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
17 | | 2a1 28 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = 2 → ((2 ∈ ℤ
∧ 𝑁 ∈ ℤ
∧ 2 ≤ 𝑁) →
(𝑁 < 3 → 𝑁 = 2))) |
18 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 ∈
ℤ → 2 ∈ ℝ) |
19 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
20 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 ≤
𝑁 → 2 ≤ 𝑁) |
21 | | leltne 10006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 2 ≤ 𝑁) → (2 < 𝑁 ↔ 𝑁 ≠ 2)) |
22 | 18, 19, 20, 21 | syl3an 1360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (2 < 𝑁 ↔ 𝑁 ≠ 2)) |
23 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℤ |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℤ ∧ 𝑁 < 3) ∧ 2 < 𝑁) → 2 ∈
ℤ) |
25 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℤ ∧ 𝑁 < 3) ∧ 2 < 𝑁) → 2 < 𝑁) |
26 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 = (2 +
1) |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → 3 = (2 +
1)) |
28 | 27 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → (𝑁 < 3 ↔ 𝑁 < (2 + 1))) |
29 | 28 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 3) → 𝑁 < (2 + 1)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℤ ∧ 𝑁 < 3) ∧ 2 < 𝑁) → 𝑁 < (2 + 1)) |
31 | | btwnnz 11329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℤ ∧ 2 < 𝑁 ∧ 𝑁 < (2 + 1)) → ¬ 𝑁 ∈
ℤ) |
32 | 24, 25, 30, 31 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℤ ∧ 𝑁 < 3) ∧ 2 < 𝑁) → ¬ 𝑁 ∈ ℤ) |
33 | 32 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℤ ∧ 𝑁 < 3) ∧ 2 < 𝑁) → (𝑁 ∈ ℤ → 𝑁 = 2)) |
34 | 33 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → (𝑁 < 3 → (2 < 𝑁 → (𝑁 ∈ ℤ → 𝑁 = 2)))) |
35 | 34 | com24 93 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ → (2 <
𝑁 → (𝑁 < 3 → 𝑁 = 2)))) |
36 | 35 | pm2.43i 50 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
37 | 36 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (2 < 𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
38 | 22, 37 | sylbird 249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (𝑁 ≠ 2 → (𝑁 < 3 → 𝑁 = 2))) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ≠ 2 → ((2 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 2 ≤ 𝑁)
→ (𝑁 < 3 →
𝑁 = 2))) |
40 | 17, 39 | pm2.61ine 2865 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (𝑁 < 3 → 𝑁 = 2)) |
41 | 16, 40 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 3 → 𝑁 = 2)) |
42 | 41 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 < 3) → 𝑁 = 2) |
43 | 42 | olcd 407 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 < 3) → (𝑁 = 1 ∨ 𝑁 = 2)) |
44 | 43 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
45 | 15, 44 | sylbir 224 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
46 | 45 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑁 ≠ 1 → (𝑁 ∈ ℕ → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2)))) |
47 | 14, 46 | pm2.61ine 2865 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
48 | 11, 47 | sylbir 224 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁) →
(𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
49 | 48 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 < 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
50 | 10, 49 | sylbid 229 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (¬ 𝑁 = 3 → (𝑁 = 1 ∨ 𝑁 = 2))) |
51 | 50 | impcom 445 |
. . . . 5
⊢ ((¬
𝑁 = 3 ∧ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3)) → (𝑁 = 1 ∨ 𝑁 = 2)) |
52 | 51 | orcd 406 |
. . . 4
⊢ ((¬
𝑁 = 3 ∧ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3)) → ((𝑁 = 1 ∨ 𝑁 = 2) ∨ 𝑁 = 3)) |
53 | | df-3or 1032 |
. . . 4
⊢ ((𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3) ↔ ((𝑁 = 1 ∨ 𝑁 = 2) ∨ 𝑁 = 3)) |
54 | 52, 53 | sylibr 223 |
. . 3
⊢ ((¬
𝑁 = 3 ∧ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3)) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
55 | 54 | ex 449 |
. 2
⊢ (¬
𝑁 = 3 → ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
56 | 2, 55 | pm2.61i 175 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |