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 ) |