Theorem oddm1evenALTV

Description: An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

	Ref	Expression
Assertion	oddm1evenALTV	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( 𝑁 − 1 ) ∈ Even ) )

Proof

Step	Hyp	Ref	Expression
1		isodd2	⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
2	1	baib	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
3		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 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 ) )