Metamath Proof Explorer

Theorem rmy0

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

Ref Expression
Assertion rmy0 
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )

Proof

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