Metamath Proof Explorer

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 𝑁 ) ) ) )