gcdass

Description: Associative law for gcd operator. Theorem 1.4(b) in ApostolNT p. 16. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	gcdass	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (N \gcd M) \gcd P = N \gcd (M \gcd P)$

Proof

Step	Hyp	Ref	Expression
1		anass	$⊢ ((N = 0 \land M = 0) \land P = 0) \leftrightarrow (N = 0 \land (M = 0 \land P = 0))$
2		anass	$⊢ ((x ∥ N \land x ∥ M) \land x ∥ P) \leftrightarrow (x ∥ N \land (x ∥ M \land x ∥ P))$
3	2	rabbii	$⊢ \{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} = \{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\}$
4	3	supeq1i	$⊢ sup (\{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} ℝ <) = sup (\{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} ℝ <)$
5	1 4	ifbieq2i	$⊢ if (((N = 0 \land M = 0) \land P = 0), 0, sup (\{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} ℝ <)) = if ((N = 0 \land (M = 0 \land P = 0)), 0, sup (\{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} ℝ <))$
6		gcdcl	$⊢ (N \in ℤ \land M \in ℤ) \to N \gcd M \in ℕ_{0}$
7	6	3adant3	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to N \gcd M \in ℕ_{0}$
8	7	nn0zd	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to N \gcd M \in ℤ$
9		simp3	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to P \in ℤ$
10		gcdval	$⊢ (N \gcd M \in ℤ \land P \in ℤ) \to (N \gcd M) \gcd P = if ((N \gcd M = 0 \land P = 0), 0, sup (\{x \in ℤ \| (x ∥ (N \gcd M) \land x ∥ P)\} ℝ <))$
11	8 9 10	syl2anc	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (N \gcd M) \gcd P = if ((N \gcd M = 0 \land P = 0), 0, sup (\{x \in ℤ \| (x ∥ (N \gcd M) \land x ∥ P)\} ℝ <))$
12		gcdeq0	$⊢ (N \in ℤ \land M \in ℤ) \to (N \gcd M = 0 \leftrightarrow (N = 0 \land M = 0))$
13	12	3adant3	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (N \gcd M = 0 \leftrightarrow (N = 0 \land M = 0))$
14	13	anbi1d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to ((N \gcd M = 0 \land P = 0) \leftrightarrow ((N = 0 \land M = 0) \land P = 0))$
15	14	bicomd	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (((N = 0 \land M = 0) \land P = 0) \leftrightarrow (N \gcd M = 0 \land P = 0))$
16		simpr	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to x \in ℤ$
17		simpl1	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to N \in ℤ$
18		simpl2	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to M \in ℤ$
19		dvdsgcdb	$⊢ (x \in ℤ \land N \in ℤ \land M \in ℤ) \to ((x ∥ N \land x ∥ M) \leftrightarrow x ∥ (N \gcd M))$
20	16 17 18 19	syl3anc	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to ((x ∥ N \land x ∥ M) \leftrightarrow x ∥ (N \gcd M))$
21	20	anbi1d	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to (((x ∥ N \land x ∥ M) \land x ∥ P) \leftrightarrow (x ∥ (N \gcd M) \land x ∥ P))$
22	21	rabbidva	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to \{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} = \{x \in ℤ \| (x ∥ (N \gcd M) \land x ∥ P)\}$
23	22	supeq1d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to sup (\{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} ℝ <) = sup (\{x \in ℤ \| (x ∥ (N \gcd M) \land x ∥ P)\} ℝ <)$
24	15 23	ifbieq2d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to if (((N = 0 \land M = 0) \land P = 0), 0, sup (\{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} ℝ <)) = if ((N \gcd M = 0 \land P = 0), 0, sup (\{x \in ℤ \| (x ∥ (N \gcd M) \land x ∥ P)\} ℝ <))$
25	11 24	eqtr4d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (N \gcd M) \gcd P = if (((N = 0 \land M = 0) \land P = 0), 0, sup (\{x \in ℤ \| ((x ∥ N \land x ∥ M) \land x ∥ P)\} ℝ <))$
26		simp1	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to N \in ℤ$
27		gcdcl	$⊢ (M \in ℤ \land P \in ℤ) \to M \gcd P \in ℕ_{0}$
28	27	3adant1	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to M \gcd P \in ℕ_{0}$
29	28	nn0zd	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to M \gcd P \in ℤ$
30		gcdval	$⊢ (N \in ℤ \land M \gcd P \in ℤ) \to N \gcd (M \gcd P) = if ((N = 0 \land M \gcd P = 0), 0, sup (\{x \in ℤ \| (x ∥ N \land x ∥ (M \gcd P))\} ℝ <))$
31	26 29 30	syl2anc	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to N \gcd (M \gcd P) = if ((N = 0 \land M \gcd P = 0), 0, sup (\{x \in ℤ \| (x ∥ N \land x ∥ (M \gcd P))\} ℝ <))$
32		gcdeq0	$⊢ (M \in ℤ \land P \in ℤ) \to (M \gcd P = 0 \leftrightarrow (M = 0 \land P = 0))$
33	32	3adant1	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (M \gcd P = 0 \leftrightarrow (M = 0 \land P = 0))$
34	33	anbi2d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to ((N = 0 \land M \gcd P = 0) \leftrightarrow (N = 0 \land (M = 0 \land P = 0)))$
35	34	bicomd	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to ((N = 0 \land (M = 0 \land P = 0)) \leftrightarrow (N = 0 \land M \gcd P = 0))$
36		simpl3	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to P \in ℤ$
37		dvdsgcdb	$⊢ (x \in ℤ \land M \in ℤ \land P \in ℤ) \to ((x ∥ M \land x ∥ P) \leftrightarrow x ∥ (M \gcd P))$
38	16 18 36 37	syl3anc	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to ((x ∥ M \land x ∥ P) \leftrightarrow x ∥ (M \gcd P))$
39	38	anbi2d	$⊢ ((N \in ℤ \land M \in ℤ \land P \in ℤ) \land x \in ℤ) \to ((x ∥ N \land (x ∥ M \land x ∥ P)) \leftrightarrow (x ∥ N \land x ∥ (M \gcd P)))$
40	39	rabbidva	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to \{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} = \{x \in ℤ \| (x ∥ N \land x ∥ (M \gcd P))\}$
41	40	supeq1d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to sup (\{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} ℝ <) = sup (\{x \in ℤ \| (x ∥ N \land x ∥ (M \gcd P))\} ℝ <)$
42	35 41	ifbieq2d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to if ((N = 0 \land (M = 0 \land P = 0)), 0, sup (\{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} ℝ <)) = if ((N = 0 \land M \gcd P = 0), 0, sup (\{x \in ℤ \| (x ∥ N \land x ∥ (M \gcd P))\} ℝ <))$
43	31 42	eqtr4d	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to N \gcd (M \gcd P) = if ((N = 0 \land (M = 0 \land P = 0)), 0, sup (\{x \in ℤ \| (x ∥ N \land (x ∥ M \land x ∥ P))\} ℝ <))$
44	5 25 43	3eqtr4a	$⊢ (N \in ℤ \land M \in ℤ \land P \in ℤ) \to (N \gcd M) \gcd P = N \gcd (M \gcd P)$

Metamath Proof Explorer

Theorem gcdass

Proof