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 ) )