eucalginv

Description: The invariant of the step function E for Euclid's Algorithm is the gcd operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 29-May-2014)

		Ref	Expression
	Hypothesis	eucalgval.1	$⊢ E = (x \in ℕ_{0}, y \in ℕ_{0} ⟼ if (y = 0, ⟨x, y⟩, ⟨y, x \mod y⟩))$
	Assertion	eucalginv	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to \gcd (E (X)) = \gcd (X)$

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	1	eucalgval	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)$
3	2	fveq2d	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to \gcd (E (X)) = \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩))$
4		1st2nd2	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
5	4	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
6	5	fveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \mod (X) = \mod (⟨1^{st} (X), 2^{nd} (X)⟩)$
7		df-ov	$⊢ 1^{st} (X) \mod 2^{nd} (X) = \mod (⟨1^{st} (X), 2^{nd} (X)⟩)$
8	6 7	eqtr4di	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \mod (X) = 1^{st} (X) \mod 2^{nd} (X)$
9	8	oveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 2^{nd} (X) \gcd \mod (X) = 2^{nd} (X) \gcd (1^{st} (X) \mod 2^{nd} (X))$
10		nnz	$⊢ 2^{nd} (X) \in ℕ \to 2^{nd} (X) \in ℤ$
11		xp1st	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (X) \in ℕ_{0}$
12	11	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 1^{st} (X) \in ℕ_{0}$
13	12	nn0zd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 1^{st} (X) \in ℤ$
14		zmodcl	$⊢ (1^{st} (X) \in ℤ \land 2^{nd} (X) \in ℕ) \to 1^{st} (X) \mod 2^{nd} (X) \in ℕ_{0}$
15	13 14	sylancom	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 1^{st} (X) \mod 2^{nd} (X) \in ℕ_{0}$
16	15	nn0zd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 1^{st} (X) \mod 2^{nd} (X) \in ℤ$
17		gcdcom	$⊢ (2^{nd} (X) \in ℤ \land 1^{st} (X) \mod 2^{nd} (X) \in ℤ) \to 2^{nd} (X) \gcd (1^{st} (X) \mod 2^{nd} (X)) = (1^{st} (X) \mod 2^{nd} (X)) \gcd 2^{nd} (X)$
18	10 16 17	syl2an2	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 2^{nd} (X) \gcd (1^{st} (X) \mod 2^{nd} (X)) = (1^{st} (X) \mod 2^{nd} (X)) \gcd 2^{nd} (X)$
19		modgcd	$⊢ (1^{st} (X) \in ℤ \land 2^{nd} (X) \in ℕ) \to (1^{st} (X) \mod 2^{nd} (X)) \gcd 2^{nd} (X) = 1^{st} (X) \gcd 2^{nd} (X)$
20	13 19	sylancom	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to (1^{st} (X) \mod 2^{nd} (X)) \gcd 2^{nd} (X) = 1^{st} (X) \gcd 2^{nd} (X)$
21	9 18 20	3eqtrd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 2^{nd} (X) \gcd \mod (X) = 1^{st} (X) \gcd 2^{nd} (X)$
22		nnne0	$⊢ 2^{nd} (X) \in ℕ \to 2^{nd} (X) \neq 0$
23	22	adantl	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to 2^{nd} (X) \neq 0$
24	23	neneqd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \neg 2^{nd} (X) = 0$
25	24	iffalsed	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) = ⟨2^{nd} (X), \mod (X)⟩$
26	25	fveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = \gcd (⟨2^{nd} (X), \mod (X)⟩)$
27		df-ov	$⊢ 2^{nd} (X) \gcd \mod (X) = \gcd (⟨2^{nd} (X), \mod (X)⟩)$
28	26 27	eqtr4di	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = 2^{nd} (X) \gcd \mod (X)$
29	5	fveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \gcd (X) = \gcd (⟨1^{st} (X), 2^{nd} (X)⟩)$
30		df-ov	$⊢ 1^{st} (X) \gcd 2^{nd} (X) = \gcd (⟨1^{st} (X), 2^{nd} (X)⟩)$
31	29 30	eqtr4di	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \gcd (X) = 1^{st} (X) \gcd 2^{nd} (X)$
32	21 28 31	3eqtr4d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) \in ℕ) \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = \gcd (X)$
33		iftrue	$⊢ 2^{nd} (X) = 0 \to if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) = X$
34	33	fveq2d	$⊢ 2^{nd} (X) = 0 \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = \gcd (X)$
35	34	adantl	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (X) = 0) \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = \gcd (X)$
36		xp2nd	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (X) \in ℕ_{0}$
37		elnn0	$⊢ 2^{nd} (X) \in ℕ_{0} \leftrightarrow (2^{nd} (X) \in ℕ \lor 2^{nd} (X) = 0)$
38	36 37	sylib	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to (2^{nd} (X) \in ℕ \lor 2^{nd} (X) = 0)$
39	32 35 38	mpjaodan	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to \gcd (if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)) = \gcd (X)$
40	3 39	eqtrd	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to \gcd (E (X)) = \gcd (X)$

Metamath Proof Explorer

Theorem eucalginv

Proof