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 ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge 2\parallel {B}\right)\right)\to ¬2\parallel \left({A}+{B}\right)$

Proof

Step Hyp Ref Expression
1 odd2np1 ${⊢}{A}\in ℤ\to \left(¬2\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\right)$
2 2z ${⊢}2\in ℤ$
3 divides ${⊢}\left(2\in ℤ\wedge {B}\in ℤ\right)\to \left(2\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\cdot 2={B}\right)$
4 2 3 mpan ${⊢}{B}\in ℤ\to \left(2\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\cdot 2={B}\right)$
5 1 4 bi2anan9 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left(¬2\parallel {A}\wedge 2\parallel {B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\cdot 2={B}\right)\right)$
6 reeanv ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\cdot 2={B}\right)$
7 zaddcl ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}+{b}\in ℤ$
8 zcn ${⊢}{a}\in ℤ\to {a}\in ℂ$
9 zcn ${⊢}{b}\in ℤ\to {b}\in ℂ$
10 2cn ${⊢}2\in ℂ$
11 adddi ${⊢}\left(2\in ℂ\wedge {a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}+{b}\right)=2{a}+2{b}$
12 10 11 mp3an1 ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}+{b}\right)=2{a}+2{b}$
13 12 oveq1d ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}+{b}\right)+1=2{a}+2{b}+1$
14 mulcl ${⊢}\left(2\in ℂ\wedge {a}\in ℂ\right)\to 2{a}\in ℂ$
15 10 14 mpan ${⊢}{a}\in ℂ\to 2{a}\in ℂ$
16 mulcl ${⊢}\left(2\in ℂ\wedge {b}\in ℂ\right)\to 2{b}\in ℂ$
17 10 16 mpan ${⊢}{b}\in ℂ\to 2{b}\in ℂ$
18 ax-1cn ${⊢}1\in ℂ$
19 add32 ${⊢}\left(2{a}\in ℂ\wedge 2{b}\in ℂ\wedge 1\in ℂ\right)\to 2{a}+2{b}+1=2{a}+1+2{b}$
20 18 19 mp3an3 ${⊢}\left(2{a}\in ℂ\wedge 2{b}\in ℂ\right)\to 2{a}+2{b}+1=2{a}+1+2{b}$
21 15 17 20 syl2an ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2{a}+2{b}+1=2{a}+1+2{b}$
22 mulcom ${⊢}\left(2\in ℂ\wedge {b}\in ℂ\right)\to 2{b}={b}\cdot 2$
23 10 22 mpan ${⊢}{b}\in ℂ\to 2{b}={b}\cdot 2$
24 23 adantl ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2{b}={b}\cdot 2$
25 24 oveq2d ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2{a}+1+2{b}=2{a}+1+{b}\cdot 2$
26 13 21 25 3eqtrd ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}+{b}\right)+1=2{a}+1+{b}\cdot 2$
27 8 9 26 syl2an ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to 2\left({a}+{b}\right)+1=2{a}+1+{b}\cdot 2$
28 oveq2 ${⊢}{c}={a}+{b}\to 2{c}=2\left({a}+{b}\right)$
29 28 oveq1d ${⊢}{c}={a}+{b}\to 2{c}+1=2\left({a}+{b}\right)+1$
30 29 eqeq1d ${⊢}{c}={a}+{b}\to \left(2{c}+1=2{a}+1+{b}\cdot 2↔2\left({a}+{b}\right)+1=2{a}+1+{b}\cdot 2\right)$
31 30 rspcev ${⊢}\left({a}+{b}\in ℤ\wedge 2\left({a}+{b}\right)+1=2{a}+1+{b}\cdot 2\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1=2{a}+1+{b}\cdot 2$
32 7 27 31 syl2anc ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1=2{a}+1+{b}\cdot 2$
33 oveq12 ${⊢}\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)\to 2{a}+1+{b}\cdot 2={A}+{B}$
34 33 eqeq2d ${⊢}\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)\to \left(2{c}+1=2{a}+1+{b}\cdot 2↔2{c}+1={A}+{B}\right)$
35 34 rexbidv ${⊢}\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)\to \left(\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1=2{a}+1+{b}\cdot 2↔\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}\right)$
36 32 35 syl5ibcom ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left(\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}\right)$
37 36 rexlimivv ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left(2{a}+1={A}\wedge {b}\cdot 2={B}\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}$
38 6 37 sylbir ${⊢}\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\cdot 2={B}\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}$
39 5 38 syl6bi ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left(¬2\parallel {A}\wedge 2\parallel {B}\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}\right)$
40 39 imp ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left(¬2\parallel {A}\wedge 2\parallel {B}\right)\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}$
41 40 an4s ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge 2\parallel {B}\right)\right)\to \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}$
42 zaddcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}+{B}\in ℤ$
43 42 ad2ant2r ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge 2\parallel {B}\right)\right)\to {A}+{B}\in ℤ$
44 odd2np1 ${⊢}{A}+{B}\in ℤ\to \left(¬2\parallel \left({A}+{B}\right)↔\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}\right)$
45 43 44 syl ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge 2\parallel {B}\right)\right)\to \left(¬2\parallel \left({A}+{B}\right)↔\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}2{c}+1={A}+{B}\right)$
46 41 45 mpbird ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge 2\parallel {B}\right)\right)\to ¬2\parallel \left({A}+{B}\right)$