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	⊢ 𝐸 = ( 𝑥 ∈ ℕ₀ , 𝑦 ∈ ℕ₀ ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
	Assertion	eucalginv	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( gcd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( gcd ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	⊢ 𝐸 = ( 𝑥 ∈ ℕ₀ , 𝑦 ∈ ℕ₀ ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
2	1	eucalgval	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) )
3	2	fveq2d	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( gcd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) )
4		1st2nd2	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
5	4	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
6	5	fveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( mod ‘ 𝑋 ) = ( mod ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) )
7		df-ov	⊢ ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) = ( mod ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
8	6 7	syl6eqr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( mod ‘ 𝑋 ) = ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) )
9	8	oveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 2^nd ‘ 𝑋 ) gcd ( mod ‘ 𝑋 ) ) = ( ( 2^nd ‘ 𝑋 ) gcd ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ) )
10		nnz	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ → ( 2^nd ‘ 𝑋 ) ∈ ℤ )
11		xp1st	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 1^st ‘ 𝑋 ) ∈ ℕ₀ )
12	11	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( 1^st ‘ 𝑋 ) ∈ ℕ₀ )
13	12	nn0zd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( 1^st ‘ 𝑋 ) ∈ ℤ )
14		zmodcl	⊢ ( ( ( 1^st ‘ 𝑋 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ∈ ℕ₀ )
15	13 14	sylancom	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ∈ ℕ₀ )
16	15	nn0zd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ∈ ℤ )
17		gcdcom	⊢ ( ( ( 2^nd ‘ 𝑋 ) ∈ ℤ ∧ ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ∈ ℤ ) → ( ( 2^nd ‘ 𝑋 ) gcd ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ) = ( ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) gcd ( 2^nd ‘ 𝑋 ) ) )
18	10 16 17	syl2an2	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 2^nd ‘ 𝑋 ) gcd ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) ) = ( ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) gcd ( 2^nd ‘ 𝑋 ) ) )
19		modgcd	⊢ ( ( ( 1^st ‘ 𝑋 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) gcd ( 2^nd ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) gcd ( 2^nd ‘ 𝑋 ) ) )
20	13 19	sylancom	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) gcd ( 2^nd ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) gcd ( 2^nd ‘ 𝑋 ) ) )
21	9 18 20	3eqtrd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( ( 2^nd ‘ 𝑋 ) gcd ( mod ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) gcd ( 2^nd ‘ 𝑋 ) ) )
22		nnne0	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ → ( 2^nd ‘ 𝑋 ) ≠ 0 )
23	22	adantl	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( 2^nd ‘ 𝑋 ) ≠ 0 )
24	23	neneqd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ¬ ( 2^nd ‘ 𝑋 ) = 0 )
25	24	iffalsed	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ )
26	25	fveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( gcd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) )
27		df-ov	⊢ ( ( 2^nd ‘ 𝑋 ) gcd ( mod ‘ 𝑋 ) ) = ( gcd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ )
28	26 27	syl6eqr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( ( 2^nd ‘ 𝑋 ) gcd ( mod ‘ 𝑋 ) ) )
29	5	fveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( gcd ‘ 𝑋 ) = ( gcd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) )
30		df-ov	⊢ ( ( 1^st ‘ 𝑋 ) gcd ( 2^nd ‘ 𝑋 ) ) = ( gcd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
31	29 30	syl6eqr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( gcd ‘ 𝑋 ) = ( ( 1^st ‘ 𝑋 ) gcd ( 2^nd ‘ 𝑋 ) ) )
32	21 28 31	3eqtr4d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ℕ ) → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( gcd ‘ 𝑋 ) )
33		iftrue	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) = 𝑋 )
34	33	fveq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( gcd ‘ 𝑋 ) )
35	34	adantl	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ 𝑋 ) = 0 ) → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( gcd ‘ 𝑋 ) )
36		xp2nd	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 2^nd ‘ 𝑋 ) ∈ ℕ₀ )
37		elnn0	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ₀ ↔ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ ∨ ( 2^nd ‘ 𝑋 ) = 0 ) )
38	36 37	sylib	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( ( 2^nd ‘ 𝑋 ) ∈ ℕ ∨ ( 2^nd ‘ 𝑋 ) = 0 ) )
39	32 35 38	mpjaodan	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( gcd ‘ if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ) = ( gcd ‘ 𝑋 ) )
40	3 39	eqtrd	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( gcd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( gcd ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem eucalginv

Proof