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 ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Odd )

Proof

Step Hyp Ref Expression
1 oddz ⊢ ( 𝐴 ∈ Odd → 𝐴 ∈ ℤ )
2 evenz ⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℤ )
3 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
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 · 𝑗 ) ↔ 𝐵 = ( 2 · 𝑗 ) ) )
10 9 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑗 ∈ ℤ 𝑏 = ( 2 · 𝑗 ) ↔ ∃ 𝑗 ∈ ℤ 𝐵 = ( 2 · 𝑗 ) ) )
11 dfeven4 ⊢ Even = { 𝑏 ∈ ℤ ∣ ∃ 𝑗 ∈ ℤ 𝑏 = ( 2 · 𝑗 ) }
12 10 11 elrab2 ⊢ ( 𝐵 ∈ Even ↔ ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( 2 · 𝑗 ) ) )
13 zaddcl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
14 13 ex ⊢ ( 𝑖 ∈ ℤ → ( 𝑗 ∈ ℤ → ( 𝑖 + 𝑗 ) ∈ ℤ ) )
15 14 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝑗 ∈ ℤ → ( 𝑖 + 𝑗 ) ∈ ℤ ) )
16 15 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
17 16 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
18 oveq2 ⊢ ( 𝑛 = ( 𝑖 + 𝑗 ) → ( 2 · 𝑛 ) = ( 2 · ( 𝑖 + 𝑗 ) ) )
19 18 oveq1d ⊢ ( 𝑛 = ( 𝑖 + 𝑗 ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
20 19 eqeq2d ⊢ ( 𝑛 = ( 𝑖 + 𝑗 ) → ( ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ↔ ( 𝐴 + 𝐵 ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) ) )
21 20 adantl ⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) ∧ 𝑛 = ( 𝑖 + 𝑗 ) ) → ( ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ↔ ( 𝐴 + 𝐵 ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) ) )
22 oveq12 ⊢ ( ( 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) )
23 22 ex ⊢ ( 𝐴 = ( ( 2 · 𝑖 ) + 1 ) → ( 𝐵 = ( 2 · 𝑗 ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) ) )
24 23 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( 𝐵 = ( 2 · 𝑗 ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) ) )
25 24 imp ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ( 𝐴 + 𝐵 ) = ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) )
26 2cnd ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
27 zcn ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
28 27 adantl ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
29 26 28 mulcld ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 2 · 𝑖 ) ∈ ℂ )
30 29 ancoms ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 2 · 𝑖 ) ∈ ℂ )
31 1cnd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 1 ∈ ℂ )
32 2cnd ⊢ ( 𝑖 ∈ ℤ → 2 ∈ ℂ )
33 zcn ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
34 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 2 · 𝑗 ) ∈ ℂ )
35 32 33 34 syl2an ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 2 · 𝑗 ) ∈ ℂ )
36 30 31 35 add32d ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + 1 ) )
37 2cnd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 2 ∈ ℂ )
38 27 adantr ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑖 ∈ ℂ )
39 33 adantl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℂ )
40 37 38 39 adddid ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 2 · ( 𝑖 + 𝑗 ) ) = ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) )
41 40 eqcomd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) = ( 2 · ( 𝑖 + 𝑗 ) ) )
42 41 oveq1d ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + ( 2 · 𝑗 ) ) + 1 ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
43 36 42 eqtrd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
44 43 ex ⊢ ( 𝑖 ∈ ℤ → ( 𝑗 ∈ ℤ → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) ) )
45 44 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝑗 ∈ ℤ → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) ) )
46 45 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
47 46 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ( ( ( 2 · 𝑖 ) + 1 ) + ( 2 · 𝑗 ) ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
48 25 47 eqtrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ( 𝐴 + 𝐵 ) = ( ( 2 · ( 𝑖 + 𝑗 ) ) + 1 ) )
49 17 21 48 rspcedvd ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ 𝐵 = ( 2 · 𝑗 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) )
50 49 rexlimdva2 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) ∧ 𝐵 ∈ ℤ ) → ( ∃ 𝑗 ∈ ℤ 𝐵 = ( 2 · 𝑗 ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
51 50 expimpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( 2 · 𝑗 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
52 51 r19.29an ⊢ ( ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝐵 ∈ ℤ ∧ ∃ 𝑗 ∈ ℤ 𝐵 = ( 2 · 𝑗 ) ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
53 12 52 syl5bi ⊢ ( ( 𝐴 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 2 · 𝑖 ) + 1 ) ) → ( 𝐵 ∈ Even → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
54 8 53 sylbi ⊢ ( 𝐴 ∈ Odd → ( 𝐵 ∈ Even → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
55 54 imp ⊢ ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) )
56 eqeq1 ⊢ ( 𝑧 = ( 𝐴 + 𝐵 ) → ( 𝑧 = ( ( 2 · 𝑛 ) + 1 ) ↔ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
57 56 rexbidv ⊢ ( 𝑧 = ( 𝐴 + 𝐵 ) → ( ∃ 𝑛 ∈ ℤ 𝑧 = ( ( 2 · 𝑛 ) + 1 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
58 dfodd6 ⊢ Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑛 ∈ ℤ 𝑧 = ( ( 2 · 𝑛 ) + 1 ) }
59 57 58 elrab2 ⊢ ( ( 𝐴 + 𝐵 ) ∈ Odd ↔ ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝐴 + 𝐵 ) = ( ( 2 · 𝑛 ) + 1 ) ) )
60 4 55 59 sylanbrc ⊢ ( ( 𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Odd )