Metamath Proof Explorer


Theorem rmxadd

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

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

Proof

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