Theorem rmy1

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

	Ref	Expression
Assertion	rmy1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}1=1$$

Proof

Step	Hyp	Ref	Expression
1		rmxy1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A{X}_{\mathrm{rm}}1=A\wedge A{Y}_{\mathrm{rm}}1=1\right)$$
2	1	simprd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}1=1$$