Theorem oddp1even

Description: An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	oddp1even	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oddm1even	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
2		2z	⊢ 2 ∈ ℤ
3		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
4		dvdsadd	⊢ ( ( 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ) )
5	2 3 4	sylancr	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 𝑁 − 1 ) ↔ 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ) )
6		2cnd	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
7		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8		1cnd	⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ )
9	6 7 8	addsub12d	⊢ ( 𝑁 ∈ ℤ → ( 2 + ( 𝑁 − 1 ) ) = ( 𝑁 + ( 2 − 1 ) ) )
10		2m1e1	⊢ ( 2 − 1 ) = 1
11	10	oveq2i	⊢ ( 𝑁 + ( 2 − 1 ) ) = ( 𝑁 + 1 )
12	9 11	eqtrdi	⊢ ( 𝑁 ∈ ℤ → ( 2 + ( 𝑁 − 1 ) ) = ( 𝑁 + 1 ) )
13	12	breq2d	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ↔ 2 ∥ ( 𝑁 + 1 ) ) )
14	1 5 13	3bitrd	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )