Description: Euclid's Algorithm computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. Theorem 1.15 in ApostolNT p. 20.
Upon halting, the 1st member of the final state ( RN ) is equal to the gcd of the values comprising the input state <. M , N >. . This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Paul Chapman, 31-Mar-2011) (Proof shortened by Mario Carneiro, 29-May-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | eucalgval.1 | ⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ) | |
| eucalg.2 | ⊢ 𝑅 = seq 0 ( ( 𝐸 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) ) | ||
| eucalg.3 | ⊢ 𝐴 = ⟨ 𝑀 , 𝑁 ⟩ | ||
| Assertion | eucalg | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eucalgval.1 | ⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ) | |
| 2 | eucalg.2 | ⊢ 𝑅 = seq 0 ( ( 𝐸 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) ) | |
| 3 | eucalg.3 | ⊢ 𝐴 = ⟨ 𝑀 , 𝑁 ⟩ | |
| 4 | nn0uz | ⊢ ℕ0 = ( ℤ≥ ‘ 0 ) | |
| 5 | 0zd | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 0 ∈ ℤ ) | |
| 6 | opelxpi | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ℕ0 × ℕ0 ) ) | |
| 7 | 3 6 | eqeltrid | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ( ℕ0 × ℕ0 ) ) |
| 8 | 1 | eucalgf | ⊢ 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 ) |
| 9 | 8 | a1i | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 ) ) |
| 10 | 4 2 5 7 9 | algrf | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑅 : ℕ0 ⟶ ( ℕ0 × ℕ0 ) ) |
| 11 | ffvelrn | ⊢ ( ( 𝑅 : ℕ0 ⟶ ( ℕ0 × ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑁 ) ∈ ( ℕ0 × ℕ0 ) ) | |
| 12 | 10 11 | sylancom | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑁 ) ∈ ( ℕ0 × ℕ0 ) ) |
| 13 | 1st2nd2 | ⊢ ( ( 𝑅 ‘ 𝑁 ) ∈ ( ℕ0 × ℕ0 ) → ( 𝑅 ‘ 𝑁 ) = ⟨ ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ⟩ ) | |
| 14 | 12 13 | syl | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑁 ) = ⟨ ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ⟩ ) |
| 15 | 14 | fveq2d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( gcd ‘ ( 𝑅 ‘ 𝑁 ) ) = ( gcd ‘ ⟨ ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ⟩ ) ) |
| 16 | df-ov | ⊢ ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ) = ( gcd ‘ ⟨ ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ⟩ ) | |
| 17 | 15 16 | eqtr4di | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( gcd ‘ ( 𝑅 ‘ 𝑁 ) ) = ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ) ) |
| 18 | 3 | fveq2i | ⊢ ( 2nd ‘ 𝐴 ) = ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) |
| 19 | op2ndg | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 ) | |
| 20 | 18 19 | eqtrid | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2nd ‘ 𝐴 ) = 𝑁 ) |
| 21 | 20 | fveq2d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ ( 2nd ‘ 𝐴 ) ) = ( 𝑅 ‘ 𝑁 ) ) |
| 22 | 21 | fveq2d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2nd ‘ ( 𝑅 ‘ ( 2nd ‘ 𝐴 ) ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ) |
| 23 | xp2nd | ⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝐴 ) ∈ ℕ0 ) | |
| 24 | 23 | nn0zd | ⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝐴 ) ∈ ℤ ) |
| 25 | uzid | ⊢ ( ( 2nd ‘ 𝐴 ) ∈ ℤ → ( 2nd ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 2nd ‘ 𝐴 ) ) ) | |
| 26 | 24 25 | syl | ⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 2nd ‘ 𝐴 ) ) ) |
| 27 | eqid | ⊢ ( 2nd ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) | |
| 28 | 1 2 27 | eucalgcvga | ⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( ( 2nd ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 2nd ‘ 𝐴 ) ) → ( 2nd ‘ ( 𝑅 ‘ ( 2nd ‘ 𝐴 ) ) ) = 0 ) ) |
| 29 | 26 28 | mpd | ⊢ ( 𝐴 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ ( 𝑅 ‘ ( 2nd ‘ 𝐴 ) ) ) = 0 ) |
| 30 | 7 29 | syl | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2nd ‘ ( 𝑅 ‘ ( 2nd ‘ 𝐴 ) ) ) = 0 ) |
| 31 | 22 30 | eqtr3d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) |
| 32 | 31 | oveq2d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd ( 2nd ‘ ( 𝑅 ‘ 𝑁 ) ) ) = ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd 0 ) ) |
| 33 | xp1st | ⊢ ( ( 𝑅 ‘ 𝑁 ) ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) ∈ ℕ0 ) | |
| 34 | nn0gcdid0 | ⊢ ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) ∈ ℕ0 → ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd 0 ) = ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) ) | |
| 35 | 12 33 34 | 3syl | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) gcd 0 ) = ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) ) |
| 36 | 17 32 35 | 3eqtrrd | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) = ( gcd ‘ ( 𝑅 ‘ 𝑁 ) ) ) |
| 37 | 1 | eucalginv | ⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( gcd ‘ ( 𝐸 ‘ 𝑧 ) ) = ( gcd ‘ 𝑧 ) ) |
| 38 | 8 | ffvelrni | ⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( 𝐸 ‘ 𝑧 ) ∈ ( ℕ0 × ℕ0 ) ) |
| 39 | 38 | fvresd | ⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) = ( gcd ‘ ( 𝐸 ‘ 𝑧 ) ) ) |
| 40 | fvres | ⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝑧 ) = ( gcd ‘ 𝑧 ) ) | |
| 41 | 37 39 40 | 3eqtr4d | ⊢ ( 𝑧 ∈ ( ℕ0 × ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝐸 ‘ 𝑧 ) ) = ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ 𝑧 ) ) |
| 42 | 2 8 41 | alginv | ⊢ ( ( 𝐴 ∈ ( ℕ0 × ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝑁 ) ) = ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 0 ) ) ) |
| 43 | 7 42 | sylancom | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝑁 ) ) = ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 0 ) ) ) |
| 44 | 12 | fvresd | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 𝑁 ) ) = ( gcd ‘ ( 𝑅 ‘ 𝑁 ) ) ) |
| 45 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
| 46 | ffvelrn | ⊢ ( ( 𝑅 : ℕ0 ⟶ ( ℕ0 × ℕ0 ) ∧ 0 ∈ ℕ0 ) → ( 𝑅 ‘ 0 ) ∈ ( ℕ0 × ℕ0 ) ) | |
| 47 | 10 45 46 | sylancl | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 0 ) ∈ ( ℕ0 × ℕ0 ) ) |
| 48 | 47 | fvresd | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( gcd ↾ ( ℕ0 × ℕ0 ) ) ‘ ( 𝑅 ‘ 0 ) ) = ( gcd ‘ ( 𝑅 ‘ 0 ) ) ) |
| 49 | 43 44 48 | 3eqtr3d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( gcd ‘ ( 𝑅 ‘ 𝑁 ) ) = ( gcd ‘ ( 𝑅 ‘ 0 ) ) ) |
| 50 | 4 2 5 7 | algr0 | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 0 ) = 𝐴 ) |
| 51 | 50 3 | eqtrdi | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ‘ 0 ) = ⟨ 𝑀 , 𝑁 ⟩ ) |
| 52 | 51 | fveq2d | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( gcd ‘ ( 𝑅 ‘ 0 ) ) = ( gcd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) |
| 53 | df-ov | ⊢ ( 𝑀 gcd 𝑁 ) = ( gcd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) | |
| 54 | 52 53 | eqtr4di | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( gcd ‘ ( 𝑅 ‘ 0 ) ) = ( 𝑀 gcd 𝑁 ) ) |
| 55 | 36 49 54 | 3eqtrd | ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 1st ‘ ( 𝑅 ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) |