# 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 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{x}={B}↔\frac{{B}}{{A}}\in ℕ\right)$

### Proof

Step Hyp Ref Expression
1 risset ${⊢}\frac{{B}}{{A}}\in ℕ↔\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}{x}=\frac{{B}}{{A}}$
2 eqcom ${⊢}{x}=\frac{{B}}{{A}}↔\frac{{B}}{{A}}={x}$
3 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
4 3 ad2antlr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to {B}\in ℂ$
5 nncn ${⊢}{A}\in ℕ\to {A}\in ℂ$
6 5 ad2antrr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to {A}\in ℂ$
7 nncn ${⊢}{x}\in ℕ\to {x}\in ℂ$
8 7 adantl ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to {x}\in ℂ$
9 nnne0 ${⊢}{A}\in ℕ\to {A}\ne 0$
10 9 ad2antrr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to {A}\ne 0$
11 4 6 8 10 divmuld ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to \left(\frac{{B}}{{A}}={x}↔{A}{x}={B}\right)$
12 2 11 syl5bb ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge {x}\in ℕ\right)\to \left({x}=\frac{{B}}{{A}}↔{A}{x}={B}\right)$
13 12 rexbidva ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}{x}=\frac{{B}}{{A}}↔\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{x}={B}\right)$
14 1 13 syl5rbb ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{x}={B}↔\frac{{B}}{{A}}\in ℕ\right)$