Step | Hyp | Ref
| Expression |
1 | | odd2np1 11819 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (¬ 2
∥ 𝐴 ↔
∃𝑎 ∈ ℤ ((2
· 𝑎) + 1) = 𝐴)) |
2 | | 2z 9227 |
. . . . . . 7
⊢ 2 ∈
ℤ |
3 | | divides 11738 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐵
∈ ℤ) → (2 ∥ 𝐵 ↔ ∃𝑏 ∈ ℤ (𝑏 · 2) = 𝐵)) |
4 | 2, 3 | mpan 422 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → (2
∥ 𝐵 ↔
∃𝑏 ∈ ℤ
(𝑏 · 2) = 𝐵)) |
5 | 1, 4 | bi2anan9 601 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ 2 ∥
𝐵) ↔ (∃𝑎 ∈ ℤ ((2 ·
𝑎) + 1) = 𝐴 ∧ ∃𝑏 ∈ ℤ (𝑏 · 2) = 𝐵))) |
6 | | reeanv 2639 |
. . . . . 6
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) ↔ (∃𝑎 ∈ ℤ ((2 · 𝑎) + 1) = 𝐴 ∧ ∃𝑏 ∈ ℤ (𝑏 · 2) = 𝐵)) |
7 | | zsubcl 9240 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 − 𝑏) ∈ ℤ) |
8 | | zcn 9204 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
9 | | zcn 9204 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
10 | | 2cn 8936 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
11 | | subdi 8291 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · (𝑎 − 𝑏)) = ((2 · 𝑎) − (2 · 𝑏))) |
12 | 10, 11 | mp3an1 1319 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (2
· (𝑎 − 𝑏)) = ((2 · 𝑎) − (2 · 𝑏))) |
13 | 12 | oveq1d 5865 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((2
· (𝑎 − 𝑏)) + 1) = (((2 · 𝑎) − (2 · 𝑏)) + 1)) |
14 | | mulcl 7888 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑎
∈ ℂ) → (2 · 𝑎) ∈ ℂ) |
15 | 10, 14 | mpan 422 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℂ → (2
· 𝑎) ∈
ℂ) |
16 | | mulcl 7888 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · 𝑏) ∈ ℂ) |
17 | 10, 16 | mpan 422 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℂ → (2
· 𝑏) ∈
ℂ) |
18 | | ax-1cn 7854 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
19 | | addsub 8117 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑎) ∈ ℂ
∧ 1 ∈ ℂ ∧ (2 · 𝑏) ∈ ℂ) → (((2 · 𝑎) + 1) − (2 · 𝑏)) = (((2 · 𝑎) − (2 · 𝑏)) + 1)) |
20 | 18, 19 | mp3an2 1320 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑎) ∈ ℂ
∧ (2 · 𝑏) ∈
ℂ) → (((2 · 𝑎) + 1) − (2 · 𝑏)) = (((2 · 𝑎) − (2 · 𝑏)) + 1)) |
21 | 15, 17, 20 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (((2
· 𝑎) + 1) − (2
· 𝑏)) = (((2
· 𝑎) − (2
· 𝑏)) +
1)) |
22 | | mulcom 7890 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑏
∈ ℂ) → (2 · 𝑏) = (𝑏 · 2)) |
23 | 10, 22 | mpan 422 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℂ → (2
· 𝑏) = (𝑏 · 2)) |
24 | 23 | oveq2d 5866 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℂ → (((2
· 𝑎) + 1) − (2
· 𝑏)) = (((2
· 𝑎) + 1) −
(𝑏 ·
2))) |
25 | 24 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (((2
· 𝑎) + 1) − (2
· 𝑏)) = (((2
· 𝑎) + 1) −
(𝑏 ·
2))) |
26 | 13, 21, 25 | 3eqtr2d 2209 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((2
· (𝑎 − 𝑏)) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2))) |
27 | 8, 9, 26 | syl2an 287 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((2
· (𝑎 − 𝑏)) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2))) |
28 | | oveq2 5858 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑎 − 𝑏) → (2 · 𝑐) = (2 · (𝑎 − 𝑏))) |
29 | 28 | oveq1d 5865 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑎 − 𝑏) → ((2 · 𝑐) + 1) = ((2 · (𝑎 − 𝑏)) + 1)) |
30 | 29 | eqeq1d 2179 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑎 − 𝑏) → (((2 · 𝑐) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2)) ↔ ((2 · (𝑎 − 𝑏)) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2)))) |
31 | 30 | rspcev 2834 |
. . . . . . . . 9
⊢ (((𝑎 − 𝑏) ∈ ℤ ∧ ((2 · (𝑎 − 𝑏)) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2))) → ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (((2 ·
𝑎) + 1) − (𝑏 · 2))) |
32 | 7, 27, 31 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
∃𝑐 ∈ ℤ ((2
· 𝑐) + 1) = (((2
· 𝑎) + 1) −
(𝑏 ·
2))) |
33 | | oveq12 5859 |
. . . . . . . . . 10
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) → (((2 · 𝑎) + 1) − (𝑏 · 2)) = (𝐴 − 𝐵)) |
34 | 33 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) → (((2 · 𝑐) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2)) ↔ ((2 · 𝑐) + 1) = (𝐴 − 𝐵))) |
35 | 34 | rexbidv 2471 |
. . . . . . . 8
⊢ ((((2
· 𝑎) + 1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) → (∃𝑐 ∈ ℤ ((2 · 𝑐) + 1) = (((2 · 𝑎) + 1) − (𝑏 · 2)) ↔
∃𝑐 ∈ ℤ ((2
· 𝑐) + 1) = (𝐴 − 𝐵))) |
36 | 32, 35 | syl5ibcom 154 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((((2
· 𝑎) + 1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) → ∃𝑐 ∈ ℤ ((2 · 𝑐) + 1) = (𝐴 − 𝐵))) |
37 | 36 | rexlimivv 2593 |
. . . . . 6
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((2 · 𝑎) +
1) = 𝐴 ∧ (𝑏 · 2) = 𝐵) → ∃𝑐 ∈ ℤ ((2 · 𝑐) + 1) = (𝐴 − 𝐵)) |
38 | 6, 37 | sylbir 134 |
. . . . 5
⊢
((∃𝑎 ∈
ℤ ((2 · 𝑎) +
1) = 𝐴 ∧ ∃𝑏 ∈ ℤ (𝑏 · 2) = 𝐵) → ∃𝑐 ∈ ℤ ((2 · 𝑐) + 1) = (𝐴 − 𝐵)) |
39 | 5, 38 | syl6bi 162 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((¬
2 ∥ 𝐴 ∧ 2 ∥
𝐵) → ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (𝐴 − 𝐵))) |
40 | 39 | imp 123 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ 2 ∥
𝐵)) → ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (𝐴 − 𝐵)) |
41 | 40 | an4s 583 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥
𝐵)) → ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (𝐴 − 𝐵)) |
42 | | zsubcl 9240 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) |
43 | 42 | ad2ant2r 506 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥
𝐵)) → (𝐴 − 𝐵) ∈ ℤ) |
44 | | odd2np1 11819 |
. . 3
⊢ ((𝐴 − 𝐵) ∈ ℤ → (¬ 2 ∥
(𝐴 − 𝐵) ↔ ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (𝐴 − 𝐵))) |
45 | 43, 44 | syl 14 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥
𝐵)) → (¬ 2 ∥
(𝐴 − 𝐵) ↔ ∃𝑐 ∈ ℤ ((2 ·
𝑐) + 1) = (𝐴 − 𝐵))) |
46 | 41, 45 | mpbird 166 |
1
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥
𝐵)) → ¬ 2 ∥
(𝐴 − 𝐵)) |