Theorem evenp1odd

Description: The successor of an even number is odd. (Contributed by AV, 16-Jun-2020)

	Ref	Expression
Assertion	evenp1odd	⊢ ( 𝑍 ∈ Even → ( 𝑍 + 1 ) ∈ Odd )

Proof

Step	Hyp	Ref	Expression
1		evenz	⊢ ( 𝑍 ∈ Even → 𝑍 ∈ ℤ )
2	1	peano2zd	⊢ ( 𝑍 ∈ Even → ( 𝑍 + 1 ) ∈ ℤ )
3		iseven	⊢ ( 𝑍 ∈ Even ↔ ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) )
4		zcn	⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℂ )
5		pncan1	⊢ ( 𝑍 ∈ ℂ → ( ( 𝑍 + 1 ) − 1 ) = 𝑍 )
6	4 5	syl	⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 + 1 ) − 1 ) = 𝑍 )
7	6	eqcomd	⊢ ( 𝑍 ∈ ℤ → 𝑍 = ( ( 𝑍 + 1 ) − 1 ) )
8	7	oveq1d	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 / 2 ) = ( ( ( 𝑍 + 1 ) − 1 ) / 2 ) )
9	8	eleq1d	⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 / 2 ) ∈ ℤ ↔ ( ( ( 𝑍 + 1 ) − 1 ) / 2 ) ∈ ℤ ) )
10	9	biimpa	⊢ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) → ( ( ( 𝑍 + 1 ) − 1 ) / 2 ) ∈ ℤ )
11	3 10	sylbi	⊢ ( 𝑍 ∈ Even → ( ( ( 𝑍 + 1 ) − 1 ) / 2 ) ∈ ℤ )
12		isodd2	⊢ ( ( 𝑍 + 1 ) ∈ Odd ↔ ( ( 𝑍 + 1 ) ∈ ℤ ∧ ( ( ( 𝑍 + 1 ) − 1 ) / 2 ) ∈ ℤ ) )
13	2 11 12	sylanbrc	⊢ ( 𝑍 ∈ Even → ( 𝑍 + 1 ) ∈ Odd )