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

Metamath Proof Explorer

Theorem 1oddALTV

Description: 1 is an odd number. (Contributed by AV, 3-Feb-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion 1oddALTV 1 ∈ Odd

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 1p1e2 ⊢ ( 1 + 1 ) = 2
3 2 oveq1i ⊢ ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
4 2div2e1 ⊢ ( 2 / 2 ) = 1
5 3 4 eqtri ⊢ ( ( 1 + 1 ) / 2 ) = 1
6 5 1 eqeltri ⊢ ( ( 1 + 1 ) / 2 ) ∈ ℤ
7 isodd ⊢ ( 1 ∈ Odd ↔ ( 1 ∈ ℤ ∧ ( ( 1 + 1 ) / 2 ) ∈ ℤ ) )
8 1 6 7 mpbir2an ⊢ 1 ∈ Odd