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