Theorem rmynn0

Description: rmY is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Assertion	rmynn0	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
3	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}N\in \mathbb{Z}$$
4	1 3	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}N\in \mathbb{Z}$$
5		rmxypos	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to \left(0<A{X}_{\mathrm{rm}}N\wedge 0\le A{Y}_{\mathrm{rm}}N\right)$$
6	5	simprd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to 0\le A{Y}_{\mathrm{rm}}N$$
7		elnn0z	$$⊢A{Y}_{\mathrm{rm}}N\in {\mathbb{N}}_0\leftrightarrow \left(A{Y}_{\mathrm{rm}}N\in \mathbb{Z}\wedge 0\le A{Y}_{\mathrm{rm}}N\right)$$
8	4 6 7	sylanbrc	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}N\in {\mathbb{N}}_0$$