Metamath Proof Explorer

Theorem 4sqlem4

Description: Lemma for 4sq . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Hypothesis 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion 4sqlem4 ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 1 4sqlem2 ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
3 gzreim ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + ( i · 𝑏 ) ) ∈ ℤ[i] )
4 3 adantr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 + ( i · 𝑏 ) ) ∈ ℤ[i] )
5 gzreim ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑐 + ( i · 𝑑 ) ) ∈ ℤ[i] )
6 5 adantl ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑐 + ( i · 𝑑 ) ) ∈ ℤ[i] )
7 gzcn ⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ∈ ℤ[i] → ( 𝑎 + ( i · 𝑏 ) ) ∈ ℂ )
8 3 7 syl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + ( i · 𝑏 ) ) ∈ ℂ )
9 8 absvalsq2d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) ) )
10 zre ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℝ )
11 zre ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℝ )
12 crre ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑎 )
13 10 11 12 syl2an ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑎 )
14 13 oveq1d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) = ( 𝑎 ↑ 2 ) )
15 crim ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑏 )
16 10 11 15 syl2an ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑏 )
17 16 oveq1d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) = ( 𝑏 ↑ 2 ) )
18 14 17 oveq12d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
19 9 18 eqtrd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
20 gzcn ⊢ ( ( 𝑐 + ( i · 𝑑 ) ) ∈ ℤ[i] → ( 𝑐 + ( i · 𝑑 ) ) ∈ ℂ )
21 5 20 syl ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑐 + ( i · 𝑑 ) ) ∈ ℂ )
22 21 absvalsq2d ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) )
23 zre ⊢ ( 𝑐 ∈ ℤ → 𝑐 ∈ ℝ )
24 zre ⊢ ( 𝑑 ∈ ℤ → 𝑑 ∈ ℝ )
25 crre ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ℜ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) = 𝑐 )
26 23 24 25 syl2an ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ℜ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) = 𝑐 )
27 26 oveq1d ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( ℜ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) = ( 𝑐 ↑ 2 ) )
28 crim ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ℑ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) = 𝑑 )
29 23 24 28 syl2an ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ℑ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) = 𝑑 )
30 29 oveq1d ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( ℑ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) = ( 𝑑 ↑ 2 ) )
31 27 30 oveq12d ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( ( ℜ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) = ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) )
32 22 31 eqtrd ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) = ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) )
33 19 32 oveqan12d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
34 33 eqcomd ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) )
35 fveq2 ⊢ ( 𝑢 = ( 𝑎 + ( i · 𝑏 ) ) → ( abs ‘ 𝑢 ) = ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) )
36 35 oveq1d ⊢ ( 𝑢 = ( 𝑎 + ( i · 𝑏 ) ) → ( ( abs ‘ 𝑢 ) ↑ 2 ) = ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) )
37 36 oveq1d ⊢ ( 𝑢 = ( 𝑎 + ( i · 𝑏 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )
38 37 eqeq2d ⊢ ( 𝑢 = ( 𝑎 + ( i · 𝑏 ) ) → ( ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ↔ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ) )
39 fveq2 ⊢ ( 𝑣 = ( 𝑐 + ( i · 𝑑 ) ) → ( abs ‘ 𝑣 ) = ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) )
40 39 oveq1d ⊢ ( 𝑣 = ( 𝑐 + ( i · 𝑑 ) ) → ( ( abs ‘ 𝑣 ) ↑ 2 ) = ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) )
41 40 oveq2d ⊢ ( 𝑣 = ( 𝑐 + ( i · 𝑑 ) ) → ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) )
42 41 eqeq2d ⊢ ( 𝑣 = ( 𝑐 + ( i · 𝑑 ) ) → ( ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ↔ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) ) )
43 38 42 rspc2ev ⊢ ( ( ( 𝑎 + ( i · 𝑏 ) ) ∈ ℤ[i] ∧ ( 𝑐 + ( i · 𝑑 ) ) ∈ ℤ[i] ∧ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝑎 + ( i · 𝑏 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑐 + ( i · 𝑑 ) ) ) ↑ 2 ) ) ) → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )
44 4 6 34 43 syl3anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )
45 eqeq1 ⊢ ( 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ( 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ↔ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ) )
46 45 2rexbidv ⊢ ( 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ( ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ↔ ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ) )
47 44 46 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ) )
48 47 rexlimdvva ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ) )
49 48 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )
50 2 49 sylbi ⊢ ( 𝐴 ∈ 𝑆 → ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )
51 1 4sqlem4a ⊢ ( ( 𝑢 ∈ ℤ[i] ∧ 𝑣 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ∈ 𝑆 )
52 eleq1a ⊢ ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) ∈ 𝑆 → ( 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) → 𝐴 ∈ 𝑆 ) )
53 51 52 syl ⊢ ( ( 𝑢 ∈ ℤ[i] ∧ 𝑣 ∈ ℤ[i] ) → ( 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) → 𝐴 ∈ 𝑆 ) )
54 53 rexlimivv ⊢ ( ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) → 𝐴 ∈ 𝑆 )
55 50 54 impbii ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑢 ∈ ℤ[i] ∃ 𝑣 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 𝑣 ) ↑ 2 ) ) )