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 )