Step |
Hyp |
Ref |
Expression |
1 |
|
nn0z |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ ) |
2 |
|
oddp1d2 |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) |
3 |
1 2
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) |
4 |
|
peano2nn0 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
5 |
4
|
nn0red |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ ) |
6 |
|
2rp |
⊢ 2 ∈ ℝ+ |
7 |
6
|
a1i |
⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ+ ) |
8 |
|
nn0re |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ ) |
9 |
|
1red |
⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ ) |
10 |
|
nn0ge0 |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 ) |
11 |
|
0le1 |
⊢ 0 ≤ 1 |
12 |
11
|
a1i |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 1 ) |
13 |
8 9 10 12
|
addge0d |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( 𝑁 + 1 ) ) |
14 |
5 7 13
|
divge0d |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( ( 𝑁 + 1 ) / 2 ) ) |
15 |
14
|
anim1ci |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 1 ) / 2 ) ) ) |
16 |
|
elnn0z |
⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 1 ) / 2 ) ) ) |
17 |
15 16
|
sylibr |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) |
18 |
17
|
ex |
⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) |
19 |
|
nn0z |
⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) |
20 |
18 19
|
impbid1 |
⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) |
21 |
|
nn0ob |
⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) ) |
22 |
3 20 21
|
3bitrd |
⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) ) |