rmyluc

Description: The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 and rmy1 . Part 3 of equation 2.12 of JonesMatijasevic p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain ( ZZ X. ZZ ) , which simplifies some later theorems. It may shorten the derivation to use this as our initial definition. Incidentally, the X sequence satisfies the exact same recurrence. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
2		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
3	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A Y_{rm} (N + 1) \in ℤ$
4	1 3	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) \in ℤ$
5	4	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) \in ℂ$
6		2cn	$⊢ 2 \in ℂ$
7	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
8	7	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
9		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
10	9	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A \in ℂ$
11	8 10	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A \in ℂ$
12		mulcl	$⊢ (2 \in ℂ \land (A Y_{rm} N) A \in ℂ) \to 2 (A Y_{rm} N) A \in ℂ$
13	6 11 12	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A \in ℂ$
14		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
15	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A Y_{rm} (N - 1) \in ℤ$
16	14 15	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) \in ℤ$
17	16	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) \in ℂ$
18	13 17	subcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1)) \in ℂ$
19		rmyp1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) = (A Y_{rm} N) A + (A X_{rm} N)$
20		rmym1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) = (A Y_{rm} N) A - (A X_{rm} N)$
21	19 20	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} (N + 1)) + (A Y_{rm} (N - 1)) = (A Y_{rm} N) A + (A X_{rm} N) + ((A Y_{rm} N) A - (A X_{rm} N))$
22		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
23	22	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
24	23	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
25	11 24 11	ppncand	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A + (A X_{rm} N) + ((A Y_{rm} N) A - (A X_{rm} N)) = (A Y_{rm} N) A + (A Y_{rm} N) A$
26	13 17	npcand	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1)) = 2 (A Y_{rm} N) A$
27	11	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A Y_{rm} N) A = (A Y_{rm} N) A + (A Y_{rm} N) A$
28	26 27	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A + (A Y_{rm} N) A = 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1))$
29	21 25 28	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} (N + 1)) + (A Y_{rm} (N - 1)) = 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1))$
30	5 18 17 29	addcan2ad	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + 1) = 2 (A Y_{rm} N) A - (A Y_{rm} (N - 1))$

Metamath Proof Explorer

Theorem rmyluc

Proof