Metamath Proof Explorer


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

Proof

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