Theorem rmxp1

Description: Special addition-of-1 formula for X sequence. Part 1 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014)

	Ref	Expression
Assertion	rmxp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		rmxadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) )
4		rmx1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )
5	4	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 1 ) = 𝐴 )
6	5	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) )
7		rmy1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
8	7	oveq2d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 1 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 1 ) )
10		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
11	10	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
12	11	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
13	12	mulridd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 1 ) = ( 𝐴 Yrm 𝑁 ) )
14	9 13	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( 𝐴 Yrm 𝑁 ) )
15	14	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) )
16	6 15	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
17	3 16	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )