Theorem evensumeven

Description: If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020)

	Ref	Expression
Assertion	evensumeven	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )

Proof

Step	Hyp	Ref	Expression
1		epee	⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Even )
2	1	expcom	⊢ ( 𝐵 ∈ Even → ( 𝐴 ∈ Even → ( 𝐴 + 𝐵 ) ∈ Even ) )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even → ( 𝐴 + 𝐵 ) ∈ Even ) )
4		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
5		evenz	⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℤ )
6	5	zcnd	⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℂ )
7		pncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
8	4 6 7	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
9	8	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
10		simpr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → 𝐵 ∈ Even )
11	10	anim1i	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( 𝐵 ∈ Even ∧ ( 𝐴 + 𝐵 ) ∈ Even ) )
12	11	ancomd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) ∈ Even ∧ 𝐵 ∈ Even ) )
13		emee	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ Even ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) ∈ Even )
14	12 13	syl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) ∈ Even )
15	9 14	eqeltrrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → 𝐴 ∈ Even )
16	15	ex	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) ∈ Even → 𝐴 ∈ Even ) )
17	3 16	impbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )