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