Theorem rmynn0

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
2		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
3	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
5		rmxypos	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) )
6	5	simprd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ ( 𝐴 Yrm 𝑁 ) )
7		elnn0z	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 ↔ ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) )
8	4 6 7	sylanbrc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 )