Metamath Proof Explorer

Theorem 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 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 3simpa ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
2 3simpc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
3 3simpb ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
5 4 adantl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
6 oveq2 ⊢ ( ( 𝑥 · 𝐾 ) = 𝑀 → ( 𝑦 · ( 𝑥 · 𝐾 ) ) = ( 𝑦 · 𝑀 ) )
7 6 adantr ⊢ ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝑀 ) = 𝑁 ) → ( 𝑦 · ( 𝑥 · 𝐾 ) ) = ( 𝑦 · 𝑀 ) )
8 eqeq2 ⊢ ( ( 𝑦 · 𝑀 ) = 𝑁 → ( ( 𝑦 · ( 𝑥 · 𝐾 ) ) = ( 𝑦 · 𝑀 ) ↔ ( 𝑦 · ( 𝑥 · 𝐾 ) ) = 𝑁 ) )
9 8 adantl ⊢ ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝑀 ) = 𝑁 ) → ( ( 𝑦 · ( 𝑥 · 𝐾 ) ) = ( 𝑦 · 𝑀 ) ↔ ( 𝑦 · ( 𝑥 · 𝐾 ) ) = 𝑁 ) )
10 7 9 mpbid ⊢ ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝑀 ) = 𝑁 ) → ( 𝑦 · ( 𝑥 · 𝐾 ) ) = 𝑁 )
11 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
12 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
13 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
14 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑥 · ( 𝑦 · 𝐾 ) ) )
15 mul12 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑥 · ( 𝑦 · 𝐾 ) ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
16 14 15 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
17 11 12 13 16 syl3an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
18 17 3comr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
19 18 3expb ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
20 19 3ad2antl1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = ( 𝑦 · ( 𝑥 · 𝐾 ) ) )
21 20 eqeq1d ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝑦 ) · 𝐾 ) = 𝑁 ↔ ( 𝑦 · ( 𝑥 · 𝐾 ) ) = 𝑁 ) )
22 10 21 syl5ibr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝑀 ) = 𝑁 ) → ( ( 𝑥 · 𝑦 ) · 𝐾 ) = 𝑁 ) )
23 1 2 3 5 22 dvds2lem ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )