Step | Hyp | Ref
| Expression |
1 | | neg1cn 8983 |
. . 3
⊢ -1 ∈
ℂ |
2 | | prid1g 3687 |
. . 3
⊢ (-1
∈ ℂ → -1 ∈ {-1, 1}) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ -1 ∈
{-1, 1} |
4 | | neg1ap0 8987 |
. 2
⊢ -1 #
0 |
5 | | ax-1cn 7867 |
. . . 4
⊢ 1 ∈
ℂ |
6 | | prssi 3738 |
. . . 4
⊢ ((-1
∈ ℂ ∧ 1 ∈ ℂ) → {-1, 1} ⊆
ℂ) |
7 | 1, 5, 6 | mp2an 424 |
. . 3
⊢ {-1, 1}
⊆ ℂ |
8 | | elpri 3606 |
. . . . 5
⊢ (𝑥 ∈ {-1, 1} → (𝑥 = -1 ∨ 𝑥 = 1)) |
9 | 7 | sseli 3143 |
. . . . . . . . 9
⊢ (𝑦 ∈ {-1, 1} → 𝑦 ∈
ℂ) |
10 | 9 | mulm1d 8329 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → (-1
· 𝑦) = -𝑦) |
11 | | elpri 3606 |
. . . . . . . . 9
⊢ (𝑦 ∈ {-1, 1} → (𝑦 = -1 ∨ 𝑦 = 1)) |
12 | | negeq 8112 |
. . . . . . . . . . 11
⊢ (𝑦 = -1 → -𝑦 = --1) |
13 | | negneg1e1 8988 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
14 | | 1ex 7915 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
15 | 14 | prid2 3690 |
. . . . . . . . . . . 12
⊢ 1 ∈
{-1, 1} |
16 | 13, 15 | eqeltri 2243 |
. . . . . . . . . . 11
⊢ --1
∈ {-1, 1} |
17 | 12, 16 | eqeltrdi 2261 |
. . . . . . . . . 10
⊢ (𝑦 = -1 → -𝑦 ∈ {-1, 1}) |
18 | | negeq 8112 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → -𝑦 = -1) |
19 | 18, 3 | eqeltrdi 2261 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → -𝑦 ∈ {-1, 1}) |
20 | 17, 19 | jaoi 711 |
. . . . . . . . 9
⊢ ((𝑦 = -1 ∨ 𝑦 = 1) → -𝑦 ∈ {-1, 1}) |
21 | 11, 20 | syl 14 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → -𝑦 ∈ {-1,
1}) |
22 | 10, 21 | eqeltrd 2247 |
. . . . . . 7
⊢ (𝑦 ∈ {-1, 1} → (-1
· 𝑦) ∈ {-1,
1}) |
23 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑥 = -1 → (𝑥 · 𝑦) = (-1 · 𝑦)) |
24 | 23 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑥 = -1 → ((𝑥 · 𝑦) ∈ {-1, 1} ↔ (-1 · 𝑦) ∈ {-1,
1})) |
25 | 22, 24 | syl5ibr 155 |
. . . . . 6
⊢ (𝑥 = -1 → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
26 | 9 | mulid2d 7938 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → (1
· 𝑦) = 𝑦) |
27 | | id 19 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → 𝑦 ∈ {-1,
1}) |
28 | 26, 27 | eqeltrd 2247 |
. . . . . . 7
⊢ (𝑦 ∈ {-1, 1} → (1
· 𝑦) ∈ {-1,
1}) |
29 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 · 𝑦) = (1 · 𝑦)) |
30 | 29 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑥 · 𝑦) ∈ {-1, 1} ↔ (1 · 𝑦) ∈ {-1,
1})) |
31 | 28, 30 | syl5ibr 155 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
32 | 25, 31 | jaoi 711 |
. . . . 5
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
33 | 8, 32 | syl 14 |
. . . 4
⊢ (𝑥 ∈ {-1, 1} → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
34 | 33 | imp 123 |
. . 3
⊢ ((𝑥 ∈ {-1, 1} ∧ 𝑦 ∈ {-1, 1}) → (𝑥 · 𝑦) ∈ {-1, 1}) |
35 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑥 = -1 → (1 / 𝑥) = (1 / -1)) |
36 | | 1ap0 8509 |
. . . . . . . . . 10
⊢ 1 #
0 |
37 | | divneg2ap 8653 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 # 0) → -(1 / 1) = (1 /
-1)) |
38 | 5, 5, 36, 37 | mp3an 1332 |
. . . . . . . . 9
⊢ -(1 / 1)
= (1 / -1) |
39 | | 1div1e1 8621 |
. . . . . . . . . 10
⊢ (1 / 1) =
1 |
40 | 39 | negeqi 8113 |
. . . . . . . . 9
⊢ -(1 / 1)
= -1 |
41 | 38, 40 | eqtr3i 2193 |
. . . . . . . 8
⊢ (1 / -1)
= -1 |
42 | 41, 3 | eqeltri 2243 |
. . . . . . 7
⊢ (1 / -1)
∈ {-1, 1} |
43 | 35, 42 | eqeltrdi 2261 |
. . . . . 6
⊢ (𝑥 = -1 → (1 / 𝑥) ∈ {-1,
1}) |
44 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑥 = 1 → (1 / 𝑥) = (1 / 1)) |
45 | 39, 15 | eqeltri 2243 |
. . . . . . 7
⊢ (1 / 1)
∈ {-1, 1} |
46 | 44, 45 | eqeltrdi 2261 |
. . . . . 6
⊢ (𝑥 = 1 → (1 / 𝑥) ∈ {-1,
1}) |
47 | 43, 46 | jaoi 711 |
. . . . 5
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (1 / 𝑥) ∈ {-1, 1}) |
48 | 8, 47 | syl 14 |
. . . 4
⊢ (𝑥 ∈ {-1, 1} → (1 /
𝑥) ∈ {-1,
1}) |
49 | 48 | adantr 274 |
. . 3
⊢ ((𝑥 ∈ {-1, 1} ∧ 𝑥 # 0) → (1 / 𝑥) ∈ {-1,
1}) |
50 | 7, 34, 15, 49 | expcl2lemap 10488 |
. 2
⊢ ((-1
∈ {-1, 1} ∧ -1 # 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ {-1,
1}) |
51 | 3, 4, 50 | mp3an12 1322 |
1
⊢ (𝑁 ∈ ℤ →
(-1↑𝑁) ∈ {-1,
1}) |