| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | odd2np1 16379 | . . . . 5
⊢ (𝐴 ∈ ℤ → (¬ 2
∥ 𝐴 ↔
∃𝑎 ∈ ℤ ((2
· 𝑎) + 1) = 𝐴)) | 
| 2 |  | odd2np1 16379 | . . . . 5
⊢ (𝐵 ∈ ℤ → (¬ 2
∥ 𝐵 ↔
∃𝑏 ∈ ℤ ((2
· 𝑏) + 1) = 𝐵)) | 
| 3 | 1, 2 | bi2anan9 638 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ ¬ 2
∥ 𝐵) ↔
(∃𝑎 ∈ ℤ
((2 · 𝑎) + 1) =
𝐴 ∧ ∃𝑏 ∈ ℤ ((2 ·
𝑏) + 1) = 𝐵))) | 
| 4 |  | reeanv 3228 | . . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ ((2 ·
𝑏) + 1) = 𝐵) ↔ (∃𝑎 ∈ ℤ ((2 · 𝑎) + 1) = 𝐴 ∧ ∃𝑏 ∈ ℤ ((2 · 𝑏) + 1) = 𝐵)) | 
| 5 |  | 2z 12651 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 6 |  | zsubcl 12661 | . . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 − 𝑏) ∈ ℤ) | 
| 7 |  | dvdsmul1 16316 | . . . . . . . . 9
⊢ ((2
∈ ℤ ∧ (𝑎
− 𝑏) ∈ ℤ)
→ 2 ∥ (2 · (𝑎 − 𝑏))) | 
| 8 | 5, 6, 7 | sylancr 587 | . . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 2
∥ (2 · (𝑎
− 𝑏))) | 
| 9 |  | zcn 12620 | . . . . . . . . 9
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) | 
| 10 |  | zcn 12620 | . . . . . . . . 9
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) | 
| 11 |  | 2cn 12342 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 12 |  | mulcl 11240 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ) → (2 · 𝑎) ∈ ℂ) | 
| 13 | 11, 12 | mpan 690 | . . . . . . . . . . 11
⊢ (𝑎 ∈ ℂ → (2
· 𝑎) ∈
ℂ) | 
| 14 |  | mulcl 11240 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · 𝑏) ∈ ℂ) | 
| 15 | 11, 14 | mpan 690 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ℂ → (2
· 𝑏) ∈
ℂ) | 
| 16 |  | ax-1cn 11214 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 17 |  | pnpcan2 11550 | . . . . . . . . . . . 12
⊢ (((2
· 𝑎) ∈ ℂ
∧ (2 · 𝑏) ∈
ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑎) + 1) − ((2 · 𝑏) + 1)) = ((2 · 𝑎) − (2 · 𝑏))) | 
| 18 | 16, 17 | mp3an3 1451 | . . . . . . . . . . 11
⊢ (((2
· 𝑎) ∈ ℂ
∧ (2 · 𝑏) ∈
ℂ) → (((2 · 𝑎) + 1) − ((2 · 𝑏) + 1)) = ((2 · 𝑎) − (2 · 𝑏))) | 
| 19 | 13, 15, 18 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (((2
· 𝑎) + 1) −
((2 · 𝑏) + 1)) = ((2
· 𝑎) − (2
· 𝑏))) | 
| 20 |  | subdi 11697 | . . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · (𝑎 − 𝑏)) = ((2 · 𝑎) − (2 · 𝑏))) | 
| 21 | 11, 20 | mp3an1 1449 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· (𝑎 − 𝑏)) = ((2 · 𝑎) − (2 · 𝑏))) | 
| 22 | 19, 21 | eqtr4d 2779 | . . . . . . . . 9
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (((2
· 𝑎) + 1) −
((2 · 𝑏) + 1)) = (2
· (𝑎 − 𝑏))) | 
| 23 | 9, 10, 22 | syl2an 596 | . . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (((2
· 𝑎) + 1) −
((2 · 𝑏) + 1)) = (2
· (𝑎 − 𝑏))) | 
| 24 | 8, 23 | breqtrrd 5170 | . . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 2
∥ (((2 · 𝑎) +
1) − ((2 · 𝑏)
+ 1))) | 
| 25 |  | oveq12 7441 | . . . . . . . 8
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → (((2 · 𝑎) + 1) − ((2 · 𝑏) + 1)) = (𝐴 − 𝐵)) | 
| 26 | 25 | breq2d 5154 | . . . . . . 7
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → (2 ∥ (((2 · 𝑎) + 1) − ((2 ·
𝑏) + 1)) ↔ 2 ∥
(𝐴 − 𝐵))) | 
| 27 | 24, 26 | syl5ibcom 245 | . . . . . 6
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((((2
· 𝑎) + 1) = 𝐴 ∧ ((2 · 𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 − 𝐵))) | 
| 28 | 27 | rexlimivv 3200 | . . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ ((2 ·
𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 − 𝐵)) | 
| 29 | 4, 28 | sylbir 235 | . . . 4
⊢
((∃𝑎 ∈
ℤ ((2 · 𝑎) +
1) = 𝐴 ∧ ∃𝑏 ∈ ℤ ((2 ·
𝑏) + 1) = 𝐵) → 2 ∥ (𝐴 − 𝐵)) | 
| 30 | 3, 29 | biimtrdi 253 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ ¬ 2
∥ 𝐵) → 2 ∥
(𝐴 − 𝐵))) | 
| 31 | 30 | imp 406 | . 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → 2
∥ (𝐴 − 𝐵)) | 
| 32 | 31 | an4s 660 | 1
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2
∥ 𝐵)) → 2
∥ (𝐴 − 𝐵)) |