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

Metamath Proof Explorer

Theorem oddge22np1

Description: An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion oddge22np1 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
3 2 adantl ⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
4 eluz2 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ ∧ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) )
5 2re ⊢ 2 ∈ ℝ
6 5 a1i ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℝ )
7 1red ⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℝ )
8 2nn0 ⊢ 2 ∈ ℕ0
9 8 a1i ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
10 id ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
11 9 10 nn0mulcld ⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 )
12 11 nn0red ⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℝ )
13 6 7 12 lesubaddd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) ↔ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) )
14 2m1e1 ⊢ ( 2 − 1 ) = 1
15 14 breq1i ⊢ ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) ↔ 1 ≤ ( 2 · 𝑛 ) )
16 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
17 2rp ⊢ 2 ∈ ℝ+
18 17 a1i ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℝ+ )
19 7 16 18 ledivmuld ⊢ ( 𝑛 ∈ ℕ0 → ( ( 1 / 2 ) ≤ 𝑛 ↔ 1 ≤ ( 2 · 𝑛 ) ) )
20 halfgt0 ⊢ 0 < ( 1 / 2 )
21 0red ⊢ ( 𝑛 ∈ ℕ0 → 0 ∈ ℝ )
22 halfre ⊢ ( 1 / 2 ) ∈ ℝ
23 22 a1i ⊢ ( 𝑛 ∈ ℕ0 → ( 1 / 2 ) ∈ ℝ )
24 ltletr ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑛 ) → 0 < 𝑛 ) )
25 21 23 16 24 syl3anc ⊢ ( 𝑛 ∈ ℕ0 → ( ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑛 ) → 0 < 𝑛 ) )
26 20 25 mpani ⊢ ( 𝑛 ∈ ℕ0 → ( ( 1 / 2 ) ≤ 𝑛 → 0 < 𝑛 ) )
27 19 26 sylbird ⊢ ( 𝑛 ∈ ℕ0 → ( 1 ≤ ( 2 · 𝑛 ) → 0 < 𝑛 ) )
28 15 27 biimtrid ⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) → 0 < 𝑛 ) )
29 13 28 sylbird ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ≤ ( ( 2 · 𝑛 ) + 1 ) → 0 < 𝑛 ) )
30 29 com12 ⊢ ( 2 ≤ ( ( 2 · 𝑛 ) + 1 ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
31 30 3ad2ant3 ⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ ∧ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
32 4 31 sylbi ⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
33 32 imp ⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 0 < 𝑛 )
34 elnnz ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℤ ∧ 0 < 𝑛 ) )
35 3 33 34 sylanbrc ⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ )
36 35 ex ⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ ) )
37 1 36 biimtrrdi ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ ) ) )
38 37 com13 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ ) ) )
39 38 impcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ ) )
40 39 pm4.71rd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
41 40 bicomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
42 41 rexbidva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
43 nnssnn0 ⊢ ℕ ⊆ ℕ0
44 rexss ⊢ ( ℕ ⊆ ℕ0 → ( ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
45 43 44 mp1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
46 eluzge2nn0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
47 oddnn02np1 ⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
48 46 47 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
49 42 45 48 3bitr4rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )