Metamath Proof Explorer


Theorem rmx1

Description: Value of X sequence at 1. Part 2 of equation 2.11 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmx1 ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 rmxy1 ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 Xrm 1 ) = 𝐴 ∧ ( 𝐴 Yrm 1 ) = 1 ) )
2 1 simpld ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )