eucalgcvga

Description: Once Euclid's Algorithm halts after N steps, the second element of the state remains 0 . (Contributed by Paul Chapman, 22-Jun-2011) (Revised 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\}))$
	eucalgcvga.3	$⊢ N = 2^{nd} (A)$
Assertion	eucalgcvga	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to (K \in ℤ_{\geq N} \to 2^{nd} (R (K)) = 0)$

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		eucalgcvga.3	$⊢ N = 2^{nd} (A)$
4		xp2nd	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (A) \in ℕ_{0}$
5	3 4	eqeltrid	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to N \in ℕ_{0}$
6		eluznn0	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N}) \to K \in ℕ_{0}$
7	5 6	sylan	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to K \in ℕ_{0}$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		0zd	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to 0 \in ℤ$
10		id	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to A \in (ℕ_{0} \times ℕ_{0})$
11	1	eucalgf	$⊢ E : ℕ_{0} \times ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
12	11	a1i	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
13	8 2 9 10 12	algrf	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to R : ℕ_{0} ⟶ ℕ_{0} \times ℕ_{0}$
14	13	ffvelcdmda	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℕ_{0}) \to R (K) \in (ℕ_{0} \times ℕ_{0})$
15	7 14	syldan	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to R (K) \in (ℕ_{0} \times ℕ_{0})$
16	15	fvresd	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (K)) = 2^{nd} (R (K))$
17		simpl	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to A \in (ℕ_{0} \times ℕ_{0})$
18		fvres	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A) = 2^{nd} (A)$
19	18 3	eqtr4di	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A) = N$
20	19	fveq2d	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to ℤ_{\geq ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A)} = ℤ_{\geq N}$
21	20	eleq2d	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to (K \in ℤ_{\geq ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A)} \leftrightarrow K \in ℤ_{\geq N})$
22	21	biimpar	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to K \in ℤ_{\geq ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A)}$
23		f2ndres	$⊢ ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) : ℕ_{0} \times ℕ_{0} ⟶ ℕ_{0}$
24	1	eucalglt	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to (2^{nd} (E (z)) \neq 0 \to 2^{nd} (E (z)) < 2^{nd} (z))$
25	11	ffvelcdmi	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to E (z) \in (ℕ_{0} \times ℕ_{0})$
26	25	fvresd	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) = 2^{nd} (E (z))$
27	26	neeq1d	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to (({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) \neq 0 \leftrightarrow 2^{nd} (E (z)) \neq 0)$
28		fvres	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (z) = 2^{nd} (z)$
29	26 28	breq12d	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to (({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) < ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (z) \leftrightarrow 2^{nd} (E (z)) < 2^{nd} (z))$
30	24 27 29	3imtr4d	$⊢ z \in (ℕ_{0} \times ℕ_{0}) \to (({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) \neq 0 \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (E (z)) < ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (z))$
31		eqid	$⊢ ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A) = ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A)$
32	11 2 23 30 31	algcvga	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to (K \in ℤ_{\geq ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (A)} \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (K)) = 0)$
33	17 22 32	sylc	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to ({2^{nd} ↾}_{(ℕ_{0} \times ℕ_{0})}) (R (K)) = 0$
34	16 33	eqtr3d	$⊢ (A \in (ℕ_{0} \times ℕ_{0}) \land K \in ℤ_{\geq N}) \to 2^{nd} (R (K)) = 0$
35	34	ex	$⊢ A \in (ℕ_{0} \times ℕ_{0}) \to (K \in ℤ_{\geq N} \to 2^{nd} (R (K)) = 0)$

Metamath Proof Explorer

Theorem eucalgcvga

Proof