Metamath Proof Explorer

Theorem rmxadd

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

		Ref	Expression
	Assertion	rmxadd	$⊢ (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)$

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	simpld	$⊢ (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)$