Metamath Proof Explorer

Theorem rmyp1

Description: Special addition of 1 formula for Y sequence. Part 2 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 24-Sep-2014)

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

Proof

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