Theorem rmynn

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

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

Proof

Step	Hyp	Ref	Expression
1		nnz	|- ( N e. NN -> 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. NN ) -> ( A rmY N ) e. ZZ )
5		rmy0	|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
6	5	adantr	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) = 0 )
7		nngt0	|- ( N e. NN -> 0 < N )
8	7	adantl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < N )
9		simpl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. ( ZZ>= ` 2 ) )
10		0zd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 e. ZZ )
11	1	adantl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )
12		ltrmy	|- ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ N e. ZZ ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
13	9 10 11 12	syl3anc	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
14	8 13	mpbid	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) < ( A rmY N ) )
15	6 14	eqbrtrrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( A rmY N ) )
16		elnnz	|- ( ( A rmY N ) e. NN <-> ( ( A rmY N ) e. ZZ /\ 0 < ( A rmY N ) ) )
17	4 15 16	sylanbrc	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. NN )