Metamath Proof Explorer


Theorem rmyadd

Description: Addition formula for Y sequence. Equation 2.8 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmyadd A2MNAYrmM+N=AYrmMAXrmN+AXrmMAYrmN

Proof

Step Hyp Ref Expression
1 rmxyadd A2MNAXrmM+N=AXrmMAXrmN+A21AYrmMAYrmNAYrmM+N=AYrmMAXrmN+AXrmMAYrmN
2 1 simprd A2MNAYrmM+N=AYrmMAXrmN+AXrmMAYrmN