Description: 3 is an odd number. (Contributed by AV, 20-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | 3odd | ⊢ 3 ∈ Odd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2evenALTV | ⊢ 2 ∈ Even | |
2 | df-3 | ⊢ 3 = ( 2 + 1 ) | |
3 | evenp1odd | ⊢ ( 2 ∈ Even → ( 2 + 1 ) ∈ Odd ) | |
4 | 2 3 | eqeltrid | ⊢ ( 2 ∈ Even → 3 ∈ Odd ) |
5 | 1 4 | ax-mp | ⊢ 3 ∈ Odd |