Metamath Proof Explorer

Theorem 1dvds

Description: 1 divides any integer. Theorem 1.1(f) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion 1dvds ⊢ N ∈ ℤ → 1 ∥ N

Proof

Step Hyp Ref Expression
1 zcn ⊢ N ∈ ℤ → N ∈ ℂ
2 1 mulridd ⊢ N ∈ ℤ → N ⋅ 1 = N
3 1z ⊢ 1 ∈ ℤ
4 dvds0lem ⊢ N ∈ ℤ ∧ 1 ∈ ℤ ∧ N ∈ ℤ ∧ N ⋅ 1 = N → 1 ∥ N
5 3 4 mp3anl2 ⊢ N ∈ ℤ ∧ N ∈ ℤ ∧ N ⋅ 1 = N → 1 ∥ N
6 5 anabsan ⊢ N ∈ ℤ ∧ N ⋅ 1 = N → 1 ∥ N
7 2 6 mpdan ⊢ N ∈ ℤ → 1 ∥ N