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 ⊢ N ∈ ℤ → 0 ∥ N ↔ N = 0

Proof

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