Metamath Proof Explorer

Theorem rmyneg

Description: Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmyneg 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u N ) = -u ( A rmY 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 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u N ) = -u ( A rmY N ) )