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

Metamath Proof Explorer

Theorem epee

Description: The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020)

Ref Expression
Assertion epee ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Even )

Proof

Step Hyp Ref Expression
1 evenp1odd ⊢ ( 𝐴 ∈ Even → ( 𝐴 + 1 ) ∈ Odd )
2 evenm1odd ⊢ ( 𝐵 ∈ Even → ( 𝐵 − 1 ) ∈ Odd )
3 opoeALTV ⊢ ( ( ( 𝐴 + 1 ) ∈ Odd ∧ ( 𝐵 − 1 ) ∈ Odd ) → ( ( 𝐴 + 1 ) + ( 𝐵 − 1 ) ) ∈ Even )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 1 ) + ( 𝐵 − 1 ) ) ∈ Even )
5 evenz ⊢ ( 𝐴 ∈ Even → 𝐴 ∈ ℤ )
6 5 zcnd ⊢ ( 𝐴 ∈ Even → 𝐴 ∈ ℂ )
7 6 adantr ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → 𝐴 ∈ ℂ )
8 1cnd ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → 1 ∈ ℂ )
9 evenz ⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℤ )
10 9 zcnd ⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℂ )
11 10 adantl ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → 𝐵 ∈ ℂ )
12 ppncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 1 ) + ( 𝐵 − 1 ) ) = ( 𝐴 + 𝐵 ) )
13 12 eleq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 1 ) + ( 𝐵 − 1 ) ) ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )
14 7 8 11 13 syl3anc ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( ( ( 𝐴 + 1 ) + ( 𝐵 − 1 ) ) ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )
15 4 14 mpbid ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Even )