dvdstr

Description: The divides relation is transitive. Theorem 1.1(b) in ApostolNT p. 14 (transitive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	dvdstr	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land M ∥ N) \to K ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land M \in ℤ)$
2		3simpc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \in ℤ \land N \in ℤ)$
3		3simpb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land N \in ℤ)$
4		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
5	4	adantl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
6		oveq2	$⊢ x K = M \to y x K = y \cdot M$
7	6	adantr	$⊢ (x K = M \land y \cdot M = N) \to y x K = y \cdot M$
8		eqeq2	$⊢ y \cdot M = N \to (y x K = y \cdot M \leftrightarrow y x K = N)$
9	8	adantl	$⊢ (x K = M \land y \cdot M = N) \to (y x K = y \cdot M \leftrightarrow y x K = N)$
10	7 9	mpbid	$⊢ (x K = M \land y \cdot M = N) \to y x K = N$
11		zcn	$⊢ x \in ℤ \to x \in ℂ$
12		zcn	$⊢ y \in ℤ \to y \in ℂ$
13		zcn	$⊢ K \in ℤ \to K \in ℂ$
14		mulass	$⊢ (x \in ℂ \land y \in ℂ \land K \in ℂ) \to x y K = x y K$
15		mul12	$⊢ (x \in ℂ \land y \in ℂ \land K \in ℂ) \to x y K = y x K$
16	14 15	eqtrd	$⊢ (x \in ℂ \land y \in ℂ \land K \in ℂ) \to x y K = y x K$
17	11 12 13 16	syl3an	$⊢ (x \in ℤ \land y \in ℤ \land K \in ℤ) \to x y K = y x K$
18	17	3comr	$⊢ (K \in ℤ \land x \in ℤ \land y \in ℤ) \to x y K = y x K$
19	18	3expb	$⊢ (K \in ℤ \land (x \in ℤ \land y \in ℤ)) \to x y K = y x K$
20	19	3ad2antl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to x y K = y x K$
21	20	eqeq1d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to (x y K = N \leftrightarrow y x K = N)$
22	10 21	syl5ibr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to ((x K = M \land y \cdot M = N) \to x y K = N)$
23	1 2 3 5 22	dvds2lem	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land M ∥ N) \to K ∥ N)$

Metamath Proof Explorer

Theorem dvdstr

Proof