Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eucalg Structured version   Visualization version   GIF version

Theorem eucalg 15938
 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 (𝑅‘𝑁) is equal to the gcd of the values comprising the input state ⟨𝑀, 𝑁⟩. 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.)
Hypotheses
Ref Expression
eucalgval.1 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))
eucalg.2 𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}))
eucalg.3 𝐴 = ⟨𝑀, 𝑁
Assertion
Ref Expression
eucalg ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (1st ‘(𝑅𝑁)) = (𝑀 gcd 𝑁))
Distinct variable groups:   𝑥,𝑦,𝑀   𝑥,𝑁,𝑦   𝑥,𝐴,𝑦   𝑥,𝑅
Allowed substitution hints:   𝑅(𝑦)   𝐸(𝑥,𝑦)

Proof of Theorem eucalg
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nn0uz 12285 . . . . . . . 8 0 = (ℤ‘0)
2 eucalg.2 . . . . . . . 8 𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}))
3 0zd 11998 . . . . . . . 8 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 ∈ ℤ)
4 eucalg.3 . . . . . . . . 9 𝐴 = ⟨𝑀, 𝑁
5 opelxpi 5559 . . . . . . . . 9 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ⟨𝑀, 𝑁⟩ ∈ (ℕ0 × ℕ0))
64, 5eqeltrid 2894 . . . . . . . 8 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝐴 ∈ (ℕ0 × ℕ0))
7 eucalgval.1 . . . . . . . . . 10 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))
87eucalgf 15934 . . . . . . . . 9 𝐸:(ℕ0 × ℕ0)⟶(ℕ0 × ℕ0)
98a1i 11 . . . . . . . 8 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝐸:(ℕ0 × ℕ0)⟶(ℕ0 × ℕ0))
101, 2, 3, 6, 9algrf 15924 . . . . . . 7 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑅:ℕ0⟶(ℕ0 × ℕ0))
11 ffvelrn 6833 . . . . . . 7 ((𝑅:ℕ0⟶(ℕ0 × ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑅𝑁) ∈ (ℕ0 × ℕ0))
1210, 11sylancom 591 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅𝑁) ∈ (ℕ0 × ℕ0))
13 1st2nd2 7720 . . . . . 6 ((𝑅𝑁) ∈ (ℕ0 × ℕ0) → (𝑅𝑁) = ⟨(1st ‘(𝑅𝑁)), (2nd ‘(𝑅𝑁))⟩)
1412, 13syl 17 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅𝑁) = ⟨(1st ‘(𝑅𝑁)), (2nd ‘(𝑅𝑁))⟩)
1514fveq2d 6656 . . . 4 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ( gcd ‘(𝑅𝑁)) = ( gcd ‘⟨(1st ‘(𝑅𝑁)), (2nd ‘(𝑅𝑁))⟩))
16 df-ov 7145 . . . 4 ((1st ‘(𝑅𝑁)) gcd (2nd ‘(𝑅𝑁))) = ( gcd ‘⟨(1st ‘(𝑅𝑁)), (2nd ‘(𝑅𝑁))⟩)
1715, 16eqtr4di 2851 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ( gcd ‘(𝑅𝑁)) = ((1st ‘(𝑅𝑁)) gcd (2nd ‘(𝑅𝑁))))
184fveq2i 6655 . . . . . . . 8 (2nd𝐴) = (2nd ‘⟨𝑀, 𝑁⟩)
19 op2ndg 7694 . . . . . . . 8 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (2nd ‘⟨𝑀, 𝑁⟩) = 𝑁)
2018, 19syl5eq 2845 . . . . . . 7 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (2nd𝐴) = 𝑁)
2120fveq2d 6656 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅‘(2nd𝐴)) = (𝑅𝑁))
2221fveq2d 6656 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (2nd ‘(𝑅‘(2nd𝐴))) = (2nd ‘(𝑅𝑁)))
23 xp2nd 7714 . . . . . . . . 9 (𝐴 ∈ (ℕ0 × ℕ0) → (2nd𝐴) ∈ ℕ0)
2423nn0zd 12090 . . . . . . . 8 (𝐴 ∈ (ℕ0 × ℕ0) → (2nd𝐴) ∈ ℤ)
25 uzid 12263 . . . . . . . 8 ((2nd𝐴) ∈ ℤ → (2nd𝐴) ∈ (ℤ‘(2nd𝐴)))
2624, 25syl 17 . . . . . . 7 (𝐴 ∈ (ℕ0 × ℕ0) → (2nd𝐴) ∈ (ℤ‘(2nd𝐴)))
27 eqid 2798 . . . . . . . 8 (2nd𝐴) = (2nd𝐴)
287, 2, 27eucalgcvga 15937 . . . . . . 7 (𝐴 ∈ (ℕ0 × ℕ0) → ((2nd𝐴) ∈ (ℤ‘(2nd𝐴)) → (2nd ‘(𝑅‘(2nd𝐴))) = 0))
2926, 28mpd 15 . . . . . 6 (𝐴 ∈ (ℕ0 × ℕ0) → (2nd ‘(𝑅‘(2nd𝐴))) = 0)
306, 29syl 17 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (2nd ‘(𝑅‘(2nd𝐴))) = 0)
3122, 30eqtr3d 2835 . . . 4 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (2nd ‘(𝑅𝑁)) = 0)
3231oveq2d 7158 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((1st ‘(𝑅𝑁)) gcd (2nd ‘(𝑅𝑁))) = ((1st ‘(𝑅𝑁)) gcd 0))
33 xp1st 7713 . . . 4 ((𝑅𝑁) ∈ (ℕ0 × ℕ0) → (1st ‘(𝑅𝑁)) ∈ ℕ0)
34 nn0gcdid0 15876 . . . 4 ((1st ‘(𝑅𝑁)) ∈ ℕ0 → ((1st ‘(𝑅𝑁)) gcd 0) = (1st ‘(𝑅𝑁)))
3512, 33, 343syl 18 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((1st ‘(𝑅𝑁)) gcd 0) = (1st ‘(𝑅𝑁)))
3617, 32, 353eqtrrd 2838 . 2 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (1st ‘(𝑅𝑁)) = ( gcd ‘(𝑅𝑁)))
377eucalginv 15935 . . . . . 6 (𝑧 ∈ (ℕ0 × ℕ0) → ( gcd ‘(𝐸𝑧)) = ( gcd ‘𝑧))
388ffvelrni 6834 . . . . . . 7 (𝑧 ∈ (ℕ0 × ℕ0) → (𝐸𝑧) ∈ (ℕ0 × ℕ0))
3938fvresd 6672 . . . . . 6 (𝑧 ∈ (ℕ0 × ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝐸𝑧)) = ( gcd ‘(𝐸𝑧)))
40 fvres 6671 . . . . . 6 (𝑧 ∈ (ℕ0 × ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘𝑧) = ( gcd ‘𝑧))
4137, 39, 403eqtr4d 2843 . . . . 5 (𝑧 ∈ (ℕ0 × ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝐸𝑧)) = (( gcd ↾ (ℕ0 × ℕ0))‘𝑧))
422, 8, 41alginv 15926 . . . 4 ((𝐴 ∈ (ℕ0 × ℕ0) ∧ 𝑁 ∈ ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅𝑁)) = (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅‘0)))
436, 42sylancom 591 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅𝑁)) = (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅‘0)))
4412fvresd 6672 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅𝑁)) = ( gcd ‘(𝑅𝑁)))
45 0nn0 11915 . . . . 5 0 ∈ ℕ0
46 ffvelrn 6833 . . . . 5 ((𝑅:ℕ0⟶(ℕ0 × ℕ0) ∧ 0 ∈ ℕ0) → (𝑅‘0) ∈ (ℕ0 × ℕ0))
4710, 45, 46sylancl 589 . . . 4 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅‘0) ∈ (ℕ0 × ℕ0))
4847fvresd 6672 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (( gcd ↾ (ℕ0 × ℕ0))‘(𝑅‘0)) = ( gcd ‘(𝑅‘0)))
4943, 44, 483eqtr3d 2841 . 2 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ( gcd ‘(𝑅𝑁)) = ( gcd ‘(𝑅‘0)))
501, 2, 3, 6algr0 15923 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅‘0) = 𝐴)
5150, 4eqtrdi 2849 . . . 4 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑅‘0) = ⟨𝑀, 𝑁⟩)
5251fveq2d 6656 . . 3 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ( gcd ‘(𝑅‘0)) = ( gcd ‘⟨𝑀, 𝑁⟩))
53 df-ov 7145 . . 3 (𝑀 gcd 𝑁) = ( gcd ‘⟨𝑀, 𝑁⟩)
5452, 53eqtr4di 2851 . 2 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ( gcd ‘(𝑅‘0)) = (𝑀 gcd 𝑁))
5536, 49, 543eqtrd 2837 1 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (1st ‘(𝑅𝑁)) = (𝑀 gcd 𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ifcif 4427  {csn 4527  ⟨cop 4533   × cxp 5520   ↾ cres 5524   ∘ ccom 5526  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142   ∈ cmpo 7144  1st c1st 7679  2nd c2nd 7680  0cc0 10541  ℕ0cn0 11900  ℤcz 11986  ℤ≥cuz 12248   mod cmo 13249  seqcseq 13381   gcd cgcd 15850 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-pre-sup 10619 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-sup 8905  df-inf 8906  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-div 11302  df-nn 11641  df-2 11703  df-3 11704  df-n0 11901  df-z 11987  df-uz 12249  df-rp 12395  df-fz 12903  df-fl 13174  df-mod 13250  df-seq 13382  df-exp 13443  df-cj 14467  df-re 14468  df-im 14469  df-sqrt 14603  df-abs 14604  df-dvds 15617  df-gcd 15851 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator