Theorem dfz2

Description: Alternative definition of the integers, based on elz2 . (Contributed by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	dfz2	$$⊢\mathbb{Z}=-\left[\mathbb{N}\times \mathbb{N}\right]$$

Proof

Step	Hyp	Ref	Expression
1		elz2	$$⊢x\in \mathbb{Z}\leftrightarrow \exists y\in \mathbb{N}\exists z\in \mathbb{N}x=y-z$$
2		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
3		ffn	$$⊢-:ℂ\times ℂ⟶ℂ\to -Fn\left(ℂ\times ℂ\right)$$
4	2 3	ax-mp	$$⊢-Fn\left(ℂ\times ℂ\right)$$
5		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
6		xpss12	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \mathbb{N}\subseteq ℂ\right)\to \mathbb{N}\times \mathbb{N}\subseteq ℂ\times ℂ$$
7	5 5 6	mp2an	$$⊢\mathbb{N}\times \mathbb{N}\subseteq ℂ\times ℂ$$
8		ovelimab	$$⊢\left(-Fn\left(ℂ\times ℂ\right)\wedge \mathbb{N}\times \mathbb{N}\subseteq ℂ\times ℂ\right)\to \left(x\in -\left[\mathbb{N}\times \mathbb{N}\right]\leftrightarrow \exists y\in \mathbb{N}\exists z\in \mathbb{N}x=y-z\right)$$
9	4 7 8	mp2an	$$⊢x\in -\left[\mathbb{N}\times \mathbb{N}\right]\leftrightarrow \exists y\in \mathbb{N}\exists z\in \mathbb{N}x=y-z$$
10	1 9	bitr4i	$$⊢x\in \mathbb{Z}\leftrightarrow x\in -\left[\mathbb{N}\times \mathbb{N}\right]$$
11	10	eqriv	$$⊢\mathbb{Z}=-\left[\mathbb{N}\times \mathbb{N}\right]$$