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

Metamath Proof Explorer

Theorem nnoddm1d2

Description: A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion nnoddm1d2 ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2 oddp1d2 ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
3 1 2 syl ⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
4 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
5 4 nnred ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
8 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
9 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
10 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
11 0lt1 ⊢ 0 < 1
12 11 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
13 8 9 10 12 addgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
14 2pos ⊢ 0 < 2
15 14 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 2 )
16 5 7 13 15 divgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 𝑁 + 1 ) / 2 ) )
17 16 anim1ci ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
18 elnnz ⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
19 17 18 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )
20 19 ex ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
21 nnz ⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
22 20 21 impbid1 ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
23 3 22 bitrd ⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )