This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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