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	$$⊢E=\left(x\in {\mathbb{N}}_0,y\in {\mathbb{N}}_0⟼if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\right)$$
Assertion	eucalgval2	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to MEN=if\left(N=0,⟨M,N⟩,⟨N,M\mathrm{mod}N⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	$$⊢E=\left(x\in {\mathbb{N}}_0,y\in {\mathbb{N}}_0⟼if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\right)$$
2		simpr	$$⊢\left(x=M\wedge y=N\right)\to y=N$$
3	2	eqeq1d	$$⊢\left(x=M\wedge y=N\right)\to \left(y=0\leftrightarrow N=0\right)$$
4		opeq12	$$⊢\left(x=M\wedge y=N\right)\to ⟨x,y⟩=⟨M,N⟩$$
5		oveq12	$$⊢\left(x=M\wedge y=N\right)\to x\mathrm{mod}y=M\mathrm{mod}N$$
6	2 5	opeq12d	$$⊢\left(x=M\wedge y=N\right)\to ⟨y,x\mathrm{mod}y⟩=⟨N,M\mathrm{mod}N⟩$$
7	3 4 6	ifbieq12d	$$⊢\left(x=M\wedge y=N\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)=if\left(N=0,⟨M,N⟩,⟨N,M\mathrm{mod}N⟩\right)$$
8		opex	$$⊢⟨M,N⟩\in \mathrm{V}$$
9		opex	$$⊢⟨N,M\mathrm{mod}N⟩\in \mathrm{V}$$
10	8 9	ifex	$$⊢if\left(N=0,⟨M,N⟩,⟨N,M\mathrm{mod}N⟩\right)\in \mathrm{V}$$
11	7 1 10	ovmpoa	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to MEN=if\left(N=0,⟨M,N⟩,⟨N,M\mathrm{mod}N⟩\right)$$