This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )