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	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\gcd B=A\gcd B$$

Proof

Step	Hyp	Ref	Expression
1		gcdass	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\gcd B=A\gcd \left(B\gcd B\right)$$
2	1	3anidm23	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\gcd B=A\gcd \left(B\gcd B\right)$$
3		gcdid	$$⊢B\in \mathbb{Z}\to B\gcd B=\left|B\right|$$
4	3	oveq2d	$$⊢B\in \mathbb{Z}\to A\gcd \left(B\gcd B\right)=A\gcd \left|B\right|$$
5	4	adantl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\gcd \left(B\gcd B\right)=A\gcd \left|B\right|$$
6		gcdabs2	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\gcd \left|B\right|=A\gcd B$$
7	2 5 6	3eqtrd	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\gcd B=A\gcd B$$