Proof of Theorem 0nodd
Step | Hyp | Ref
| Expression |
1 | | halfnz 12284 |
. . . . . . . . . . 11
⊢ ¬ (1
/ 2) ∈ ℤ |
2 | | eleq1 2827 |
. . . . . . . . . . 11
⊢ ((1 / 2)
= -𝑥 → ((1 / 2) ∈
ℤ ↔ -𝑥 ∈
ℤ)) |
3 | 1, 2 | mtbii 329 |
. . . . . . . . . 10
⊢ ((1 / 2)
= -𝑥 → ¬ -𝑥 ∈
ℤ) |
4 | | znegcl 12241 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → -𝑥 ∈
ℤ) |
5 | 3, 4 | nsyl3 140 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → ¬ (1
/ 2) = -𝑥) |
6 | | eqcom 2746 |
. . . . . . . . 9
⊢ (-𝑥 = (1 / 2) ↔ (1 / 2) =
-𝑥) |
7 | 5, 6 | sylnibr 332 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → ¬
-𝑥 = (1 /
2)) |
8 | | ax-1cn 10816 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
9 | | 2cn 11934 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
10 | | 2ne0 11963 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
11 | | divneg 11553 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 /
2)) |
12 | 11 | eqcomd 2745 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (-1 / 2) = -(1 /
2)) |
13 | 8, 9, 10, 12 | mp3an 1463 |
. . . . . . . . . . 11
⊢ (-1 / 2)
= -(1 / 2) |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → (-1 / 2)
= -(1 / 2)) |
15 | 14 | eqeq1d 2741 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → ((-1 / 2)
= 𝑥 ↔ -(1 / 2) = 𝑥)) |
16 | | halfcn 12074 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → (1 / 2)
∈ ℂ) |
18 | | zcn 12210 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
19 | 17, 18 | negcon1d 11212 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → (-(1 / 2)
= 𝑥 ↔ -𝑥 = (1 / 2))) |
20 | 15, 19 | bitrd 282 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → ((-1 / 2)
= 𝑥 ↔ -𝑥 = (1 / 2))) |
21 | 7, 20 | mtbird 328 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → ¬ (-1
/ 2) = 𝑥) |
22 | | neg1cn 11973 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → -1 ∈
ℂ) |
24 | | 2cnd 11937 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → 2 ∈
ℂ) |
25 | 10 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → 2 ≠
0) |
26 | 23, 18, 24, 25 | divmul2d 11670 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → ((-1 / 2)
= 𝑥 ↔ -1 = (2 ·
𝑥))) |
27 | 21, 26 | mtbid 327 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → ¬ -1
= (2 · 𝑥)) |
28 | | eqcom 2746 |
. . . . . . . 8
⊢ (0 = ((2
· 𝑥) + 1) ↔ ((2
· 𝑥) + 1) =
0) |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (0 = ((2
· 𝑥) + 1) ↔ ((2
· 𝑥) + 1) =
0)) |
30 | | 0cnd 10855 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → 0 ∈
ℂ) |
31 | | 1cnd 10857 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → 1 ∈
ℂ) |
32 | 24, 18 | mulcld 10882 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
33 | | subadd2 11111 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ ∧ (2 · 𝑥) ∈ ℂ) → ((0 − 1) = (2
· 𝑥) ↔ ((2
· 𝑥) + 1) =
0)) |
34 | 33 | bicomd 226 |
. . . . . . . 8
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ ∧ (2 · 𝑥) ∈ ℂ) → (((2 · 𝑥) + 1) = 0 ↔ (0 − 1)
= (2 · 𝑥))) |
35 | 30, 31, 32, 34 | syl3anc 1373 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) = 0 ↔
(0 − 1) = (2 · 𝑥))) |
36 | | df-neg 11094 |
. . . . . . . . . 10
⊢ -1 = (0
− 1) |
37 | 36 | eqcomi 2748 |
. . . . . . . . 9
⊢ (0
− 1) = -1 |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → (0
− 1) = -1) |
39 | 38 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → ((0
− 1) = (2 · 𝑥)
↔ -1 = (2 · 𝑥))) |
40 | 29, 35, 39 | 3bitrd 308 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → (0 = ((2
· 𝑥) + 1) ↔ -1
= (2 · 𝑥))) |
41 | 27, 40 | mtbird 328 |
. . . . 5
⊢ (𝑥 ∈ ℤ → ¬ 0 =
((2 · 𝑥) +
1)) |
42 | 41 | nrex 3197 |
. . . 4
⊢ ¬
∃𝑥 ∈ ℤ 0 =
((2 · 𝑥) +
1) |
43 | 42 | intnan 490 |
. . 3
⊢ ¬ (0
∈ ℤ ∧ ∃𝑥 ∈ ℤ 0 = ((2 · 𝑥) + 1)) |
44 | | eqeq1 2743 |
. . . . 5
⊢ (𝑧 = 0 → (𝑧 = ((2 · 𝑥) + 1) ↔ 0 = ((2 · 𝑥) + 1))) |
45 | 44 | rexbidv 3226 |
. . . 4
⊢ (𝑧 = 0 → (∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1) ↔ ∃𝑥 ∈ ℤ 0 = ((2 ·
𝑥) + 1))) |
46 | | oddinmgm.e |
. . . 4
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} |
47 | 45, 46 | elrab2 3620 |
. . 3
⊢ (0 ∈
𝑂 ↔ (0 ∈ ℤ
∧ ∃𝑥 ∈
ℤ 0 = ((2 · 𝑥)
+ 1))) |
48 | 43, 47 | mtbir 326 |
. 2
⊢ ¬ 0
∈ 𝑂 |
49 | 48 | nelir 3052 |
1
⊢ 0 ∉
𝑂 |