Theorem 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=\left(x\in {\mathbb{N}}_0,y\in {\mathbb{N}}_0⟼if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\right)$$
	eucalg.2	$$⊢R=seq0\left(\left(E\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{A\right\}\right)\right)$$
	eucalgcvga.3	$$⊢N=2^{nd}\left(A\right)$$
Assertion	eucalgcvga	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(K\in {\mathbb{Z}}_{\ge N}\to 2^{nd}\left(R\left(K\right)\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	$$⊢E=\left(x\in {\mathbb{N}}_0,y\in {\mathbb{N}}_0⟼if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\right)$$
2		eucalg.2	$$⊢R=seq0\left(\left(E\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{A\right\}\right)\right)$$
3		eucalgcvga.3	$$⊢N=2^{nd}\left(A\right)$$
4		xp2nd	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to 2^{nd}\left(A\right)\in {\mathbb{N}}_0$$
5	3 4	eqeltrid	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
6		eluznn0	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to K\in {\mathbb{N}}_0$$
7	5 6	sylan	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to K\in {\mathbb{N}}_0$$
8		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
9		0zd	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to 0\in \mathbb{Z}$$
10		id	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
11	1	eucalgf	$$⊢E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$
12	11	a1i	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$
13	8 2 9 10 12	algrf	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to R:{\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$
14	13	ffvelrnda	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{N}}_0\right)\to R\left(K\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
15	7 14	syldan	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to R\left(K\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
16	15	fvresd	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(R\left(K\right)\right)=2^{nd}\left(R\left(K\right)\right)$$
17		simpl	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
18		fvres	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)=2^{nd}\left(A\right)$$
19	18 3	eqtr4di	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)=N$$
20	19	fveq2d	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to {\mathbb{Z}}_{\ge \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)}={\mathbb{Z}}_{\ge N}$$
21	20	eleq2d	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(K\in {\mathbb{Z}}_{\ge \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)}\leftrightarrow K\in {\mathbb{Z}}_{\ge N}\right)$$
22	21	biimpar	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to K\in {\mathbb{Z}}_{\ge \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)}$$
23		f2ndres	$$⊢\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right):{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0$$
24	1	eucalglt	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(2^{nd}\left(E\left(z\right)\right)\ne 0\to 2^{nd}\left(E\left(z\right)\right)<2^{nd}\left(z\right)\right)$$
25	11	ffvelrni	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to E\left(z\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
26	25	fvresd	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(E\left(z\right)\right)=2^{nd}\left(E\left(z\right)\right)$$
27	26	neeq1d	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(E\left(z\right)\right)\ne 0\leftrightarrow 2^{nd}\left(E\left(z\right)\right)\ne 0\right)$$
28		fvres	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(z\right)=2^{nd}\left(z\right)$$
29	26 28	breq12d	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(E\left(z\right)\right)<\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(z\right)\leftrightarrow 2^{nd}\left(E\left(z\right)\right)<2^{nd}\left(z\right)\right)$$
30	24 27 29	3imtr4d	$$⊢z\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(E\left(z\right)\right)\ne 0\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(E\left(z\right)\right)<\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(z\right)\right)$$
31		eqid	$$⊢\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)=\left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)$$
32	11 2 23 30 31	algcvga	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(K\in {\mathbb{Z}}_{\ge \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(A\right)}\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(R\left(K\right)\right)=0\right)$$
33	17 22 32	sylc	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to \left({2^{nd}\upharpoonright }_{\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)}\right)\left(R\left(K\right)\right)=0$$
34	16 33	eqtr3d	$$⊢\left(A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to 2^{nd}\left(R\left(K\right)\right)=0$$
35	34	ex	$$⊢A\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to \left(K\in {\mathbb{Z}}_{\ge N}\to 2^{nd}\left(R\left(K\right)\right)=0\right)$$