Theorem rmynn0

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

	Ref	Expression
Assertion	rmynn0	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY N ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( N e. NN0 -> N e. ZZ )
2		frmy	|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
3	2	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
4	1 3	sylan2	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY N ) e. ZZ )
5		rmxypos	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) )
6	5	simprd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 0 <_ ( A rmY N ) )
7		elnn0z	|- ( ( A rmY N ) e. NN0 <-> ( ( A rmY N ) e. ZZ /\ 0 <_ ( A rmY N ) ) )
8	4 6 7	sylanbrc	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY N ) e. NN0 )