Metamath Proof Explorer

Theorem rmxp1

Description: Special addition-of-1 formula for X sequence. Part 1 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014)

		Ref	Expression
	Assertion	rmxp1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + 1) = (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N)$

Proof

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		rmxadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land 1 \in ℤ) \to A X_{rm} (N + 1) = (A X_{rm} N) (A X_{rm} 1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} 1)$
3	1 2	mp3an3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + 1) = (A X_{rm} N) (A X_{rm} 1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} 1)$
4		rmx1	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} 1 = A$
5	4	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} 1 = A$
6	5	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} 1) = (A X_{rm} N) A$
7		rmy1	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 1 = 1$
8	7	oveq2d	$⊢ A \in ℤ_{\geq 2} \to (A Y_{rm} N) (A Y_{rm} 1) = (A Y_{rm} N) \cdot 1$
9	8	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A Y_{rm} 1) = (A Y_{rm} N) \cdot 1$
10		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
11	10	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
12	11	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
13	12	mulid1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) \cdot 1 = A Y_{rm} N$
14	9 13	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A Y_{rm} 1) = A Y_{rm} N$
15	14	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} 1) = (A^{2} - 1) (A Y_{rm} N)$
16	6 15	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} 1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} 1) = (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N)$
17	3 16	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + 1) = (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N)$