Theorem eucalgval2

Description: The value of the step function E for Euclid's Algorithm on an ordered pair. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypothesis	eucalgval.1	⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
Assertion	eucalgval2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 𝐸 𝑁 ) = if ( 𝑁 = 0 , ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
2		simpr	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → 𝑦 = 𝑁 )
3	2	eqeq1d	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → ( 𝑦 = 0 ↔ 𝑁 = 0 ) )
4		opeq12	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ )
5		oveq12	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → ( 𝑥 mod 𝑦 ) = ( 𝑀 mod 𝑁 ) )
6	2 5	opeq12d	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ = ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ )
7	3 4 6	ifbieq12d	⊢ ( ( 𝑥 = 𝑀 ∧ 𝑦 = 𝑁 ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) = if ( 𝑁 = 0 , ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ ) )
8		opex	⊢ ⟨ 𝑀 , 𝑁 ⟩ ∈ V
9		opex	⊢ ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ ∈ V
10	8 9	ifex	⊢ if ( 𝑁 = 0 , ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ ) ∈ V
11	7 1 10	ovmpoa	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 𝐸 𝑁 ) = if ( 𝑁 = 0 , ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑁 , ( 𝑀 mod 𝑁 ) ⟩ ) )