Metamath Proof Explorer


Theorem oddp1evenALTV

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 ) )

Proof

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 ) )