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