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