Metamath Proof Explorer


Theorem nn0oddm1d2

Description: A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion nn0oddm1d2 ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )

Proof

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 ) )