Theorem opoe

Description: The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	opoe	⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		odd2np1	⊢ ( 𝐴 ∈ ℤ → ( ¬ 2 ∥ 𝐴 ↔ ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ) )
2		odd2np1	⊢ ( 𝐵 ∈ ℤ → ( ¬ 2 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) )
3	1 2	bi2anan9	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) ) )
4		reeanv	⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) )
5		2z	⊢ 2 ∈ ℤ
6		zaddcl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
7	6	peano2zd	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( 𝑎 + 𝑏 ) + 1 ) ∈ ℤ )
8		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ ( ( 𝑎 + 𝑏 ) + 1 ) ∈ ℤ ) → 2 ∥ ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) )
9	5 7 8	sylancr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) )
10		zcn	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
11		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
12		addcl	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 + 𝑏 ) ∈ ℂ )
13		2cn	⊢ 2 ∈ ℂ
14		ax-1cn	⊢ 1 ∈ ℂ
15		adddi	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑎 + 𝑏 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
16	13 14 15	mp3an13	⊢ ( ( 𝑎 + 𝑏 ) ∈ ℂ → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
17	12 16	syl	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
18		adddi	⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 + 𝑏 ) ) = ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) )
19	13 18	mp3an1	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 + 𝑏 ) ) = ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) )
20	19	oveq1d	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 2 · 1 ) ) )
21	17 20	eqtrd	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 2 · 1 ) ) )
22		2t1e2	⊢ ( 2 · 1 ) = 2
23		df-2	⊢ 2 = ( 1 + 1 )
24	22 23	eqtri	⊢ ( 2 · 1 ) = ( 1 + 1 )
25	24	oveq2i	⊢ ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 2 · 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) )
26	21 25	syl6eq	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) )
27		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 2 · 𝑎 ) ∈ ℂ )
28	13 27	mpan	⊢ ( 𝑎 ∈ ℂ → ( 2 · 𝑎 ) ∈ ℂ )
29		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · 𝑏 ) ∈ ℂ )
30	13 29	mpan	⊢ ( 𝑏 ∈ ℂ → ( 2 · 𝑏 ) ∈ ℂ )
31		add4	⊢ ( ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) ∧ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
32	14 14 31	mpanr12	⊢ ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
33	28 30 32	syl2an	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
34	26 33	eqtrd	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
35	10 11 34	syl2an	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
36	9 35	breqtrd	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
37		oveq12	⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) = ( 𝐴 + 𝐵 ) )
38	37	breq2d	⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) ↔ 2 ∥ ( 𝐴 + 𝐵 ) ) )
39	36 38	syl5ibcom	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) ) )
40	39	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) )
41	4 40	sylbir	⊢ ( ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) )
42	3 41	syl6bi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) ) )
43	42	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )
44	43	an4s	⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )