Theorem 2sqlem1

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

	Ref	Expression
Hypothesis	2sq.1	⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
Assertion	2sqlem1	⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2sq.1	⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝑆 ↔ 𝐴 ∈ ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) )
3		fveq2	⊢ ( 𝑤 = 𝑥 → ( abs ‘ 𝑤 ) = ( abs ‘ 𝑥 ) )
4	3	oveq1d	⊢ ( 𝑤 = 𝑥 → ( ( abs ‘ 𝑤 ) ↑ 2 ) = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
5	4	cbvmptv	⊢ ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) = ( 𝑥 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑥 ) ↑ 2 ) )
6		ovex	⊢ ( ( abs ‘ 𝑥 ) ↑ 2 ) ∈ V
7	5 6	elrnmpti	⊢ ( 𝐴 ∈ ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) ↔ ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
8	2 7	bitri	⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )