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 e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ ( X - Y ) ) = ( -u 1 ^ ( X + Y ) ) )

Proof

Step Hyp Ref Expression
1 m1expcl 
 |-  ( X e. ZZ -> ( -u 1 ^ X ) e. ZZ )
2 1 zcnd 
 |-  ( X e. ZZ -> ( -u 1 ^ X ) e. CC )
3 2 adantr 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ X ) e. CC )
4 m1expcl 
 |-  ( Y e. ZZ -> ( -u 1 ^ Y ) e. ZZ )
5 4 zcnd 
 |-  ( Y e. ZZ -> ( -u 1 ^ Y ) e. CC )
6 5 adantl 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ Y ) e. CC )
7 neg1cn 
 |-  -u 1 e. CC
8 neg1ne0 
 |-  -u 1 =/= 0
9 expne0i 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ Y e. ZZ ) -> ( -u 1 ^ Y ) =/= 0 )
10 7 8 9 mp3an12 
 |-  ( Y e. ZZ -> ( -u 1 ^ Y ) =/= 0 )
11 10 adantl 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ Y ) =/= 0 )
12 3 6 11 divrecd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( -u 1 ^ X ) / ( -u 1 ^ Y ) ) = ( ( -u 1 ^ X ) x. ( 1 / ( -u 1 ^ Y ) ) ) )
13 m1expcl2 
 |-  ( Y e. ZZ -> ( -u 1 ^ Y ) e. { -u 1 , 1 } )
14 elpri 
 |-  ( ( -u 1 ^ Y ) e. { -u 1 , 1 } -> ( ( -u 1 ^ Y ) = -u 1 \/ ( -u 1 ^ Y ) = 1 ) )
15 ax-1cn 
 |-  1 e. CC
16 ax-1ne0 
 |-  1 =/= 0
17 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
18 15 15 16 17 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
19 1div1e1 
 |-  ( 1 / 1 ) = 1
20 19 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
21 18 20 eqtr3i 
 |-  ( 1 / -u 1 ) = -u 1
22 oveq2 
 |-  ( ( -u 1 ^ Y ) = -u 1 -> ( 1 / ( -u 1 ^ Y ) ) = ( 1 / -u 1 ) )
23 id 
 |-  ( ( -u 1 ^ Y ) = -u 1 -> ( -u 1 ^ Y ) = -u 1 )
24 21 22 23 3eqtr4a 
 |-  ( ( -u 1 ^ Y ) = -u 1 -> ( 1 / ( -u 1 ^ Y ) ) = ( -u 1 ^ Y ) )
25 oveq2 
 |-  ( ( -u 1 ^ Y ) = 1 -> ( 1 / ( -u 1 ^ Y ) ) = ( 1 / 1 ) )
26 id 
 |-  ( ( -u 1 ^ Y ) = 1 -> ( -u 1 ^ Y ) = 1 )
27 19 25 26 3eqtr4a 
 |-  ( ( -u 1 ^ Y ) = 1 -> ( 1 / ( -u 1 ^ Y ) ) = ( -u 1 ^ Y ) )
28 24 27 jaoi 
 |-  ( ( ( -u 1 ^ Y ) = -u 1 \/ ( -u 1 ^ Y ) = 1 ) -> ( 1 / ( -u 1 ^ Y ) ) = ( -u 1 ^ Y ) )
29 13 14 28 3syl 
 |-  ( Y e. ZZ -> ( 1 / ( -u 1 ^ Y ) ) = ( -u 1 ^ Y ) )
30 29 adantl 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( 1 / ( -u 1 ^ Y ) ) = ( -u 1 ^ Y ) )
31 30 oveq2d 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( -u 1 ^ X ) x. ( 1 / ( -u 1 ^ Y ) ) ) = ( ( -u 1 ^ X ) x. ( -u 1 ^ Y ) ) )
32 12 31 eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( -u 1 ^ X ) / ( -u 1 ^ Y ) ) = ( ( -u 1 ^ X ) x. ( -u 1 ^ Y ) ) )
33 expsub 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( -u 1 ^ ( X - Y ) ) = ( ( -u 1 ^ X ) / ( -u 1 ^ Y ) ) )
34 7 8 33 mpanl12 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ ( X - Y ) ) = ( ( -u 1 ^ X ) / ( -u 1 ^ Y ) ) )
35 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( -u 1 ^ ( X + Y ) ) = ( ( -u 1 ^ X ) x. ( -u 1 ^ Y ) ) )
36 7 8 35 mpanl12 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ ( X + Y ) ) = ( ( -u 1 ^ X ) x. ( -u 1 ^ Y ) ) )
37 32 34 36 3eqtr4d 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ ( X - Y ) ) = ( -u 1 ^ ( X + Y ) ) )