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 ∈ ℕ ∧ B ∈ ℕ → ∃ x ∈ ℕ A ⁢ x = B ↔ B A ∈ ℕ

Proof

Step Hyp Ref Expression
1 risset ⊢ B A ∈ ℕ ↔ ∃ x ∈ ℕ x = B A
2 eqcom ⊢ x = B A ↔ B A = x
3 nncn ⊢ B ∈ ℕ → B ∈ ℂ
4 3 ad2antlr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → B ∈ ℂ
5 nncn ⊢ A ∈ ℕ → A ∈ ℂ
6 5 ad2antrr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → A ∈ ℂ
7 nncn ⊢ x ∈ ℕ → x ∈ ℂ
8 7 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → x ∈ ℂ
9 nnne0 ⊢ A ∈ ℕ → A ≠ 0
10 9 ad2antrr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → A ≠ 0
11 4 6 8 10 divmuld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → B A = x ↔ A ⁢ x = B
12 2 11 syl5bb ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ x ∈ ℕ → x = B A ↔ A ⁢ x = B
13 12 rexbidva ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ x ∈ ℕ x = B A ↔ ∃ x ∈ ℕ A ⁢ x = B
14 1 13 bitr2id ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ x ∈ ℕ A ⁢ x = B ↔ B A ∈ ℕ