| Step | Hyp | Ref
| Expression |
| 1 | | odd2np1 16378 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (¬ 2
∥ 𝐴 ↔
∃𝑎 ∈ ℤ ((2
· 𝑎) + 1) = 𝐴)) |
| 2 | | odd2np1 16378 |
. . . . 5
⊢ (𝐵 ∈ ℤ → (¬ 2
∥ 𝐵 ↔
∃𝑏 ∈ ℤ ((2
· 𝑏) + 1) = 𝐵)) |
| 3 | 1, 2 | bi2anan9 638 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ ¬ 2
∥ 𝐵) ↔
(∃𝑎 ∈ ℤ
((2 · 𝑎) + 1) =
𝐴 ∧ ∃𝑏 ∈ ℤ ((2 ·
𝑏) + 1) = 𝐵))) |
| 4 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ ((2 ·
𝑏) + 1) = 𝐵) ↔ (∃𝑎 ∈ ℤ ((2 · 𝑎) + 1) = 𝐴 ∧ ∃𝑏 ∈ ℤ ((2 · 𝑏) + 1) = 𝐵)) |
| 5 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 6 | | zaddcl 12657 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
| 7 | 6 | peano2zd 12725 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝑎 + 𝑏) + 1) ∈ ℤ) |
| 8 | | dvdsmul1 16315 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ ((𝑎 +
𝑏) + 1) ∈ ℤ)
→ 2 ∥ (2 · ((𝑎 + 𝑏) + 1))) |
| 9 | 5, 7, 8 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 2
∥ (2 · ((𝑎 +
𝑏) + 1))) |
| 10 | | zcn 12618 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
| 11 | | zcn 12618 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
| 12 | | addcl 11237 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ) |
| 13 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 14 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 15 | | adddi 11244 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ (𝑎 +
𝑏) ∈ ℂ ∧ 1
∈ ℂ) → (2 · ((𝑎 + 𝑏) + 1)) = ((2 · (𝑎 + 𝑏)) + (2 · 1))) |
| 16 | 13, 14, 15 | mp3an13 1454 |
. . . . . . . . . . . . 13
⊢ ((𝑎 + 𝑏) ∈ ℂ → (2 · ((𝑎 + 𝑏) + 1)) = ((2 · (𝑎 + 𝑏)) + (2 · 1))) |
| 17 | 12, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· ((𝑎 + 𝑏) + 1)) = ((2 · (𝑎 + 𝑏)) + (2 · 1))) |
| 18 | | adddi 11244 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · (𝑎 + 𝑏)) = ((2 · 𝑎) + (2 · 𝑏))) |
| 19 | 13, 18 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· (𝑎 + 𝑏)) = ((2 · 𝑎) + (2 · 𝑏))) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((2
· (𝑎 + 𝑏)) + (2 · 1)) = (((2
· 𝑎) + (2 ·
𝑏)) + (2 ·
1))) |
| 21 | 17, 20 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· ((𝑎 + 𝑏) + 1)) = (((2 · 𝑎) + (2 · 𝑏)) + (2 ·
1))) |
| 22 | | 2t1e2 12429 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = 2 |
| 23 | | df-2 12329 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
| 24 | 22, 23 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (2
· 1) = (1 + 1) |
| 25 | 24 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (((2
· 𝑎) + (2 ·
𝑏)) + (2 · 1)) =
(((2 · 𝑎) + (2
· 𝑏)) + (1 +
1)) |
| 26 | 21, 25 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· ((𝑎 + 𝑏) + 1)) = (((2 · 𝑎) + (2 · 𝑏)) + (1 + 1))) |
| 27 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ) → (2 · 𝑎) ∈ ℂ) |
| 28 | 13, 27 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℂ → (2
· 𝑎) ∈
ℂ) |
| 29 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · 𝑏) ∈ ℂ) |
| 30 | 13, 29 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℂ → (2
· 𝑏) ∈
ℂ) |
| 31 | | add4 11482 |
. . . . . . . . . . . 12
⊢ ((((2
· 𝑎) ∈ ℂ
∧ (2 · 𝑏) ∈
ℂ) ∧ (1 ∈ ℂ ∧ 1 ∈ ℂ)) → (((2 ·
𝑎) + (2 · 𝑏)) + (1 + 1)) = (((2 ·
𝑎) + 1) + ((2 ·
𝑏) + 1))) |
| 32 | 14, 14, 31 | mpanr12 705 |
. . . . . . . . . . 11
⊢ (((2
· 𝑎) ∈ ℂ
∧ (2 · 𝑏) ∈
ℂ) → (((2 · 𝑎) + (2 · 𝑏)) + (1 + 1)) = (((2 · 𝑎) + 1) + ((2 · 𝑏) + 1))) |
| 33 | 28, 30, 32 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (((2
· 𝑎) + (2 ·
𝑏)) + (1 + 1)) = (((2
· 𝑎) + 1) + ((2
· 𝑏) +
1))) |
| 34 | 26, 33 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· ((𝑎 + 𝑏) + 1)) = (((2 · 𝑎) + 1) + ((2 · 𝑏) + 1))) |
| 35 | 10, 11, 34 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (2
· ((𝑎 + 𝑏) + 1)) = (((2 · 𝑎) + 1) + ((2 · 𝑏) + 1))) |
| 36 | 9, 35 | breqtrd 5169 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 2
∥ (((2 · 𝑎) +
1) + ((2 · 𝑏) +
1))) |
| 37 | | oveq12 7440 |
. . . . . . . 8
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → (((2 · 𝑎) + 1) + ((2 · 𝑏) + 1)) = (𝐴 + 𝐵)) |
| 38 | 37 | breq2d 5155 |
. . . . . . 7
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → (2 ∥ (((2 · 𝑎) + 1) + ((2 · 𝑏) + 1)) ↔ 2 ∥ (𝐴 + 𝐵))) |
| 39 | 36, 38 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 + 𝐵))) |
| 40 | 39 | rexlimivv 3201 |
. . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ ((2 ·
𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 + 𝐵)) |
| 41 | 4, 40 | sylbir 235 |
. . . 4
⊢
((∃𝑎 ∈
ℤ ((2 · 𝑎) +
1) = 𝐴 ∧ ∃𝑏 ∈ ℤ ((2 ·
𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 + 𝐵)) |
| 42 | 3, 41 | biimtrdi 253 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ ¬ 2
∥ 𝐵) → 2 ∥
(𝐴 + 𝐵))) |
| 43 | 42 | imp 406 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → 2
∥ (𝐴 + 𝐵)) |
| 44 | 43 | an4s 660 |
1
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2
∥ 𝐵)) → 2
∥ (𝐴 + 𝐵)) |