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 e. Odd

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
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 ) e. ZZ
7 isodd 
 |-  ( 1 e. Odd <-> ( 1 e. ZZ /\ ( ( 1 + 1 ) / 2 ) e. ZZ ) )
8 1 6 7 mpbir2an 
 |-  1 e. Odd