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	⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
	eucalg.2	⊢ 𝑅 = seq 0 ( ( 𝐸 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
	eucalgcvga.3	⊢ 𝑁 = ( 2nd ‘ 𝐴 )
Assertion	eucalgcvga	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 2nd ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
2		eucalg.2	⊢ 𝑅 = seq 0 ( ( 𝐸 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
3		eucalgcvga.3	⊢ 𝑁 = ( 2nd ‘ 𝐴 )
4		xp2nd	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝐴 ) ∈ ℕ0 )
5	3 4	eqeltrid	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → 𝑁 ∈ ℕ0 )
6		eluznn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ℕ0 )
7	5 6	sylan	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ℕ0 )
8		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9		0zd	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → 0 ∈ ℤ )
10		id	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → 𝐴 ∈ ( ℕ0 × ℕ0 ) )
11	1	eucalgf	⊢ 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 )
12	11	a1i	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 ) )
13	8 2 9 10 12	algrf	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → 𝑅 : ℕ0 ⟶ ( ℕ0 × ℕ0 ) )
14	13	ffvelrnda	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑅 ‘ 𝐾 ) ∈ ( ℕ0 × ℕ0 ) )
15	7 14	syldan	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ( ℕ0 × ℕ0 ) )
16	15	fvresd	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝐾 ) ) )
17		simpl	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ∈ ( ℕ0 × ℕ0 ) )
18		fvres	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) )
19	18 3	eqtr4di	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) = 𝑁 )
20	19	fveq2d	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( ℤ≥ ‘ ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) ) = ( ℤ≥ ‘ 𝑁 ) )
21	20	eleq2d	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) ) ↔ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
22	21	biimpar	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ( ℤ≥ ‘ ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) ) )
23		f2ndres	⊢ ( 2nd ↾ ( ℕ0 × ℕ0 ) ) : ( ℕ0 × ℕ0 ) ⟶ ℕ0
24	1	eucalglt	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ‘ ( 𝐸 ‘ 𝑧 ) ) ≠ 0 → ( 2nd ‘ ( 𝐸 ‘ 𝑧 ) ) < ( 2nd ‘ 𝑧 ) ) )
25	11	ffvelrni	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( 𝐸 ‘ 𝑧 ) ∈ ( ℕ0 × ℕ0 ) )
26	25	fvresd	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝐸 ‘ 𝑧 ) ) )
27	26	neeq1d	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) ≠ 0 ↔ ( 2nd ‘ ( 𝐸 ‘ 𝑧 ) ) ≠ 0 ) )
28		fvres	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
29	26 28	breq12d	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) < ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝑧 ) ↔ ( 2nd ‘ ( 𝐸 ‘ 𝑧 ) ) < ( 2nd ‘ 𝑧 ) ) )
30	24 27 29	3imtr4d	⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) ≠ 0 → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) < ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝑧 ) ) )
31		eqid	⊢ ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) = ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 )
32	11 2 23 30 31	algcvga	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝐴 ) ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )
33	17 22 32	sylc	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2nd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 )
34	16 33	eqtr3d	⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2nd ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 )
35	34	ex	⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 2nd ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )