Theorem rmyadd

Description: Addition formula for Y sequence. Equation 2.8 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		rmxyadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
2	1	simprd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )