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 
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )

Proof

Step Hyp Ref Expression
1 rmxy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) )
2 1 simpld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )