Metamath Proof Explorer

Theorem m1expaddsub

Description: Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion m1expaddsub ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( - 1 ↑ ( 𝑋 − 𝑌 ) ) = ( - 1 ↑ ( 𝑋 + 𝑌 ) ) )

Proof

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 ↑ ( 𝑋 + 𝑌 ) ) )