Metamath Proof Explorer

Theorem nndivdvdsd

Description: A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds . (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	nndivdvdsd.1	$⊢ φ \to M \in ℕ$
	nndivdvdsd.2	$⊢ φ \to N \in ℕ$
Assertion	nndivdvdsd	$⊢ φ \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℕ)$

Proof

Step	Hyp	Ref	Expression
1		nndivdvdsd.1	$⊢ φ \to M \in ℕ$
2		nndivdvdsd.2	$⊢ φ \to N \in ℕ$
3		nndivdvds	$⊢ (N \in ℕ \land M \in ℕ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℕ)$
4	2 1 3	syl2anc	$⊢ φ \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℕ)$