rmynn

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

		Ref	Expression
	Assertion	rmynn	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℕ$

Step	Hyp	Ref	Expression
1		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
3	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
4	1 3	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℤ$
5		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
6	5	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 = 0$
7		nngt0	$⊢ N \in ℕ \to 0 < N$
8	7	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < N$
9		simpl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℤ_{\geq 2}$
10		0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 \in ℤ$
11	1	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℤ$
12		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land N \in ℤ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
13	9 10 11 12	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
14	8 13	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 < A Y_{rm} N$
15	6 14	eqbrtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < A Y_{rm} N$
16		elnnz	$⊢ A Y_{rm} N \in ℕ \leftrightarrow (A Y_{rm} N \in ℤ \land 0 < A Y_{rm} N)$
17	4 15 16	sylanbrc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℕ$

Metamath Proof Explorer