Metamath Proof Explorer

Theorem epee

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

Ref Expression
Assertion epee ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to {A}+{B}\in \mathrm{Even}$

Proof

Step Hyp Ref Expression
1 evenp1odd ${⊢}{A}\in \mathrm{Even}\to {A}+1\in \mathrm{Odd}$
2 evenm1odd ${⊢}{B}\in \mathrm{Even}\to {B}-1\in \mathrm{Odd}$
3 opoeALTV ${⊢}\left({A}+1\in \mathrm{Odd}\wedge {B}-1\in \mathrm{Odd}\right)\to {A}+1+\left({B}-1\right)\in \mathrm{Even}$
4 1 2 3 syl2an ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to {A}+1+\left({B}-1\right)\in \mathrm{Even}$
5 evenz ${⊢}{A}\in \mathrm{Even}\to {A}\in ℤ$
6 5 zcnd ${⊢}{A}\in \mathrm{Even}\to {A}\in ℂ$
7 6 adantr ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to {A}\in ℂ$
8 1cnd ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to 1\in ℂ$
9 evenz ${⊢}{B}\in \mathrm{Even}\to {B}\in ℤ$
10 9 zcnd ${⊢}{B}\in \mathrm{Even}\to {B}\in ℂ$
11 10 adantl ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to {B}\in ℂ$
12 ppncan ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\wedge {B}\in ℂ\right)\to {A}+1+\left({B}-1\right)={A}+{B}$
13 12 eleq1d ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\wedge {B}\in ℂ\right)\to \left({A}+1+\left({B}-1\right)\in \mathrm{Even}↔{A}+{B}\in \mathrm{Even}\right)$
14 7 8 11 13 syl3anc ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to \left({A}+1+\left({B}-1\right)\in \mathrm{Even}↔{A}+{B}\in \mathrm{Even}\right)$
15 4 14 mpbid ${⊢}\left({A}\in \mathrm{Even}\wedge {B}\in \mathrm{Even}\right)\to {A}+{B}\in \mathrm{Even}$