Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ ) |
2 |
|
2re |
⊢ 2 ∈ ℝ |
3 |
2
|
a1i |
⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ ) |
4 |
1 3
|
leloed |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 2 ↔ ( 𝑁 < 2 ∨ 𝑁 = 2 ) ) ) |
5 |
|
nn0z |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ ) |
6 |
|
2z |
⊢ 2 ∈ ℤ |
7 |
|
zltlem1 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝑁 < 2 ↔ 𝑁 ≤ ( 2 − 1 ) ) ) |
8 |
5 6 7
|
sylancl |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 ↔ 𝑁 ≤ ( 2 − 1 ) ) ) |
9 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
10 |
9
|
a1i |
⊢ ( 𝑁 ∈ ℕ0 → ( 2 − 1 ) = 1 ) |
11 |
10
|
breq2d |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ ( 2 − 1 ) ↔ 𝑁 ≤ 1 ) ) |
12 |
8 11
|
bitrd |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 ↔ 𝑁 ≤ 1 ) ) |
13 |
|
1red |
⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ ) |
14 |
1 13
|
leloed |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 1 ↔ ( 𝑁 < 1 ∨ 𝑁 = 1 ) ) ) |
15 |
|
nn0lt10b |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ 𝑁 = 0 ) ) |
16 |
|
3mix1 |
⊢ ( 𝑁 = 0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) |
17 |
15 16
|
syl6bi |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
18 |
17
|
com12 |
⊢ ( 𝑁 < 1 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
19 |
|
3mix2 |
⊢ ( 𝑁 = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) |
20 |
19
|
a1d |
⊢ ( 𝑁 = 1 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
21 |
18 20
|
jaoi |
⊢ ( ( 𝑁 < 1 ∨ 𝑁 = 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
22 |
21
|
com12 |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 < 1 ∨ 𝑁 = 1 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
23 |
14 22
|
sylbid |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
24 |
12 23
|
sylbid |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
25 |
24
|
com12 |
⊢ ( 𝑁 < 2 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
26 |
|
3mix3 |
⊢ ( 𝑁 = 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) |
27 |
26
|
a1d |
⊢ ( 𝑁 = 2 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
28 |
25 27
|
jaoi |
⊢ ( ( 𝑁 < 2 ∨ 𝑁 = 2 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
29 |
28
|
com12 |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 < 2 ∨ 𝑁 = 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
30 |
4 29
|
sylbid |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) |
31 |
30
|
imp |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) |