Metamath Proof Explorer
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 ) = 𝐴 ) |