eucalgval - Metamath Proof Explorer

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

Theorem eucalgval 16592

Description: Euclid's Algorithm eucalg 16597 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.

The value of the step function 𝐸 for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

**Hypothesis**
Ref	Expression
eucalgval.1	⊢ 𝐸 = (𝑥 ∈ ℕ₀, 𝑦 ∈ ℕ₀ ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))

**Assertion**
Ref	Expression
eucalgval	⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (𝐸‘𝑋) = if((2^nd ‘𝑋) = 0, 𝑋, ⟨(2^nd ‘𝑋), ( mod ‘𝑋)⟩))

Distinct variable group: 𝑥,𝑦,𝑋 Allowed substitution hints: 𝐸(𝑥,𝑦)

**Proof of Theorem eucalgval**
Step	Hyp	Ref	Expression
1		df-ov 7388	. . 3 ⊢ ((1^st ‘𝑋)𝐸(2^nd ‘𝑋)) = (𝐸‘⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩)
2		xp1st 7991	. . . 4 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (1^st ‘𝑋) ∈ ℕ₀)
3		xp2nd 7992	. . . 4 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (2^nd ‘𝑋) ∈ ℕ₀)
4		eucalgval.1	. . . . 5 ⊢ 𝐸 = (𝑥 ∈ ℕ₀, 𝑦 ∈ ℕ₀ ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))
5	4	eucalgval2 16591	. . . 4 ⊢ (((1^st ‘𝑋) ∈ ℕ₀ ∧ (2^nd ‘𝑋) ∈ ℕ₀) → ((1^st ‘𝑋)𝐸(2^nd ‘𝑋)) = if((2^nd ‘𝑋) = 0, ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩, ⟨(2^nd ‘𝑋), ((1^st ‘𝑋) mod (2^nd ‘𝑋))⟩))
6	2, 3, 5	syl2anc 592	. . 3 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → ((1^st ‘𝑋)𝐸(2^nd ‘𝑋)) = if((2^nd ‘𝑋) = 0, ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩, ⟨(2^nd ‘𝑋), ((1^st ‘𝑋) mod (2^nd ‘𝑋))⟩))
7	1, 6	eqtr3id 2805	. 2 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (𝐸‘⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩) = if((2^nd ‘𝑋) = 0, ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩, ⟨(2^nd ‘𝑋), ((1^st ‘𝑋) mod (2^nd ‘𝑋))⟩))
8		1st2nd2 7998	. . 3 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → 𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩)
9	8	fveq2d 6860	. 2 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (𝐸‘𝑋) = (𝐸‘⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩))
10	8	fveq2d 6860	. . . . 5 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → ( mod ‘𝑋) = ( mod ‘⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩))
11		df-ov 7388	. . . . 5 ⊢ ((1^st ‘𝑋) mod (2^nd ‘𝑋)) = ( mod ‘⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩)
12	10, 11	eqtr4di 2809	. . . 4 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → ( mod ‘𝑋) = ((1^st ‘𝑋) mod (2^nd ‘𝑋)))
13	12	opeq2d 4832	. . 3 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → ⟨(2^nd ‘𝑋), ( mod ‘𝑋)⟩ = ⟨(2^nd ‘𝑋), ((1^st ‘𝑋) mod (2^nd ‘𝑋))⟩)
14	8, 13	ifeq12d 4496	. 2 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → if((2^nd ‘𝑋) = 0, 𝑋, ⟨(2^nd ‘𝑋), ( mod ‘𝑋)⟩) = if((2^nd ‘𝑋) = 0, ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩, ⟨(2^nd ‘𝑋), ((1^st ‘𝑋) mod (2^nd ‘𝑋))⟩))
15	7, 9, 14	3eqtr4d 2801	1 ⊢ (𝑋 ∈ (ℕ₀ × ℕ₀) → (𝐸‘𝑋) = if((2^nd ‘𝑋) = 0, 𝑋, ⟨(2^nd ‘𝑋), ( mod ‘𝑋)⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1554 ∈ wcel 2136 ifcif 4474 ⟨cop 4582 × cxp 5638 ‘cfv 6510 (class class class)co 7385 ∈ cmpo 7387 1^st c1st 7957 2^nd c2nd 7958 0cc0 11063 ℕ₀cn0 12471 mod cmo 13869

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-sep 5240 ax-nul 5250 ax-pr 5384 ax-un 7707

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-ral 3071 df-rex 3081 df-rab 3409 df-v 3450 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4281 df-if 4475 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-br 5095 df-opab 5157 df-mpt 5176 df-id 5535 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-iota 6466 df-fun 6512 df-fv 6518 df-ov 7388 df-oprab 7389 df-mpo 7390 df-1st 7959 df-2nd 7960

This theorem is referenced by: eucalginv 16594 eucalglt 16595

W3C validator