Step | Hyp | Ref
| Expression |
1 | | oddz 44756 |
. . 3
⊢ (𝐴 ∈ Odd → 𝐴 ∈
ℤ) |
2 | | oddz 44756 |
. . 3
⊢ (𝐵 ∈ Odd → 𝐵 ∈
ℤ) |
3 | | zaddcl 12217 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ) |
4 | 1, 2, 3 | syl2an 599 |
. 2
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ ℤ) |
5 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑎 = ((2 · 𝑖) + 1) ↔ 𝐴 = ((2 · 𝑖) + 1))) |
6 | 5 | rexbidv 3216 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∃𝑖 ∈ ℤ 𝑎 = ((2 · 𝑖) + 1) ↔ ∃𝑖 ∈ ℤ 𝐴 = ((2 · 𝑖) + 1))) |
7 | | dfodd6 44762 |
. . . . 5
⊢ Odd =
{𝑎 ∈ ℤ ∣
∃𝑖 ∈ ℤ
𝑎 = ((2 · 𝑖) + 1)} |
8 | 6, 7 | elrab2 3605 |
. . . 4
⊢ (𝐴 ∈ Odd ↔ (𝐴 ∈ ℤ ∧
∃𝑖 ∈ ℤ
𝐴 = ((2 · 𝑖) + 1))) |
9 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 = ((2 · 𝑗) + 1) ↔ 𝐵 = ((2 · 𝑗) + 1))) |
10 | 9 | rexbidv 3216 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∃𝑗 ∈ ℤ 𝑏 = ((2 · 𝑗) + 1) ↔ ∃𝑗 ∈ ℤ 𝐵 = ((2 · 𝑗) + 1))) |
11 | | dfodd6 44762 |
. . . . . 6
⊢ Odd =
{𝑏 ∈ ℤ ∣
∃𝑗 ∈ ℤ
𝑏 = ((2 · 𝑗) + 1)} |
12 | 10, 11 | elrab2 3605 |
. . . . 5
⊢ (𝐵 ∈ Odd ↔ (𝐵 ∈ ℤ ∧
∃𝑗 ∈ ℤ
𝐵 = ((2 · 𝑗) + 1))) |
13 | | zaddcl 12217 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 + 𝑗) ∈ ℤ) |
14 | 13 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℤ → (𝑗 ∈ ℤ → (𝑖 + 𝑗) ∈ ℤ)) |
15 | 14 | ad3antlr 731 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((2 · 𝑖) + 1)) ∧ 𝐵 ∈ ℤ) → (𝑗 ∈ ℤ → (𝑖 + 𝑗) ∈ ℤ)) |
16 | 15 | imp 410 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) →
(𝑖 + 𝑗) ∈ ℤ) |
17 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → (𝑖 + 𝑗) ∈ ℤ) |
18 | 17 | peano2zd 12285 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → ((𝑖 + 𝑗) + 1) ∈ ℤ) |
19 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑛 = ((𝑖 + 𝑗) + 1) → (2 · 𝑛) = (2 · ((𝑖 + 𝑗) + 1))) |
20 | 19 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑛 = ((𝑖 + 𝑗) + 1) → ((𝐴 + 𝐵) = (2 · 𝑛) ↔ (𝐴 + 𝐵) = (2 · ((𝑖 + 𝑗) + 1)))) |
21 | 20 | adantl 485 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) ∧ 𝑛 = ((𝑖 + 𝑗) + 1)) → ((𝐴 + 𝐵) = (2 · 𝑛) ↔ (𝐴 + 𝐵) = (2 · ((𝑖 + 𝑗) + 1)))) |
22 | | oveq12 7222 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ((2 · 𝑖) + 1) ∧ 𝐵 = ((2 · 𝑗) + 1)) → (𝐴 + 𝐵) = (((2 · 𝑖) + 1) + ((2 · 𝑗) + 1))) |
23 | 22 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ((2 · 𝑖) + 1) → (𝐵 = ((2 · 𝑗) + 1) → (𝐴 + 𝐵) = (((2 · 𝑖) + 1) + ((2 · 𝑗) + 1)))) |
24 | 23 | ad3antlr 731 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) →
(𝐵 = ((2 · 𝑗) + 1) → (𝐴 + 𝐵) = (((2 · 𝑖) + 1) + ((2 · 𝑗) + 1)))) |
25 | 24 | imp 410 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → (𝐴 + 𝐵) = (((2 · 𝑖) + 1) + ((2 · 𝑗) + 1))) |
26 | | zcn 12181 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
27 | | zcn 12181 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
ℂ) |
28 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℂ → 2 ∈
ℂ) |
29 | 28 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (2
∈ ℂ ∧ 𝑖
∈ ℂ)) |
30 | 29 | ancoms 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (2
∈ ℂ ∧ 𝑖
∈ ℂ)) |
31 | | mulcl 10813 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℂ ∧ 𝑖
∈ ℂ) → (2 · 𝑖) ∈ ℂ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (2
· 𝑖) ∈
ℂ) |
33 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → 1 ∈
ℂ) |
34 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℂ → 2 ∈
ℂ) |
35 | | mulcl 10813 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℂ) → (2 · 𝑗) ∈ ℂ) |
36 | 34, 35 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (2
· 𝑗) ∈
ℂ) |
37 | 32, 33, 36, 33 | add4d 11060 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (((2
· 𝑖) + 1) + ((2
· 𝑗) + 1)) = (((2
· 𝑖) + (2 ·
𝑗)) + (1 +
1))) |
38 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → 2 ∈
ℂ) |
39 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → 𝑖 ∈
ℂ) |
40 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → 𝑗 ∈
ℂ) |
41 | 38, 39, 40 | adddid 10857 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (2
· (𝑖 + 𝑗)) = ((2 · 𝑖) + (2 · 𝑗))) |
42 | 41 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((2
· (𝑖 + 𝑗)) + (2 · 1)) = (((2
· 𝑖) + (2 ·
𝑗)) + (2 ·
1))) |
43 | | addcl 10811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑖 + 𝑗) ∈ ℂ) |
44 | 38, 43, 33 | adddid 10857 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (2
· ((𝑖 + 𝑗) + 1)) = ((2 · (𝑖 + 𝑗)) + (2 · 1))) |
45 | | 1p1e2 11955 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 + 1) =
2 |
46 | | 2t1e2 11993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) = 2 |
47 | 45, 46 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 + 1) =
(2 · 1) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (1 + 1)
= (2 · 1)) |
49 | 48 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (((2
· 𝑖) + (2 ·
𝑗)) + (1 + 1)) = (((2
· 𝑖) + (2 ·
𝑗)) + (2 ·
1))) |
50 | 42, 44, 49 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (((2
· 𝑖) + (2 ·
𝑗)) + (1 + 1)) = (2
· ((𝑖 + 𝑗) + 1))) |
51 | 37, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (((2
· 𝑖) + 1) + ((2
· 𝑗) + 1)) = (2
· ((𝑖 + 𝑗) + 1))) |
52 | 26, 27, 51 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (((2
· 𝑖) + 1) + ((2
· 𝑗) + 1)) = (2
· ((𝑖 + 𝑗) + 1))) |
53 | 52 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℤ → (𝑗 ∈ ℤ → (((2
· 𝑖) + 1) + ((2
· 𝑗) + 1)) = (2
· ((𝑖 + 𝑗) + 1)))) |
54 | 53 | ad3antlr 731 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((2 · 𝑖) + 1)) ∧ 𝐵 ∈ ℤ) → (𝑗 ∈ ℤ → (((2 · 𝑖) + 1) + ((2 · 𝑗) + 1)) = (2 · ((𝑖 + 𝑗) + 1)))) |
55 | 54 | imp 410 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) →
(((2 · 𝑖) + 1) + ((2
· 𝑗) + 1)) = (2
· ((𝑖 + 𝑗) + 1))) |
56 | 55 | adantr 484 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → (((2 ·
𝑖) + 1) + ((2 ·
𝑗) + 1)) = (2 ·
((𝑖 + 𝑗) + 1))) |
57 | 25, 56 | eqtrd 2777 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → (𝐴 + 𝐵) = (2 · ((𝑖 + 𝑗) + 1))) |
58 | 18, 21, 57 | rspcedvd 3540 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℤ ∧ 𝑖 ∈
ℤ) ∧ 𝐴 = ((2
· 𝑖) + 1)) ∧
𝐵 ∈ ℤ) ∧
𝑗 ∈ ℤ) ∧
𝐵 = ((2 · 𝑗) + 1)) → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛)) |
59 | 58 | rexlimdva2 3206 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((2 · 𝑖) + 1)) ∧ 𝐵 ∈ ℤ) → (∃𝑗 ∈ ℤ 𝐵 = ((2 · 𝑗) + 1) → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
60 | 59 | expimpd 457 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((2 · 𝑖) + 1)) → ((𝐵 ∈ ℤ ∧
∃𝑗 ∈ ℤ
𝐵 = ((2 · 𝑗) + 1)) → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
61 | 60 | rexlimdva2 3206 |
. . . . . 6
⊢ (𝐴 ∈ ℤ →
(∃𝑖 ∈ ℤ
𝐴 = ((2 · 𝑖) + 1) → ((𝐵 ∈ ℤ ∧
∃𝑗 ∈ ℤ
𝐵 = ((2 · 𝑗) + 1)) → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛)))) |
62 | 61 | imp 410 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧
∃𝑖 ∈ ℤ
𝐴 = ((2 · 𝑖) + 1)) → ((𝐵 ∈ ℤ ∧
∃𝑗 ∈ ℤ
𝐵 = ((2 · 𝑗) + 1)) → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
63 | 12, 62 | syl5bi 245 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧
∃𝑖 ∈ ℤ
𝐴 = ((2 · 𝑖) + 1)) → (𝐵 ∈ Odd → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
64 | 8, 63 | sylbi 220 |
. . 3
⊢ (𝐴 ∈ Odd → (𝐵 ∈ Odd → ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
65 | 64 | imp 410 |
. 2
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) →
∃𝑛 ∈ ℤ
(𝐴 + 𝐵) = (2 · 𝑛)) |
66 | | eqeq1 2741 |
. . . 4
⊢ (𝑧 = (𝐴 + 𝐵) → (𝑧 = (2 · 𝑛) ↔ (𝐴 + 𝐵) = (2 · 𝑛))) |
67 | 66 | rexbidv 3216 |
. . 3
⊢ (𝑧 = (𝐴 + 𝐵) → (∃𝑛 ∈ ℤ 𝑧 = (2 · 𝑛) ↔ ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
68 | | dfeven4 44763 |
. . 3
⊢ Even =
{𝑧 ∈ ℤ ∣
∃𝑛 ∈ ℤ
𝑧 = (2 · 𝑛)} |
69 | 67, 68 | elrab2 3605 |
. 2
⊢ ((𝐴 + 𝐵) ∈ Even ↔ ((𝐴 + 𝐵) ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝐴 + 𝐵) = (2 · 𝑛))) |
70 | 4, 65, 69 | sylanbrc 586 |
1
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Even ) |