Theorem 2sqlem1

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

	Ref	Expression
Hypothesis	2sq.1	$$⊢S=\mathrm{ran}\left(w\in \mathbb{Z}\left[i\right]⟼{\left|w\right|}^2\right)$$
Assertion	2sqlem1	$$⊢A\in S\leftrightarrow \exists x\in \mathbb{Z}\left[i\right]A={\left|x\right|}^2$$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$$⊢S=\mathrm{ran}\left(w\in \mathbb{Z}\left[i\right]⟼{\left|w\right|}^2\right)$$
2	1	eleq2i	$$⊢A\in S\leftrightarrow A\in \mathrm{ran}\left(w\in \mathbb{Z}\left[i\right]⟼{\left|w\right|}^2\right)$$
3		fveq2	$$⊢w=x\to \left|w\right|=\left|x\right|$$
4	3	oveq1d	$$⊢w=x\to {\left|w\right|}^2={\left|x\right|}^2$$
5	4	cbvmptv	$$⊢\left(w\in \mathbb{Z}\left[i\right]⟼{\left|w\right|}^2\right)=\left(x\in \mathbb{Z}\left[i\right]⟼{\left|x\right|}^2\right)$$
6		ovex	$$⊢{\left|x\right|}^2\in \mathrm{V}$$
7	5 6	elrnmpti	$$⊢A\in \mathrm{ran}\left(w\in \mathbb{Z}\left[i\right]⟼{\left|w\right|}^2\right)\leftrightarrow \exists x\in \mathbb{Z}\left[i\right]A={\left|x\right|}^2$$
8	2 7	bitri	$$⊢A\in S\leftrightarrow \exists x\in \mathbb{Z}\left[i\right]A={\left|x\right|}^2$$