rmyluc2

Description: Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014)

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

Step	Hyp	Ref	Expression
1		rmyluc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) = 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1))$
2		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
3	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
4	3	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
5		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
6	5	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A \in ℂ$
7	4 6	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A = A (A Y_{rm} N)$
8	7	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A = 2 A (A Y_{rm} N)$
9		2cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 \in ℂ$
10	9 6 4	mulassd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A (A Y_{rm} N) = 2 A (A Y_{rm} N)$
11	8 10	eqtr4d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A = 2 A (A Y_{rm} N)$
12	11	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1)) = 2 A (A Y_{rm} N) - (A Y_{rm} (N - 1))$
13	1 12	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) = 2 A (A Y_{rm} N) - (A Y_{rm} (N - 1))$

Metamath Proof Explorer