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	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)$

Step	Hyp	Ref	Expression
1		rmxyadd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} (M + N) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \land A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
2	1	simprd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)$