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 ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − Y = − 1 X + Y

Proof

Step Hyp Ref Expression
1 m1expcl ⊢ X ∈ ℤ → − 1 X ∈ ℤ
2 1 zcnd ⊢ X ∈ ℤ → − 1 X ∈ ℂ
3 2 adantr ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X ∈ ℂ
4 m1expcl ⊢ Y ∈ ℤ → − 1 Y ∈ ℤ
5 4 zcnd ⊢ Y ∈ ℤ → − 1 Y ∈ ℂ
6 5 adantl ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 Y ∈ ℂ
7 neg1cn ⊢ − 1 ∈ ℂ
8 neg1ne0 ⊢ − 1 ≠ 0
9 expne0i ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ Y ∈ ℤ → − 1 Y ≠ 0
10 7 8 9 mp3an12 ⊢ Y ∈ ℤ → − 1 Y ≠ 0
11 10 adantl ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 Y ≠ 0
12 3 6 11 divrecd ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − 1 Y = − 1 X ⁢ 1 − 1 Y
13 m1expcl2 ⊢ Y ∈ ℤ → − 1 Y ∈ − 1 1
14 elpri ⊢ − 1 Y ∈ − 1 1 → − 1 Y = − 1 ∨ − 1 Y = 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 Y = − 1 → 1 − 1 Y = 1 − 1
23 id ⊢ − 1 Y = − 1 → − 1 Y = − 1
24 21 22 23 3eqtr4a ⊢ − 1 Y = − 1 → 1 − 1 Y = − 1 Y
25 oveq2 ⊢ − 1 Y = 1 → 1 − 1 Y = 1 1
26 id ⊢ − 1 Y = 1 → − 1 Y = 1
27 19 25 26 3eqtr4a ⊢ − 1 Y = 1 → 1 − 1 Y = − 1 Y
28 24 27 jaoi ⊢ − 1 Y = − 1 ∨ − 1 Y = 1 → 1 − 1 Y = − 1 Y
29 13 14 28 3syl ⊢ Y ∈ ℤ → 1 − 1 Y = − 1 Y
30 29 adantl ⊢ X ∈ ℤ ∧ Y ∈ ℤ → 1 − 1 Y = − 1 Y
31 30 oveq2d ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X ⁢ 1 − 1 Y = − 1 X ⁢ − 1 Y
32 12 31 eqtrd ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − 1 Y = − 1 X ⁢ − 1 Y
33 expsub ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − Y = − 1 X − 1 Y
34 7 8 33 mpanl12 ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − Y = − 1 X − 1 Y
35 expaddz ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X + Y = − 1 X ⁢ − 1 Y
36 7 8 35 mpanl12 ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X + Y = − 1 X ⁢ − 1 Y
37 32 34 36 3eqtr4d ⊢ X ∈ ℤ ∧ Y ∈ ℤ → − 1 X − Y = − 1 X + Y