Theorem gcdabsorb

Description: Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	gcdabsorb	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐵 ) = ( 𝐴 gcd 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		gcdass	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐵 ) = ( 𝐴 gcd ( 𝐵 gcd 𝐵 ) ) )
2	1	3anidm23	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐵 ) = ( 𝐴 gcd ( 𝐵 gcd 𝐵 ) ) )
3		gcdid	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
4	3	oveq2d	⊢ ( 𝐵 ∈ ℤ → ( 𝐴 gcd ( 𝐵 gcd 𝐵 ) ) = ( 𝐴 gcd ( abs ‘ 𝐵 ) ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd ( 𝐵 gcd 𝐵 ) ) = ( 𝐴 gcd ( abs ‘ 𝐵 ) ) )
6		gcdabs2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd ( abs ‘ 𝐵 ) ) = ( 𝐴 gcd 𝐵 ) )
7	2 5 6	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐵 ) = ( 𝐴 gcd 𝐵 ) )