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