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

Metamath Proof Explorer

Theorem 0dvds

Description: Only 0 is divisible by 0. Theorem 1.1(h) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion 0dvds ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 divides ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 ) )
3 1 2 mpan ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 ) )
4 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
5 4 mul01d ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 0 ) = 0 )
6 eqtr2 ⊢ ( ( ( 𝑛 · 0 ) = 𝑁 ∧ ( 𝑛 · 0 ) = 0 ) → 𝑁 = 0 )
7 5 6 sylan2 ⊢ ( ( ( 𝑛 · 0 ) = 𝑁 ∧ 𝑛 ∈ ℤ ) → 𝑁 = 0 )
8 7 ancoms ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 0 ) = 𝑁 ) → 𝑁 = 0 )
9 8 rexlimiva ⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 → 𝑁 = 0 )
10 3 9 biimtrdi ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 → 𝑁 = 0 ) )
11 dvds0 ⊢ ( 0 ∈ ℤ → 0 ∥ 0 )
12 1 11 ax-mp ⊢ 0 ∥ 0
13 breq2 ⊢ ( 𝑁 = 0 → ( 0 ∥ 𝑁 ↔ 0 ∥ 0 ) )
14 12 13 mpbiri ⊢ ( 𝑁 = 0 → 0 ∥ 𝑁 )
15 10 14 impbid1 ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )