Metamath Proof Explorer

Theorem opeo

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

Ref Expression
Assertion opeo ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A+B

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢A∈ℤ→¬2∥A↔∃a∈ℤ2⁢a+1=A
2 2z ⊢2∈ℤ
3 divides ⊢2∈ℤ∧B∈ℤ→2∥B↔∃b∈ℤb⋅2=B
4 2 3 mpan ⊢B∈ℤ→2∥B↔∃b∈ℤb⋅2=B
5 1 4 bi2anan9 ⊢A∈ℤ∧B∈ℤ→¬2∥A∧2∥B↔∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B
6 reeanv ⊢∃a∈ℤ∃b∈ℤ2⁢a+1=A∧b⋅2=B↔∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B
7 zaddcl ⊢a∈ℤ∧b∈ℤ→a+b∈ℤ
8 zcn ⊢a∈ℤ→a∈ℂ
9 zcn ⊢b∈ℤ→b∈ℂ
10 2cn ⊢2∈ℂ
11 adddi ⊢2∈ℂ∧a∈ℂ∧b∈ℂ→2⁢a+b=2⁢a+2⁢b
12 10 11 mp3an1 ⊢a∈ℂ∧b∈ℂ→2⁢a+b=2⁢a+2⁢b
13 12 oveq1d ⊢a∈ℂ∧b∈ℂ→2⁢a+b+1=2⁢a+2⁢b+1
14 mulcl ⊢2∈ℂ∧a∈ℂ→2⁢a∈ℂ
15 10 14 mpan ⊢a∈ℂ→2⁢a∈ℂ
16 mulcl ⊢2∈ℂ∧b∈ℂ→2⁢b∈ℂ
17 10 16 mpan ⊢b∈ℂ→2⁢b∈ℂ
18 ax-1cn ⊢1∈ℂ
19 add32 ⊢2⁢a∈ℂ∧2⁢b∈ℂ∧1∈ℂ→2⁢a+2⁢b+1=2⁢a+1+2⁢b
20 18 19 mp3an3 ⊢2⁢a∈ℂ∧2⁢b∈ℂ→2⁢a+2⁢b+1=2⁢a+1+2⁢b
21 15 17 20 syl2an ⊢a∈ℂ∧b∈ℂ→2⁢a+2⁢b+1=2⁢a+1+2⁢b
22 mulcom ⊢2∈ℂ∧b∈ℂ→2⁢b=b⋅2
23 10 22 mpan ⊢b∈ℂ→2⁢b=b⋅2
24 23 adantl ⊢a∈ℂ∧b∈ℂ→2⁢b=b⋅2
25 24 oveq2d ⊢a∈ℂ∧b∈ℂ→2⁢a+1+2⁢b=2⁢a+1+b⋅2
26 13 21 25 3eqtrd ⊢a∈ℂ∧b∈ℂ→2⁢a+b+1=2⁢a+1+b⋅2
27 8 9 26 syl2an ⊢a∈ℤ∧b∈ℤ→2⁢a+b+1=2⁢a+1+b⋅2
28 oveq2 ⊢c=a+b→2⁢c=2⁢a+b
29 28 oveq1d ⊢c=a+b→2⁢c+1=2⁢a+b+1
30 29 eqeq1d ⊢c=a+b→2⁢c+1=2⁢a+1+b⋅2↔2⁢a+b+1=2⁢a+1+b⋅2
31 30 rspcev ⊢a+b∈ℤ∧2⁢a+b+1=2⁢a+1+b⋅2→∃c∈ℤ2⁢c+1=2⁢a+1+b⋅2
32 7 27 31 syl2anc ⊢a∈ℤ∧b∈ℤ→∃c∈ℤ2⁢c+1=2⁢a+1+b⋅2
33 oveq12 ⊢2⁢a+1=A∧b⋅2=B→2⁢a+1+b⋅2=A+B
34 33 eqeq2d ⊢2⁢a+1=A∧b⋅2=B→2⁢c+1=2⁢a+1+b⋅2↔2⁢c+1=A+B
35 34 rexbidv ⊢2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=2⁢a+1+b⋅2↔∃c∈ℤ2⁢c+1=A+B
36 32 35 syl5ibcom ⊢a∈ℤ∧b∈ℤ→2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=A+B
37 36 rexlimivv ⊢∃a∈ℤ∃b∈ℤ2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=A+B
38 6 37 sylbir ⊢∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B→∃c∈ℤ2⁢c+1=A+B
39 5 38 syl6bi ⊢A∈ℤ∧B∈ℤ→¬2∥A∧2∥B→∃c∈ℤ2⁢c+1=A+B
40 39 imp ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧2∥B→∃c∈ℤ2⁢c+1=A+B
41 40 an4s ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→∃c∈ℤ2⁢c+1=A+B
42 zaddcl ⊢A∈ℤ∧B∈ℤ→A+B∈ℤ
43 42 ad2ant2r ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→A+B∈ℤ
44 odd2np1 ⊢A+B∈ℤ→¬2∥A+B↔∃c∈ℤ2⁢c+1=A+B
45 43 44 syl ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A+B↔∃c∈ℤ2⁢c+1=A+B
46 41 45 mpbird ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A+B