Theorem 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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) − ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
2		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
3	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℕ0 )
4	3	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℂ )
5	1 4	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℂ )
6		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
7	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) ∈ ℕ0 )
8	7	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) ∈ ℂ )
9	6 8	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) ∈ ℂ )
10	5 9	addcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑁 − 1 ) ) + ( 𝐴 Xrm ( 𝑁 + 1 ) ) ) = ( ( 𝐴 Xrm ( 𝑁 + 1 ) ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
11		rmxp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
12		rmxm1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
13	11 12	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑁 + 1 ) ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) = ( ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
14	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
15	14	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
16		eluzelcn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
17	16	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
18	15 17	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) ∈ ℂ )
19		rmspecnonsq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
20	19	eldifad	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
21	20	nncnd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
22	21	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
23		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
24	23	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
25	24	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
26	22 25	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
27	17 15	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ∈ ℂ )
28	18 26 27	ppncand	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) )
29	15 17	mulcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) )
30	29	oveq1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) )
31		2cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 2 ∈ ℂ )
32	31 17 15	mulassd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) = ( 2 · ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) )
33	27	2timesd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) )
34	32 33	eqtr2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) )
35	28 30 34	3eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) )
36	10 13 35	3eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑁 − 1 ) ) + ( 𝐴 Xrm ( 𝑁 + 1 ) ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) )
37		2cn	⊢ 2 ∈ ℂ
38		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
39	37 17 38	sylancr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝐴 ) ∈ ℂ )
40	39 15	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℂ )
41	40 5 9	subaddd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) − ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Xrm ( 𝑁 + 1 ) ) ↔ ( ( 𝐴 Xrm ( 𝑁 − 1 ) ) + ( 𝐴 Xrm ( 𝑁 + 1 ) ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) ) )
42	36 41	mpbird	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) − ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Xrm ( 𝑁 + 1 ) ) )
43	42	eqcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Xrm 𝑁 ) ) − ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )