Theorem rmyneg

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

	Ref	Expression
Assertion	rmyneg	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}\mathrm{-<mi\; mathcolor="\#808">N</mi>}=-\left(A{Y}_{\mathrm{rm}}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		rmxyneg	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to \left(A{X}_{\mathrm{rm}}\mathrm{-<mi\; mathcolor="\#808">N</mi>}=A{X}_{\mathrm{rm}}N\wedge A{Y}_{\mathrm{rm}}\mathrm{-<mi\; mathcolor="\#808">N</mi>}=-\left(A{Y}_{\mathrm{rm}}N\right)\right)$$
2	1	simprd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}\mathrm{-<mi\; mathcolor="\#808">N</mi>}=-\left(A{Y}_{\mathrm{rm}}N\right)$$