Theorem oddm1even

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

	Ref	Expression
Assertion	oddm1even	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑁 ∈ ℤ )
2	1	zcnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑁 ∈ ℂ )
3		1cnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℂ )
4		2cnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℂ )
5		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
6	5	zcnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
7	4 6	mulcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℂ )
8	2 3 7	subadd2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
9		eqcom	⊢ ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( 2 · 𝑛 ) = ( 𝑁 − 1 ) )
10	4 6	mulcomd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) = ( 𝑛 · 2 ) )
11	10	eqeq1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 2 · 𝑛 ) = ( 𝑁 − 1 ) ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
12	9 11	bitrid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
13	8 12	bitr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
14	13	rexbidva	⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
15		odd2np1	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
16		2z	⊢ 2 ∈ ℤ
17		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
18		divides	⊢ ( ( 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
19	16 17 18	sylancr	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 𝑁 − 1 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) )
20	14 15 19	3bitr4d	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )