Metamath Proof Explorer

Theorem nndiv

Description: Two ways to express " A divides B " for positive integers. (Contributed by NM, 3-Feb-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

		Ref	Expression
	Assertion	nndiv	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists x \in ℕ A x = B \leftrightarrow \frac{B}{A} \in ℕ)$

Proof

Step	Hyp	Ref	Expression
1		risset	$⊢ \frac{B}{A} \in ℕ \leftrightarrow \exists x \in ℕ x = \frac{B}{A}$
2		eqcom	$⊢ x = \frac{B}{A} \leftrightarrow \frac{B}{A} = x$
3		nncn	$⊢ B \in ℕ \to B \in ℂ$
4	3	ad2antlr	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to B \in ℂ$
5		nncn	$⊢ A \in ℕ \to A \in ℂ$
6	5	ad2antrr	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to A \in ℂ$
7		nncn	$⊢ x \in ℕ \to x \in ℂ$
8	7	adantl	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to x \in ℂ$
9		nnne0	$⊢ A \in ℕ \to A \neq 0$
10	9	ad2antrr	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to A \neq 0$
11	4 6 8 10	divmuld	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to (\frac{B}{A} = x \leftrightarrow A x = B)$
12	2 11	bitrid	$⊢ ((A \in ℕ \land B \in ℕ) \land x \in ℕ) \to (x = \frac{B}{A} \leftrightarrow A x = B)$
13	12	rexbidva	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists x \in ℕ x = \frac{B}{A} \leftrightarrow \exists x \in ℕ A x = B)$
14	1 13	bitr2id	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists x \in ℕ A x = B \leftrightarrow \frac{B}{A} \in ℕ)$