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 2 N A X rm -N = A X rm N


Step Hyp Ref Expression
1 rmxyneg A 2 N A X rm -N = A X rm N A Y rm -N = A Y rm N
2 1 simpld A 2 N A X rm -N = A X rm N