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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | odd2np1 | |
|
2 | odd2np1 | |
|
3 | 1 2 | bi2anan9 | |
4 | reeanv | |
|
5 | 2z | |
|
6 | zaddcl | |
|
7 | 6 | peano2zd | |
8 | dvdsmul1 | |
|
9 | 5 7 8 | sylancr | |
10 | zcn | |
|
11 | zcn | |
|
12 | addcl | |
|
13 | 2cn | |
|
14 | ax-1cn | |
|
15 | adddi | |
|
16 | 13 14 15 | mp3an13 | |
17 | 12 16 | syl | |
18 | adddi | |
|
19 | 13 18 | mp3an1 | |
20 | 19 | oveq1d | |
21 | 17 20 | eqtrd | |
22 | 2t1e2 | |
|
23 | df-2 | |
|
24 | 22 23 | eqtri | |
25 | 24 | oveq2i | |
26 | 21 25 | eqtrdi | |
27 | mulcl | |
|
28 | 13 27 | mpan | |
29 | mulcl | |
|
30 | 13 29 | mpan | |
31 | add4 | |
|
32 | 14 14 31 | mpanr12 | |
33 | 28 30 32 | syl2an | |
34 | 26 33 | eqtrd | |
35 | 10 11 34 | syl2an | |
36 | 9 35 | breqtrd | |
37 | oveq12 | |
|
38 | 37 | breq2d | |
39 | 36 38 | syl5ibcom | |
40 | 39 | rexlimivv | |
41 | 4 40 | sylbir | |
42 | 3 41 | syl6bi | |
43 | 42 | imp | |
44 | 43 | an4s | |