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

Proof

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