Theorem rmyp1

Description: Special addition of 1 formula for Y sequence. Part 2 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 24-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		rmyadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) )
4		rmx1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )
5	4	oveq2d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) )
7		rmy1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
8	7	oveq2d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · 1 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · 1 ) )
10		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
11	10	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
12	11	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
13	12	mulid1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · 1 ) = ( 𝐴 Xrm 𝑁 ) )
14	9 13	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( 𝐴 Xrm 𝑁 ) )
15	6 14	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( 𝐴 Xrm 𝑁 ) ) )
16	3 15	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( 𝐴 Xrm 𝑁 ) ) )