Metamath Proof Explorer


Theorem opeoALTV

Description: The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by AV, 20-Jun-2020)

Ref Expression
Assertion opeoALTV A Odd B Even A + B Odd

Proof

Step Hyp Ref Expression
1 oddz A Odd A
2 evenz B Even B
3 zaddcl A B A + B
4 1 2 3 syl2an A Odd B Even A + B
5 eqeq1 a = A a = 2 i + 1 A = 2 i + 1
6 5 rexbidv a = A i a = 2 i + 1 i A = 2 i + 1
7 dfodd6 Odd = a | i a = 2 i + 1
8 6 7 elrab2 A Odd A i A = 2 i + 1
9 eqeq1 b = B b = 2 j B = 2 j
10 9 rexbidv b = B j b = 2 j j B = 2 j
11 dfeven4 Even = b | j b = 2 j
12 10 11 elrab2 B Even B j B = 2 j
13 zaddcl i j i + j
14 13 ex i j i + j
15 14 ad3antlr A i A = 2 i + 1 B j i + j
16 15 imp A i A = 2 i + 1 B j i + j
17 16 adantr A i A = 2 i + 1 B j B = 2 j i + j
18 oveq2 n = i + j 2 n = 2 i + j
19 18 oveq1d n = i + j 2 n + 1 = 2 i + j + 1
20 19 eqeq2d n = i + j A + B = 2 n + 1 A + B = 2 i + j + 1
21 20 adantl A i A = 2 i + 1 B j B = 2 j n = i + j A + B = 2 n + 1 A + B = 2 i + j + 1
22 oveq12 A = 2 i + 1 B = 2 j A + B = 2 i + 1 + 2 j
23 22 ex A = 2 i + 1 B = 2 j A + B = 2 i + 1 + 2 j
24 23 ad3antlr A i A = 2 i + 1 B j B = 2 j A + B = 2 i + 1 + 2 j
25 24 imp A i A = 2 i + 1 B j B = 2 j A + B = 2 i + 1 + 2 j
26 2cnd j i 2
27 zcn i i
28 27 adantl j i i
29 26 28 mulcld j i 2 i
30 29 ancoms i j 2 i
31 1cnd i j 1
32 2cnd i 2
33 zcn j j
34 mulcl 2 j 2 j
35 32 33 34 syl2an i j 2 j
36 30 31 35 add32d i j 2 i + 1 + 2 j = 2 i + 2 j + 1
37 2cnd i j 2
38 27 adantr i j i
39 33 adantl i j j
40 37 38 39 adddid i j 2 i + j = 2 i + 2 j
41 40 eqcomd i j 2 i + 2 j = 2 i + j
42 41 oveq1d i j 2 i + 2 j + 1 = 2 i + j + 1
43 36 42 eqtrd i j 2 i + 1 + 2 j = 2 i + j + 1
44 43 ex i j 2 i + 1 + 2 j = 2 i + j + 1
45 44 ad3antlr A i A = 2 i + 1 B j 2 i + 1 + 2 j = 2 i + j + 1
46 45 imp A i A = 2 i + 1 B j 2 i + 1 + 2 j = 2 i + j + 1
47 46 adantr A i A = 2 i + 1 B j B = 2 j 2 i + 1 + 2 j = 2 i + j + 1
48 25 47 eqtrd A i A = 2 i + 1 B j B = 2 j A + B = 2 i + j + 1
49 17 21 48 rspcedvd A i A = 2 i + 1 B j B = 2 j n A + B = 2 n + 1
50 49 rexlimdva2 A i A = 2 i + 1 B j B = 2 j n A + B = 2 n + 1
51 50 expimpd A i A = 2 i + 1 B j B = 2 j n A + B = 2 n + 1
52 51 r19.29an A i A = 2 i + 1 B j B = 2 j n A + B = 2 n + 1
53 12 52 syl5bi A i A = 2 i + 1 B Even n A + B = 2 n + 1
54 8 53 sylbi A Odd B Even n A + B = 2 n + 1
55 54 imp A Odd B Even n A + B = 2 n + 1
56 eqeq1 z = A + B z = 2 n + 1 A + B = 2 n + 1
57 56 rexbidv z = A + B n z = 2 n + 1 n A + B = 2 n + 1
58 dfodd6 Odd = z | n z = 2 n + 1
59 57 58 elrab2 A + B Odd A + B n A + B = 2 n + 1
60 4 55 59 sylanbrc A Odd B Even A + B Odd