Metamath Proof Explorer


Theorem opoeALTV

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

Ref Expression
Assertion opoeALTV ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → ( 𝐴 + 𝐵 ) ∈ Even )

Proof

Step Hyp Ref Expression
1 oddz ( 𝐴 ∈ Odd → 𝐴 ∈ ℤ )
2 oddz ( 𝐵 ∈ Odd → 𝐵 ∈ ℤ )
3 zaddcl ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
4 1 2 3 syl2an ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
5 eqeq1 ( 𝑎 = 𝐴 → ( 𝑎 = ( ( 2 · 𝑖 ) + 1 ) ↔ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) )
6 5 rexbidv ( 𝑎 = 𝐴 → ( ∃ 𝑖 ∈ ℤ 𝑎 = ( ( 2 · 𝑖 ) + 1 ) ↔ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) )
7 dfodd6 Odd = { 𝑎 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑎 = ( ( 2 · 𝑖 ) + 1 ) }
8 6 7 elrab2 ( 𝐴 ∈ Odd ↔ ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) )
9 eqeq1 ( 𝑏 = 𝐵 → ( 𝑏 = ( ( 2 · 𝑗 ) + 1 ) ↔ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) )
10 9 rexbidv ( 𝑏 = 𝐵 → ( ∃ 𝑗 ∈ ℤ 𝑏 = ( ( 2 · 𝑗 ) + 1 ) ↔ ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) )
11 dfodd6 Odd = { 𝑏 ∈ ℤ ∣ ∃ 𝑗 ∈ ℤ 𝑏 = ( ( 2 · 𝑗 ) + 1 ) }
12 10 11 elrab2 ( 𝐵 ∈ Odd ↔ ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) )
13 zaddcl ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
14 13 ex ( 𝑖 ∈ ℤ → ( 𝑗 ∈ ℤ → ( 𝑖 + 𝑗 ) ∈ ℤ ) )
15 14 ad3antlr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝑗 ∈ ℤ → ( 𝑖 + 𝑗 ) ∈ ℤ ) )
16 15 imp ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
17 16 adantr ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
18 17 peano2zd ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( ( 𝑖 + 𝑗 ) + 1 ) ∈ ℤ )
19 oveq2 ( 𝑛 = ( ( 𝑖 + 𝑗 ) + 1 ) → ( 2 · 𝑛 ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
20 19 eqeq2d ( 𝑛 = ( ( 𝑖 + 𝑗 ) + 1 ) → ( ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ↔ ( 𝐴 + 𝐵 ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) ) )
21 20 adantl ( ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) ∧ 𝑛 = ( ( 𝑖 + 𝑗 ) + 1 ) ) → ( ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ↔ ( 𝐴 + 𝐵 ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) ) )
22 oveq12 ( ( 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) )
23 22 ex ( 𝐴 = ( ( 2 · 𝑖 ) + 1 ) → ( 𝐵 = ( ( 2 · 𝑗 ) + 1 ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) ) )
24 23 ad3antlr ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( 𝐵 = ( ( 2 · 𝑗 ) + 1 ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) ) )
25 24 imp ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) )
26 zcn ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
27 zcn ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
28 2cnd ( 𝑗 ∈ ℂ → 2 ∈ ℂ )
29 28 anim1i ( ( 𝑗 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 2 ∈ ℂ ∧ 𝑖 ∈ ℂ ) )
30 29 ancoms ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 ∈ ℂ ∧ 𝑖 ∈ ℂ ) )
31 mulcl ( ( 2 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 2 · 𝑖 ) ∈ ℂ )
32 30 31 syl ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · 𝑖 ) ∈ ℂ )
33 1cnd ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → 1 ∈ ℂ )
34 2cnd ( 𝑖 ∈ ℂ → 2 ∈ ℂ )
35 mulcl ( ( 2 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · 𝑗 ) ∈ ℂ )
36 34 35 sylan ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · 𝑗 ) ∈ ℂ )
37 32 33 36 33 add4d ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + ( 1 + 1 ) ) )
38 2cnd ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → 2 ∈ ℂ )
39 simpl ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → 𝑖 ∈ ℂ )
40 simpr ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → 𝑗 ∈ ℂ )
41 38 39 40 adddid ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · ( 𝑖 + 𝑗 ) ) = ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) )
42 41 oveq1d ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( 2 · ( 𝑖 + 𝑗 ) ) + ( 2 · 1 ) ) = ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + ( 2 · 1 ) ) )
43 addcl ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑖 + 𝑗 ) ∈ ℂ )
44 38 43 33 adddid ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + ( 2 · 1 ) ) )
45 1p1e2 ( 1 + 1 ) = 2
46 2t1e2 ( 2 · 1 ) = 2
47 45 46 eqtr4i ( 1 + 1 ) = ( 2 · 1 )
48 47 a1i ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 1 + 1 ) = ( 2 · 1 ) )
49 48 oveq2d ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + ( 2 · 1 ) ) )
50 42 44 49 3eqtr4rd ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + ( 1 + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
51 37 50 eqtrd ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
52 26 27 51 syl2an ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
53 52 ex ( 𝑖 ∈ ℤ → ( 𝑗 ∈ ℤ → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) ) )
54 53 ad3antlr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝑗 ∈ ℤ → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) ) )
55 54 imp ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
56 55 adantr ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( ( 2 · 𝑗 ) + 1 ) ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
57 25 56 eqtrd ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ( 𝐴 + 𝐵 ) = ( 2 · ( ( 𝑖 + 𝑗 ) + 1 ) ) )
58 18 21 57 rspcedvd ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) )
59 58 rexlimdva2 ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
60 59 expimpd ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
61 60 rexlimdva2 ( 𝐴 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) → ( ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) ) )
62 61 imp ( ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( ( 2 · 𝑗 ) + 1 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
63 12 62 syl5bi ( ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( 𝐵 ∈ Odd → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
64 8 63 sylbi ( 𝐴 ∈ Odd → ( 𝐵 ∈ Odd → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
65 64 imp ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) )
66 eqeq1 ( 𝑧 = ( 𝐴 + 𝐵 ) → ( 𝑧 = ( 2 · 𝑛 ) ↔ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
67 66 rexbidv ( 𝑧 = ( 𝐴 + 𝐵 ) → ( ∃ 𝑛 ∈ ℤ 𝑧 = ( 2 · 𝑛 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
68 dfeven4 Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑛 ∈ ℤ 𝑧 = ( 2 · 𝑛 ) }
69 67 68 elrab2 ( ( 𝐴 + 𝐵 ) ∈ Even ↔ ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( 2 · 𝑛 ) ) )
70 4 65 69 sylanbrc ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → ( 𝐴 + 𝐵 ) ∈ Even )