eucalg

Description: Euclid's Algorithm computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. Theorem 1.15 in ApostolNT p. 20.

Upon halting, the first member of the final state ( RN ) is equal to the gcd of the values comprising the input state <. M , N >. . This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Paul Chapman, 31-Mar-2011) (Proof shortened by Mario Carneiro, 29-May-2014)

	Ref	Expression
Hypotheses	eucalgval.1	$⊢ E = (x \in ℕ_{0}, y \in ℕ_{0} ⟼ if (y = 0, ⟨x, y⟩, ⟨y, x \mod y⟩))$
	eucalg.2	$⊢ R = seq 0 ((E \circ 1^{st}), (ℕ_{0} \times \{A\}))$
	eucalg.3	$⊢ A = ⟨M, N⟩$
Assertion	eucalg	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 1^{st} (R (N)) = M \gcd N$

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	$⊢ E = (x \in ℕ_{0}, y \in ℕ_{0} ⟼ if (y = 0, ⟨x, y⟩, ⟨y, x \mod y⟩))$
2		eucalg.2	$⊢ R = seq 0 ((E \circ 1^{st}), (ℕ_{0} \times \{A\}))$
3		eucalg.3	$⊢ A = ⟨M, N⟩$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		0zd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \in ℤ$
6		opelxpi	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ⟨M, N⟩ \in (ℕ_{0} \times ℕ_{0})$
7	3 6	eqeltrid	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to A \in (ℕ_{0} \times ℕ_{0})$
8	1	eucalgf	$⊢ E : ℕ_{0} \times ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
9	8	a1i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
10	4 2 5 7 9	algrf	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R : ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
11		ffvelcdm	$⊢ (R : ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0} \land N \in ℕ_{0}) \to R (N) \in (ℕ_{0} \times ℕ_{0})$
12	10 11	sylancom	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (N) \in (ℕ_{0} \times ℕ_{0})$
13		1st2nd2	$⊢ R (N) \in (ℕ_{0} \times ℕ_{0}) \to R (N) = ⟨1^{st} (R (N)), 2^{nd} (R (N))⟩$
14	12 13	syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (N) = ⟨1^{st} (R (N)), 2^{nd} (R (N))⟩$
15	14	fveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to \gcd (R (N)) = \gcd (⟨1^{st} (R (N)), 2^{nd} (R (N))⟩)$
16		df-ov	$⊢ 1^{st} (R (N)) \gcd 2^{nd} (R (N)) = \gcd (⟨1^{st} (R (N)), 2^{nd} (R (N))⟩)$
17	15 16	eqtr4di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to \gcd (R (N)) = 1^{st} (R (N)) \gcd 2^{nd} (R (N))$
18	3	fveq2i	$⊢ 2^{nd} (A) = 2^{nd} (⟨M, N⟩)$
19		op2ndg	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 2^{nd} (⟨M, N⟩) = N$
20	18 19	eqtrid	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 2^{nd} (A) = N$
21	20	fveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (2^{nd} (A)) = R (N)$
22	21	fveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 2^{nd} (R (2^{nd} (A))) = 2^{nd} (R (N))$
23		xp2nd	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (A) \in ℕ_{0}$
24	23	nn0zd	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (A) \in ℤ$
25		uzid	$⊢ 2^{nd} (A) \in ℤ \to 2^{nd} (A) \in ℤ_{\geq 2^{nd} (A)}$
26	24 25	syl	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (A) \in ℤ_{\geq 2^{nd} (A)}$
27		eqid	$⊢ 2^{nd} (A) = 2^{nd} (A)$
28	1 2 27	eucalgcvga	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to (2^{nd} (A) \in ℤ_{\geq 2^{nd} (A)} \to 2^{nd} (R (2^{nd} (A))) = 0)$
29	26 28	mpd	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (R (2^{nd} (A))) = 0$
30	7 29	syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 2^{nd} (R (2^{nd} (A))) = 0$
31	22 30	eqtr3d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 2^{nd} (R (N)) = 0$
32	31	oveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 1^{st} (R (N)) \gcd 2^{nd} (R (N)) = 1^{st} (R (N)) \gcd 0$
33		xp1st	$⊢ R (N) \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (R (N)) \in ℕ_{0}$
34		nn0gcdid0	$⊢ 1^{st} (R (N)) \in ℕ_{0} \to 1^{st} (R (N)) \gcd 0 = 1^{st} (R (N))$
35	12 33 34	3syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 1^{st} (R (N)) \gcd 0 = 1^{st} (R (N))$
36	17 32 35	3eqtrrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 1^{st} (R (N)) = \gcd (R (N))$
37	1	eucalginv	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to \gcd (E (z)) = \gcd (z)$
38	8	ffvelcdmi	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to E (z) \in (ℕ_{0} \times ℕ_{0})$
39	38	fvresd	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) = \gcd (E (z))$
40		fvres	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (z) = \gcd (z)$
41	37 39 40	3eqtr4d	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) = ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (z)$
42	2 8 41	alginv	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land N \in ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (N)) = ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (0))$
43	7 42	sylancom	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (N)) = ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (0))$
44	12	fvresd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (N)) = \gcd (R (N))$
45		0nn0	$⊢ 0 \in ℕ_{0}$
46		ffvelcdm	$⊢ (R : ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0} \land 0 \in ℕ_{0}) \to R (0) \in (ℕ_{0} \times ℕ_{0})$
47	10 45 46	sylancl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (0) \in (ℕ_{0} \times ℕ_{0})$
48	47	fvresd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ({\gcd ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (0)) = \gcd (R (0))$
49	43 44 48	3eqtr3d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to \gcd (R (N)) = \gcd (R (0))$
50	4 2 5 7	algr0	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (0) = A$
51	50 3	eqtrdi	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to R (0) = ⟨M, N⟩$
52	51	fveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to \gcd (R (0)) = \gcd (⟨M, N⟩)$
53		df-ov	$⊢ M \gcd N = \gcd (⟨M, N⟩)$
54	52 53	eqtr4di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to \gcd (R (0)) = M \gcd N$
55	36 49 54	3eqtrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 1^{st} (R (N)) = M \gcd N$

Metamath Proof Explorer

Theorem eucalg

Proof