Metamath Proof Explorer

Theorem 1odd

Description: 1 is an odd integer. (Contributed by AV, 3-Feb-2020)

Ref Expression
Hypothesis oddinmgm.e ⊢ O = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
Assertion 1odd ⊢ 1 ∈ O

Proof

Step Hyp Ref Expression
1 oddinmgm.e ⊢ O = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
2 1z ⊢ 1 ∈ ℤ
3 0z ⊢ 0 ∈ ℤ
4 id ⊢ 0 ∈ ℤ → 0 ∈ ℤ
5 oveq2 ⊢ x = 0 → 2 ⁢ x = 2 ⋅ 0
6 2t0e0 ⊢ 2 ⋅ 0 = 0
7 5 6 eqtrdi ⊢ x = 0 → 2 ⁢ x = 0
8 7 oveq1d ⊢ x = 0 → 2 ⁢ x + 1 = 0 + 1
9 8 eqeq2d ⊢ x = 0 → 1 = 2 ⁢ x + 1 ↔ 1 = 0 + 1
10 9 adantl ⊢ 0 ∈ ℤ ∧ x = 0 → 1 = 2 ⁢ x + 1 ↔ 1 = 0 + 1
11 1e0p1 ⊢ 1 = 0 + 1
12 11 a1i ⊢ 0 ∈ ℤ → 1 = 0 + 1
13 4 10 12 rspcedvd ⊢ 0 ∈ ℤ → ∃ x ∈ ℤ 1 = 2 ⁢ x + 1
14 3 13 ax-mp ⊢ ∃ x ∈ ℤ 1 = 2 ⁢ x + 1
15 eqeq1 ⊢ z = 1 → z = 2 ⁢ x + 1 ↔ 1 = 2 ⁢ x + 1
16 15 rexbidv ⊢ z = 1 → ∃ x ∈ ℤ z = 2 ⁢ x + 1 ↔ ∃ x ∈ ℤ 1 = 2 ⁢ x + 1
17 16 1 elrab2 ⊢ 1 ∈ O ↔ 1 ∈ ℤ ∧ ∃ x ∈ ℤ 1 = 2 ⁢ x + 1
18 2 14 17 mpbir2an ⊢ 1 ∈ O