| Step | Hyp | Ref
| Expression |
| 1 | | negex 11506 |
. . 3
⊢ -1 ∈
V |
| 2 | 1 | prid1 4762 |
. 2
⊢ -1 ∈
{-1, 1} |
| 3 | | neg1ne0 12382 |
. 2
⊢ -1 ≠
0 |
| 4 | | neg1cn 12380 |
. . . 4
⊢ -1 ∈
ℂ |
| 5 | | ax-1cn 11213 |
. . . 4
⊢ 1 ∈
ℂ |
| 6 | | prssi 4821 |
. . . 4
⊢ ((-1
∈ ℂ ∧ 1 ∈ ℂ) → {-1, 1} ⊆
ℂ) |
| 7 | 4, 5, 6 | mp2an 692 |
. . 3
⊢ {-1, 1}
⊆ ℂ |
| 8 | | elpri 4649 |
. . . . 5
⊢ (𝑥 ∈ {-1, 1} → (𝑥 = -1 ∨ 𝑥 = 1)) |
| 9 | 7 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑦 ∈ {-1, 1} → 𝑦 ∈
ℂ) |
| 10 | 9 | mulm1d 11715 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → (-1
· 𝑦) = -𝑦) |
| 11 | | elpri 4649 |
. . . . . . . . 9
⊢ (𝑦 ∈ {-1, 1} → (𝑦 = -1 ∨ 𝑦 = 1)) |
| 12 | | negeq 11500 |
. . . . . . . . . . 11
⊢ (𝑦 = -1 → -𝑦 = --1) |
| 13 | | negneg1e1 12384 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
| 14 | | 1ex 11257 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
| 15 | 14 | prid2 4763 |
. . . . . . . . . . . 12
⊢ 1 ∈
{-1, 1} |
| 16 | 13, 15 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ --1
∈ {-1, 1} |
| 17 | 12, 16 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ (𝑦 = -1 → -𝑦 ∈ {-1, 1}) |
| 18 | | negeq 11500 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → -𝑦 = -1) |
| 19 | 18, 2 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → -𝑦 ∈ {-1, 1}) |
| 20 | 17, 19 | jaoi 858 |
. . . . . . . . 9
⊢ ((𝑦 = -1 ∨ 𝑦 = 1) → -𝑦 ∈ {-1, 1}) |
| 21 | 11, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → -𝑦 ∈ {-1,
1}) |
| 22 | 10, 21 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝑦 ∈ {-1, 1} → (-1
· 𝑦) ∈ {-1,
1}) |
| 23 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑥 = -1 → (𝑥 · 𝑦) = (-1 · 𝑦)) |
| 24 | 23 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = -1 → ((𝑥 · 𝑦) ∈ {-1, 1} ↔ (-1 · 𝑦) ∈ {-1,
1})) |
| 25 | 22, 24 | imbitrrid 246 |
. . . . . 6
⊢ (𝑥 = -1 → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
| 26 | 9 | mullidd 11279 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → (1
· 𝑦) = 𝑦) |
| 27 | | id 22 |
. . . . . . . 8
⊢ (𝑦 ∈ {-1, 1} → 𝑦 ∈ {-1,
1}) |
| 28 | 26, 27 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝑦 ∈ {-1, 1} → (1
· 𝑦) ∈ {-1,
1}) |
| 29 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 · 𝑦) = (1 · 𝑦)) |
| 30 | 29 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑥 · 𝑦) ∈ {-1, 1} ↔ (1 · 𝑦) ∈ {-1,
1})) |
| 31 | 28, 30 | imbitrrid 246 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
| 32 | 25, 31 | jaoi 858 |
. . . . 5
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
| 33 | 8, 32 | syl 17 |
. . . 4
⊢ (𝑥 ∈ {-1, 1} → (𝑦 ∈ {-1, 1} → (𝑥 · 𝑦) ∈ {-1, 1})) |
| 34 | 33 | imp 406 |
. . 3
⊢ ((𝑥 ∈ {-1, 1} ∧ 𝑦 ∈ {-1, 1}) → (𝑥 · 𝑦) ∈ {-1, 1}) |
| 35 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = -1 → (1 / 𝑥) = (1 / -1)) |
| 36 | | ax-1ne0 11224 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
| 37 | | divneg2 11991 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 /
-1)) |
| 38 | 5, 5, 36, 37 | mp3an 1463 |
. . . . . . . . 9
⊢ -(1 / 1)
= (1 / -1) |
| 39 | | 1div1e1 11958 |
. . . . . . . . . 10
⊢ (1 / 1) =
1 |
| 40 | 39 | negeqi 11501 |
. . . . . . . . 9
⊢ -(1 / 1)
= -1 |
| 41 | 38, 40 | eqtr3i 2767 |
. . . . . . . 8
⊢ (1 / -1)
= -1 |
| 42 | 41, 2 | eqeltri 2837 |
. . . . . . 7
⊢ (1 / -1)
∈ {-1, 1} |
| 43 | 35, 42 | eqeltrdi 2849 |
. . . . . 6
⊢ (𝑥 = -1 → (1 / 𝑥) ∈ {-1,
1}) |
| 44 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 1 → (1 / 𝑥) = (1 / 1)) |
| 45 | 39, 15 | eqeltri 2837 |
. . . . . . 7
⊢ (1 / 1)
∈ {-1, 1} |
| 46 | 44, 45 | eqeltrdi 2849 |
. . . . . 6
⊢ (𝑥 = 1 → (1 / 𝑥) ∈ {-1,
1}) |
| 47 | 43, 46 | jaoi 858 |
. . . . 5
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (1 / 𝑥) ∈ {-1, 1}) |
| 48 | 8, 47 | syl 17 |
. . . 4
⊢ (𝑥 ∈ {-1, 1} → (1 /
𝑥) ∈ {-1,
1}) |
| 49 | 48 | adantr 480 |
. . 3
⊢ ((𝑥 ∈ {-1, 1} ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ {-1,
1}) |
| 50 | 7, 34, 15, 49 | expcl2lem 14114 |
. 2
⊢ ((-1
∈ {-1, 1} ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ {-1,
1}) |
| 51 | 2, 3, 50 | mp3an12 1453 |
1
⊢ (𝑁 ∈ ℤ →
(-1↑𝑁) ∈ {-1,
1}) |