Metamath Proof Explorer
Description: Value of X sequence at 0. Part 1 of equation 2.11 of JonesMatijasevic
p. 695. (Contributed by Stefan O'Rear, 22Sep2014)


Ref 
Expression 

Assertion 
rmx0 
⊢ ( 𝐴 ∈ ( ℤ_{≥} ‘ 2 ) → ( 𝐴 X_{rm} 0 ) = 1 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

rmxy0 
⊢ ( 𝐴 ∈ ( ℤ_{≥} ‘ 2 ) → ( ( 𝐴 X_{rm} 0 ) = 1 ∧ ( 𝐴 Y_{rm} 0 ) = 0 ) ) 
2 
1

simpld 
⊢ ( 𝐴 ∈ ( ℤ_{≥} ‘ 2 ) → ( 𝐴 X_{rm} 0 ) = 1 ) 