Description: An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | oddp1evenALTV | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( 𝑁 + 1 ) ∈ Even ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isodd | ⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) | |
2 | 1 | baib | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) |
3 | peano2z | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ ) | |
4 | 3 | biantrurd | ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) ) |
5 | 2 4 | bitrd | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) ) |
6 | iseven | ⊢ ( ( 𝑁 + 1 ) ∈ Even ↔ ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) ) | |
7 | 5 6 | bitr4di | ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( 𝑁 + 1 ) ∈ Even ) ) |