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