rmxluc

Description: The X sequence is a Lucas (second-order integer recurrence) sequence. Part 3 of equation 2.11 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
3	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A X_{rm} (N - 1) \in ℕ_{0}$
4	3	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A X_{rm} (N - 1) \in ℂ$
5	1 4	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N - 1) \in ℂ$
6		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
7	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A X_{rm} (N + 1) \in ℕ_{0}$
8	7	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A X_{rm} (N + 1) \in ℂ$
9	6 8	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + 1) \in ℂ$
10	5 9	addcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} (N - 1)) + (A X_{rm} (N + 1)) = (A X_{rm} (N + 1)) + (A X_{rm} (N - 1))$
11		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)$
12		rmxm1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N - 1) = A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)$
13	11 12	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} (N + 1)) + (A X_{rm} (N - 1)) = (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N) + (A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N))$
14	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
15	14	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
16		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
17	16	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A \in ℂ$
18	15 17	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A \in ℂ$
19		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
20	19	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
21	20	nncnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
22	21	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A^{2} - 1 \in ℂ$
23		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
24	23	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
25	24	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
26	22 25	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} N) \in ℂ$
27	17 15	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A (A X_{rm} N) \in ℂ$
28	18 26 27	ppncand	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N) + (A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)) = (A X_{rm} N) A + A (A X_{rm} N)$
29	15 17	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A = A (A X_{rm} N)$
30	29	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A + A (A X_{rm} N) = A (A X_{rm} N) + A (A X_{rm} N)$
31		2cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 \in ℂ$
32	31 17 15	mulassd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A (A X_{rm} N) = 2 A (A X_{rm} N)$
33	27	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A (A X_{rm} N) = A (A X_{rm} N) + A (A X_{rm} N)$
34	32 33	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A (A X_{rm} N) + A (A X_{rm} N) = 2 A (A X_{rm} N)$
35	28 30 34	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A + (A^{2} - 1) (A Y_{rm} N) + (A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)) = 2 A (A X_{rm} N)$
36	10 13 35	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} (N - 1)) + (A X_{rm} (N + 1)) = 2 A (A X_{rm} N)$
37		2cn	$⊢ 2 \in ℂ$
38		mulcl	$⊢ (2 \in ℂ \land A \in ℂ) \to 2 A \in ℂ$
39	37 17 38	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A \in ℂ$
40	39 15	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A (A X_{rm} N) \in ℂ$
41	40 5 9	subaddd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (2 A (A X_{rm} N) - (A X_{rm} (N - 1)) = A X_{rm} (N + 1) \leftrightarrow (A X_{rm} (N - 1)) + (A X_{rm} (N + 1)) = 2 A (A X_{rm} N))$
42	36 41	mpbird	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 A (A X_{rm} N) - (A X_{rm} (N - 1)) = A X_{rm} (N + 1)$
43	42	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + 1) = 2 A (A X_{rm} N) - (A X_{rm} (N - 1))$

Metamath Proof Explorer

Theorem rmxluc

Proof