Theorem eucalgf

Description: Domain and codomain of the step function E for Euclid's Algorithm. (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	eucalgf	$$⊢E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$

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		nnne0	$$⊢y\in \mathbb{N}\to y\ne 0$$
3	2	adantl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to y\ne 0$$
4	3	neneqd	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to \neg y=0$$
5	4	iffalsed	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)=⟨y,x\mathrm{mod}y⟩$$
6		nnnn0	$$⊢y\in \mathbb{N}\to y\in {\mathbb{N}}_0$$
7	6	adantl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to y\in {\mathbb{N}}_0$$
8		nn0z	$$⊢x\in {\mathbb{N}}_0\to x\in \mathbb{Z}$$
9		zmodcl	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{N}\right)\to x\mathrm{mod}y\in {\mathbb{N}}_0$$
10	8 9	sylan	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to x\mathrm{mod}y\in {\mathbb{N}}_0$$
11	7 10	opelxpd	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to ⟨y,x\mathrm{mod}y⟩\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
12	5 11	eqeltrd	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
13	12	adantlr	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge y\in \mathbb{N}\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
14		iftrue	$$⊢y=0\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)=⟨x,y⟩$$
15	14	adantl	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge y=0\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)=⟨x,y⟩$$
16		opelxpi	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to ⟨x,y⟩\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
17	16	adantr	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge y=0\right)\to ⟨x,y⟩\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
18	15 17	eqeltrd	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge y=0\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
19		elnn0	$$⊢y\in {\mathbb{N}}_0\leftrightarrow \left(y\in \mathbb{N}\vee y=0\right)$$
20	19	bilani	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \left(y\in \mathbb{N}\vee y=0\right)$$
21	13 18 20	mpjaodan	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
22	21	rgen2	$$⊢\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_{0}if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
23	1	fmpo	$$⊢\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_{0}if\left(y=0,⟨x,y⟩,⟨y,x\mathrm{mod}y⟩\right)\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\leftrightarrow E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$
24	22 23	mpbi	$$⊢E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶{\mathbb{N}}_0\times {\mathbb{N}}_0$$