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 biimtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 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 )