gcdn0cl

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	gcdn0cl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$

Step	Hyp	Ref	Expression
1		gcdn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$
2		eqid	$⊢ \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\} = \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\}$
3		eqid	$⊢ \{n \in ℤ \| (n ∥ M \land n ∥ N)\} = \{n \in ℤ \| (n ∥ M \land n ∥ N)\}$
4	2 3	gcdcllem3	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) \in ℕ \land (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ M \land sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ N) \land ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)))$
5	4	simp1d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) \in ℕ$
6	1 5	eqeltrd	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$

Metamath Proof Explorer