This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) = 𝐵 ↔ ( 𝐵 / 𝐴 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 risset ⊢ ( ( 𝐵 / 𝐴 ) ∈ ℕ ↔ ∃ 𝑥 ∈ ℕ 𝑥 = ( 𝐵 / 𝐴 ) )
2 eqcom ⊢ ( 𝑥 = ( 𝐵 / 𝐴 ) ↔ ( 𝐵 / 𝐴 ) = 𝑥 )
3 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
4 3 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → 𝐵 ∈ ℂ )
5 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → 𝐴 ∈ ℂ )
7 nncn ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
8 7 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℂ )
9 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
10 9 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → 𝐴 ≠ 0 )
11 4 6 8 10 divmuld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐵 / 𝐴 ) = 𝑥 ↔ ( 𝐴 · 𝑥 ) = 𝐵 ) )
12 2 11 bitrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 = ( 𝐵 / 𝐴 ) ↔ ( 𝐴 · 𝑥 ) = 𝐵 ) )
13 12 rexbidva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℕ 𝑥 = ( 𝐵 / 𝐴 ) ↔ ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) = 𝐵 ) )
14 1 13 bitr2id ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) = 𝐵 ↔ ( 𝐵 / 𝐴 ) ∈ ℕ ) )