Theorem 2sqlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		2sq.1	⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2	1	2sqlem1	⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑧 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
3		elgz	⊢ ( 𝑧 ∈ ℤ[i] ↔ ( 𝑧 ∈ ℂ ∧ ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ ( ℑ ‘ 𝑧 ) ∈ ℤ ) )
4	3	simp2bi	⊢ ( 𝑧 ∈ ℤ[i] → ( ℜ ‘ 𝑧 ) ∈ ℤ )
5	3	simp3bi	⊢ ( 𝑧 ∈ ℤ[i] → ( ℑ ‘ 𝑧 ) ∈ ℤ )
6		gzcn	⊢ ( 𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ )
7	6	absvalsq2d	⊢ ( 𝑧 ∈ ℤ[i] → ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) )
8		oveq1	⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( 𝑥 ↑ 2 ) = ( ( ℜ ‘ 𝑧 ) ↑ 2 ) )
9	8	oveq1d	⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
10	9	eqeq2d	⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
11		oveq1	⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( 𝑦 ↑ 2 ) = ( ( ℑ ‘ 𝑧 ) ↑ 2 ) )
12	11	oveq2d	⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) )
13	12	eqeq2d	⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) ) )
14	10 13	rspc2ev	⊢ ( ( ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ ( ℑ ‘ 𝑧 ) ∈ ℤ ∧ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
15	4 5 7 14	syl3anc	⊢ ( 𝑧 ∈ ℤ[i] → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
16		eqeq1	⊢ ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
17	16	2rexbidv	⊢ ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
18	15 17	syl5ibrcom	⊢ ( 𝑧 ∈ ℤ[i] → ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
19	18	rexlimiv	⊢ ( ∃ 𝑧 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
20	2 19	sylbi	⊢ ( 𝐴 ∈ 𝑆 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
21		gzreim	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℤ[i] )
22		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
23		ax-icn	⊢ i ∈ ℂ
24		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
25		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
26	23 24 25	sylancr	⊢ ( 𝑦 ∈ ℤ → ( i · 𝑦 ) ∈ ℂ )
27		addcl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
28	22 26 27	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
29	28	absvalsq2d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) )
30		zre	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
31		zre	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
32		crre	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
33	30 31 32	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
34	33	oveq1d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
35		crim	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
36	30 31 35	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
37	36	oveq1d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( 𝑦 ↑ 2 ) )
38	34 37	oveq12d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
39	29 38	eqtr2d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) )
40		fveq2	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( abs ‘ 𝑧 ) = ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) )
41	40	oveq1d	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) )
42	41	rspceeqv	⊢ ( ( ( 𝑥 + ( i · 𝑦 ) ) ∈ ℤ[i] ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) → ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
43	21 39 42	syl2anc	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
44	1	2sqlem1	⊢ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 ↔ ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
45	43 44	sylibr	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 )
46		eleq1	⊢ ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → ( 𝐴 ∈ 𝑆 ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 ) )
47	45 46	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → 𝐴 ∈ 𝑆 ) )
48	47	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → 𝐴 ∈ 𝑆 )
49	20 48	impbii	⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )