Description: An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020) (Proof shortened by OpenAI, 3-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elmod2 | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 2 ) ∈ { 0 , 1 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn | ⊢ 2 ∈ ℕ | |
2 | zmodfzo | ⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑁 mod 2 ) ∈ ( 0 ..^ 2 ) ) | |
3 | 2 | ancoms | ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 mod 2 ) ∈ ( 0 ..^ 2 ) ) |
4 | 1 3 | mpan | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 2 ) ∈ ( 0 ..^ 2 ) ) |
5 | fzo0to2pr | ⊢ ( 0 ..^ 2 ) = { 0 , 1 } | |
6 | 4 5 | eleqtrdi | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 2 ) ∈ { 0 , 1 } ) |