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

Metamath Proof Explorer

Theorem ex-dvds

Description: Example for df-dvds : 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015)

Ref Expression
Assertion ex-dvds 3 ∥ 6

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 3z ⊢ 3 ∈ ℤ
3 6nn ⊢ 6 ∈ ℕ
4 3 nnzi ⊢ 6 ∈ ℤ
5 1 2 4 3pm3.2i ⊢ ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 6 ∈ ℤ )
6 3cn ⊢ 3 ∈ ℂ
7 6 2timesi ⊢ ( 2 · 3 ) = ( 3 + 3 )
8 3p3e6 ⊢ ( 3 + 3 ) = 6
9 7 8 eqtri ⊢ ( 2 · 3 ) = 6
10 dvds0lem ⊢ ( ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 6 ∈ ℤ ) ∧ ( 2 · 3 ) = 6 ) → 3 ∥ 6 )
11 5 9 10 mp2an ⊢ 3 ∥ 6