Metamath Proof Explorer


Theorem rmxneg

Description: Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg , rmxyadd , rmxy0 , and rmxy1 via qirropth results in two theorems at once, but typical use requires only one, so this group of theorems serves to separate the cases. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxneg
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u N ) = ( A rmX N ) )

Proof

Step Hyp Ref Expression
1 rmxyneg
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX -u N ) = ( A rmX N ) /\ ( A rmY -u N ) = -u ( A rmY N ) ) )
2 1 simpld
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u N ) = ( A rmX N ) )