Theorem rmx0

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

	Ref	Expression
Assertion	rmx0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		rmxy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 0 ) = 1 ∧ ( 𝐴 Yrm 0 ) = 0 ) )
2	1	simpld	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 0 ) = 1 )