Step |
Hyp |
Ref |
Expression |
1 |
|
m1expcl |
⊢ ( 𝑋 ∈ ℤ → ( - 1 ↑ 𝑋 ) ∈ ℤ ) |
2 |
1
|
zcnd |
⊢ ( 𝑋 ∈ ℤ → ( - 1 ↑ 𝑋 ) ∈ ℂ ) |
3 |
2
|
adantr |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ 𝑋 ) ∈ ℂ ) |
4 |
|
m1expcl |
⊢ ( 𝑌 ∈ ℤ → ( - 1 ↑ 𝑌 ) ∈ ℤ ) |
5 |
4
|
zcnd |
⊢ ( 𝑌 ∈ ℤ → ( - 1 ↑ 𝑌 ) ∈ ℂ ) |
6 |
5
|
adantl |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ 𝑌 ) ∈ ℂ ) |
7 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
8 |
|
neg1ne0 |
⊢ - 1 ≠ 0 |
9 |
|
expne0i |
⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ 𝑌 ) ≠ 0 ) |
10 |
7 8 9
|
mp3an12 |
⊢ ( 𝑌 ∈ ℤ → ( - 1 ↑ 𝑌 ) ≠ 0 ) |
11 |
10
|
adantl |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ 𝑌 ) ≠ 0 ) |
12 |
3 6 11
|
divrecd |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( - 1 ↑ 𝑋 ) / ( - 1 ↑ 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) · ( 1 / ( - 1 ↑ 𝑌 ) ) ) ) |
13 |
|
m1expcl2 |
⊢ ( 𝑌 ∈ ℤ → ( - 1 ↑ 𝑌 ) ∈ { - 1 , 1 } ) |
14 |
|
elpri |
⊢ ( ( - 1 ↑ 𝑌 ) ∈ { - 1 , 1 } → ( ( - 1 ↑ 𝑌 ) = - 1 ∨ ( - 1 ↑ 𝑌 ) = 1 ) ) |
15 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
16 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
17 |
|
divneg2 |
⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) ) |
18 |
15 15 16 17
|
mp3an |
⊢ - ( 1 / 1 ) = ( 1 / - 1 ) |
19 |
|
1div1e1 |
⊢ ( 1 / 1 ) = 1 |
20 |
19
|
negeqi |
⊢ - ( 1 / 1 ) = - 1 |
21 |
18 20
|
eqtr3i |
⊢ ( 1 / - 1 ) = - 1 |
22 |
|
oveq2 |
⊢ ( ( - 1 ↑ 𝑌 ) = - 1 → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( 1 / - 1 ) ) |
23 |
|
id |
⊢ ( ( - 1 ↑ 𝑌 ) = - 1 → ( - 1 ↑ 𝑌 ) = - 1 ) |
24 |
21 22 23
|
3eqtr4a |
⊢ ( ( - 1 ↑ 𝑌 ) = - 1 → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( - 1 ↑ 𝑌 ) ) |
25 |
|
oveq2 |
⊢ ( ( - 1 ↑ 𝑌 ) = 1 → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( 1 / 1 ) ) |
26 |
|
id |
⊢ ( ( - 1 ↑ 𝑌 ) = 1 → ( - 1 ↑ 𝑌 ) = 1 ) |
27 |
19 25 26
|
3eqtr4a |
⊢ ( ( - 1 ↑ 𝑌 ) = 1 → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( - 1 ↑ 𝑌 ) ) |
28 |
24 27
|
jaoi |
⊢ ( ( ( - 1 ↑ 𝑌 ) = - 1 ∨ ( - 1 ↑ 𝑌 ) = 1 ) → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( - 1 ↑ 𝑌 ) ) |
29 |
13 14 28
|
3syl |
⊢ ( 𝑌 ∈ ℤ → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( - 1 ↑ 𝑌 ) ) |
30 |
29
|
adantl |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 1 / ( - 1 ↑ 𝑌 ) ) = ( - 1 ↑ 𝑌 ) ) |
31 |
30
|
oveq2d |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( - 1 ↑ 𝑋 ) · ( 1 / ( - 1 ↑ 𝑌 ) ) ) = ( ( - 1 ↑ 𝑋 ) · ( - 1 ↑ 𝑌 ) ) ) |
32 |
12 31
|
eqtrd |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( - 1 ↑ 𝑋 ) / ( - 1 ↑ 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) · ( - 1 ↑ 𝑌 ) ) ) |
33 |
|
expsub |
⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( - 1 ↑ ( 𝑋 − 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) / ( - 1 ↑ 𝑌 ) ) ) |
34 |
7 8 33
|
mpanl12 |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ ( 𝑋 − 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) / ( - 1 ↑ 𝑌 ) ) ) |
35 |
|
expaddz |
⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( - 1 ↑ ( 𝑋 + 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) · ( - 1 ↑ 𝑌 ) ) ) |
36 |
7 8 35
|
mpanl12 |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ ( 𝑋 + 𝑌 ) ) = ( ( - 1 ↑ 𝑋 ) · ( - 1 ↑ 𝑌 ) ) ) |
37 |
32 34 36
|
3eqtr4d |
⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ ( 𝑋 − 𝑌 ) ) = ( - 1 ↑ ( 𝑋 + 𝑌 ) ) ) |