Metamath Proof Explorer


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 A¬2AB¬2B2A+B

Proof

Step Hyp Ref Expression
1 odd2np1 A¬2Aa2a+1=A
2 odd2np1 B¬2Bb2b+1=B
3 1 2 bi2anan9 AB¬2A¬2Ba2a+1=Ab2b+1=B
4 reeanv ab2a+1=A2b+1=Ba2a+1=Ab2b+1=B
5 2z 2
6 zaddcl aba+b
7 6 peano2zd aba+b+1
8 dvdsmul1 2a+b+122a+b+1
9 5 7 8 sylancr ab22a+b+1
10 zcn aa
11 zcn bb
12 addcl aba+b
13 2cn 2
14 ax-1cn 1
15 adddi 2a+b12a+b+1=2a+b+21
16 13 14 15 mp3an13 a+b2a+b+1=2a+b+21
17 12 16 syl ab2a+b+1=2a+b+21
18 adddi 2ab2a+b=2a+2b
19 13 18 mp3an1 ab2a+b=2a+2b
20 19 oveq1d ab2a+b+21=2a+2b+21
21 17 20 eqtrd ab2a+b+1=2a+2b+21
22 2t1e2 21=2
23 df-2 2=1+1
24 22 23 eqtri 21=1+1
25 24 oveq2i 2a+2b+21=2a+2b+1+1
26 21 25 eqtrdi ab2a+b+1=2a+2b+1+1
27 mulcl 2a2a
28 13 27 mpan a2a
29 mulcl 2b2b
30 13 29 mpan b2b
31 add4 2a2b112a+2b+1+1=2a+1+2b+1
32 14 14 31 mpanr12 2a2b2a+2b+1+1=2a+1+2b+1
33 28 30 32 syl2an ab2a+2b+1+1=2a+1+2b+1
34 26 33 eqtrd ab2a+b+1=2a+1+2b+1
35 10 11 34 syl2an ab2a+b+1=2a+1+2b+1
36 9 35 breqtrd ab22a+1+2b+1
37 oveq12 2a+1=A2b+1=B2a+1+2b+1=A+B
38 37 breq2d 2a+1=A2b+1=B22a+1+2b+12A+B
39 36 38 syl5ibcom ab2a+1=A2b+1=B2A+B
40 39 rexlimivv ab2a+1=A2b+1=B2A+B
41 4 40 sylbir a2a+1=Ab2b+1=B2A+B
42 3 41 syl6bi AB¬2A¬2B2A+B
43 42 imp AB¬2A¬2B2A+B
44 43 an4s A¬2AB¬2B2A+B