Theorem rmynn

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

	Ref	Expression
Assertion	rmynn	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
3	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
5		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
6	5	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) = 0 )
7		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
8	7	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
9		simpl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
10		0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℤ )
11	1	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
12		ltrmy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
13	9 10 11 12	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
14	8 13	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) )
15	6 14	eqbrtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Yrm 𝑁 ) )
16		elnnz	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ ↔ ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 0 < ( 𝐴 Yrm 𝑁 ) ) )
17	4 15 16	sylanbrc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ )