Theorem gcdval

Description: The value of the gcd operator. ( M gcd N ) is the greatest common divisor of M and N . If M and N are both 0 , the result is defined conventionally as 0 . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 10-Nov-2013)

	Ref	Expression
Assertion	gcdval	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N=if\left(\left(M=0\wedge N=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=M\to \left(x=0\leftrightarrow M=0\right)$$
2	1	anbi1d	$$⊢x=M\to \left(\left(x=0\wedge y=0\right)\leftrightarrow \left(M=0\wedge y=0\right)\right)$$
3		breq2	$$⊢x=M\to \left(n\parallel x\leftrightarrow n\parallel M\right)$$
4	3	anbi1d	$$⊢x=M\to \left(\left(n\parallel x\wedge n\parallel y\right)\leftrightarrow \left(n\parallel M\wedge n\parallel y\right)\right)$$
5	4	rabbidv	$$⊢x=M\to \left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\}=\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\}$$
6	5	supeq1d	$$⊢x=M\to sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)=sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\},ℝ,<\right)$$
7	2 6	ifbieq2d	$$⊢x=M\to if\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)=if\left(\left(M=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\},ℝ,<\right)\right)$$
8		eqeq1	$$⊢y=N\to \left(y=0\leftrightarrow N=0\right)$$
9	8	anbi2d	$$⊢y=N\to \left(\left(M=0\wedge y=0\right)\leftrightarrow \left(M=0\wedge N=0\right)\right)$$
10		breq2	$$⊢y=N\to \left(n\parallel y\leftrightarrow n\parallel N\right)$$
11	10	anbi2d	$$⊢y=N\to \left(\left(n\parallel M\wedge n\parallel y\right)\leftrightarrow \left(n\parallel M\wedge n\parallel N\right)\right)$$
12	11	rabbidv	$$⊢y=N\to \left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\}=\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\}$$
13	12	supeq1d	$$⊢y=N\to sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\},ℝ,<\right)=sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)$$
14	9 13	ifbieq2d	$$⊢y=N\to if\left(\left(M=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel y\right)\right\},ℝ,<\right)\right)=if\left(\left(M=0\wedge N=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)\right)$$
15		df-gcd	$$⊢\gcd =\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)\right)$$
16		c0ex	$$⊢0\in \mathrm{V}$$
17		ltso	$$⊢<\mathrm{Or}ℝ$$
18	17	supex	$$⊢sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)\in \mathrm{V}$$
19	16 18	ifex	$$⊢if\left(\left(M=0\wedge N=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)\right)\in \mathrm{V}$$
20	7 14 15 19	ovmpo	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N=if\left(\left(M=0\wedge N=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel M\wedge n\parallel N\right)\right\},ℝ,<\right)\right)$$