Proof of Theorem nn01to3
Step | Hyp | Ref
| Expression |
1 | | simp2 905 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 1 ≤ 𝑁) |
2 | | simp1 904 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 𝑁 ∈
ℕ0) |
3 | | 1z 8271 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
4 | | nn0z 8265 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
5 | | zleloe 8292 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 ≤ 𝑁 ↔ (1 < 𝑁 ∨ 1 = 𝑁))) |
6 | 3, 4, 5 | sylancr 393 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (1 ≤ 𝑁 ↔ (1
< 𝑁 ∨ 1 = 𝑁))) |
7 | 2, 6 | syl 14 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 ≤ 𝑁 ↔ (1 < 𝑁 ∨ 1 = 𝑁))) |
8 | 1, 7 | mpbid 135 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 < 𝑁 ∨ 1 = 𝑁)) |
9 | | 1nn0 8197 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
10 | | nn0ltp1le 8306 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (1 <
𝑁 ↔ (1 + 1) ≤ 𝑁)) |
11 | 9, 10 | mpan 400 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (1
+ 1) ≤ 𝑁)) |
12 | | df-2 7973 |
. . . . . . . . . . 11
⊢ 2 = (1 +
1) |
13 | 12 | breq1i 3771 |
. . . . . . . . . 10
⊢ (2 ≤
𝑁 ↔ (1 + 1) ≤ 𝑁) |
14 | 11, 13 | syl6bbr 187 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ 2
≤ 𝑁)) |
15 | | 2z 8273 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
16 | | zleloe 8292 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 ≤ 𝑁 ↔ (2 < 𝑁 ∨ 2 = 𝑁))) |
17 | 15, 4, 16 | sylancr 393 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (2 ≤ 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
18 | 14, 17 | bitrd 177 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
19 | 18 | orbi1d 705 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((1 < 𝑁 ∨ 1 =
𝑁) ↔ ((2 < 𝑁 ∨ 2 = 𝑁) ∨ 1 = 𝑁))) |
20 | 2, 19 | syl 14 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → ((1 < 𝑁 ∨ 1 = 𝑁) ↔ ((2 < 𝑁 ∨ 2 = 𝑁) ∨ 1 = 𝑁))) |
21 | 8, 20 | mpbid 135 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → ((2 < 𝑁 ∨ 2 = 𝑁) ∨ 1 = 𝑁)) |
22 | 21 | orcomd 648 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 = 𝑁 ∨ (2 < 𝑁 ∨ 2 = 𝑁))) |
23 | | orcom 647 |
. . . . 5
⊢ ((2 <
𝑁 ∨ 2 = 𝑁) ↔ (2 = 𝑁 ∨ 2 < 𝑁)) |
24 | 23 | orbi2i 679 |
. . . 4
⊢ ((1 =
𝑁 ∨ (2 < 𝑁 ∨ 2 = 𝑁)) ↔ (1 = 𝑁 ∨ (2 = 𝑁 ∨ 2 < 𝑁))) |
25 | 22, 24 | sylib 127 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 = 𝑁 ∨ (2 = 𝑁 ∨ 2 < 𝑁))) |
26 | | 3orass 888 |
. . 3
⊢ ((1 =
𝑁 ∨ 2 = 𝑁 ∨ 2 < 𝑁) ↔ (1 = 𝑁 ∨ (2 = 𝑁 ∨ 2 < 𝑁))) |
27 | 25, 26 | sylibr 137 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 = 𝑁 ∨ 2 = 𝑁 ∨ 2 < 𝑁)) |
28 | | 3mix1 1073 |
. . . . 5
⊢ (𝑁 = 1 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
29 | 28 | eqcoms 2043 |
. . . 4
⊢ (1 =
𝑁 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
30 | 29 | a1i 9 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (1 = 𝑁 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
31 | | 3mix2 1074 |
. . . . 5
⊢ (𝑁 = 2 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
32 | 31 | eqcoms 2043 |
. . . 4
⊢ (2 =
𝑁 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
33 | 32 | a1i 9 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (2 = 𝑁 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
34 | | simp3 906 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 𝑁 ≤ 3) |
35 | 34 | biantrurd 289 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (3 ≤ 𝑁 ↔ (𝑁 ≤ 3 ∧ 3 ≤ 𝑁))) |
36 | | 2nn0 8198 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
37 | | nn0ltp1le 8306 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 <
𝑁 ↔ (2 + 1) ≤ 𝑁)) |
38 | 36, 37 | mpan 400 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (2 < 𝑁 ↔ (2
+ 1) ≤ 𝑁)) |
39 | | df-3 7974 |
. . . . . . . 8
⊢ 3 = (2 +
1) |
40 | 39 | breq1i 3771 |
. . . . . . 7
⊢ (3 ≤
𝑁 ↔ (2 + 1) ≤ 𝑁) |
41 | 38, 40 | syl6bbr 187 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (2 < 𝑁 ↔ 3
≤ 𝑁)) |
42 | 2, 41 | syl 14 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (2 < 𝑁 ↔ 3 ≤ 𝑁)) |
43 | 2 | nn0red 8236 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → 𝑁 ∈
ℝ) |
44 | | 3re 7989 |
. . . . . 6
⊢ 3 ∈
ℝ |
45 | | letri3 7099 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℝ) → (𝑁 = 3
↔ (𝑁 ≤ 3 ∧ 3
≤ 𝑁))) |
46 | 43, 44, 45 | sylancl 392 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 3 ↔ (𝑁 ≤ 3 ∧ 3 ≤ 𝑁))) |
47 | 35, 42, 46 | 3bitr4d 209 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (2 < 𝑁 ↔ 𝑁 = 3)) |
48 | | 3mix3 1075 |
. . . 4
⊢ (𝑁 = 3 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
49 | 47, 48 | syl6bi 152 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (2 < 𝑁 → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
50 | 30, 33, 49 | 3jaod 1199 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → ((1 = 𝑁 ∨ 2 = 𝑁 ∨ 2 < 𝑁) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))) |
51 | 27, 50 | mpd 13 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |