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 
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
Assertion 4sqlem4 
|- ( A e. S <-> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 4sq.1 
 |-  S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2 1 4sqlem2 
 |-  ( A e. S <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
3 gzreim 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + ( _i x. b ) ) e. Z[i] )
4 3 adantr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a + ( _i x. b ) ) e. Z[i] )
5 gzreim 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( c + ( _i x. d ) ) e. Z[i] )
6 5 adantl 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( c + ( _i x. d ) ) e. Z[i] )
7 gzcn 
 |-  ( ( a + ( _i x. b ) ) e. Z[i] -> ( a + ( _i x. b ) ) e. CC )
8 3 7 syl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + ( _i x. b ) ) e. CC )
9 8 absvalsq2d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) = ( ( ( Re ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( Im ` ( a + ( _i x. b ) ) ) ^ 2 ) ) )
10 zre 
 |-  ( a e. ZZ -> a e. RR )
11 zre 
 |-  ( b e. ZZ -> b e. RR )
12 crre 
 |-  ( ( a e. RR /\ b e. RR ) -> ( Re ` ( a + ( _i x. b ) ) ) = a )
13 10 11 12 syl2an 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( Re ` ( a + ( _i x. b ) ) ) = a )
14 13 oveq1d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( Re ` ( a + ( _i x. b ) ) ) ^ 2 ) = ( a ^ 2 ) )
15 crim 
 |-  ( ( a e. RR /\ b e. RR ) -> ( Im ` ( a + ( _i x. b ) ) ) = b )
16 10 11 15 syl2an 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( Im ` ( a + ( _i x. b ) ) ) = b )
17 16 oveq1d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( Im ` ( a + ( _i x. b ) ) ) ^ 2 ) = ( b ^ 2 ) )
18 14 17 oveq12d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( ( Re ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( Im ` ( a + ( _i x. b ) ) ) ^ 2 ) ) = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
19 9 18 eqtrd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
20 gzcn 
 |-  ( ( c + ( _i x. d ) ) e. Z[i] -> ( c + ( _i x. d ) ) e. CC )
21 5 20 syl 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( c + ( _i x. d ) ) e. CC )
22 21 absvalsq2d 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) = ( ( ( Re ` ( c + ( _i x. d ) ) ) ^ 2 ) + ( ( Im ` ( c + ( _i x. d ) ) ) ^ 2 ) ) )
23 zre 
 |-  ( c e. ZZ -> c e. RR )
24 zre 
 |-  ( d e. ZZ -> d e. RR )
25 crre 
 |-  ( ( c e. RR /\ d e. RR ) -> ( Re ` ( c + ( _i x. d ) ) ) = c )
26 23 24 25 syl2an 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( Re ` ( c + ( _i x. d ) ) ) = c )
27 26 oveq1d 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( ( Re ` ( c + ( _i x. d ) ) ) ^ 2 ) = ( c ^ 2 ) )
28 crim 
 |-  ( ( c e. RR /\ d e. RR ) -> ( Im ` ( c + ( _i x. d ) ) ) = d )
29 23 24 28 syl2an 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( Im ` ( c + ( _i x. d ) ) ) = d )
30 29 oveq1d 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( ( Im ` ( c + ( _i x. d ) ) ) ^ 2 ) = ( d ^ 2 ) )
31 27 30 oveq12d 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( ( ( Re ` ( c + ( _i x. d ) ) ) ^ 2 ) + ( ( Im ` ( c + ( _i x. d ) ) ) ^ 2 ) ) = ( ( c ^ 2 ) + ( d ^ 2 ) ) )
32 22 31 eqtrd 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) = ( ( c ^ 2 ) + ( d ^ 2 ) ) )
33 19 32 oveqan12d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
34 33 eqcomd 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) ) )
35 fveq2 
 |-  ( u = ( a + ( _i x. b ) ) -> ( abs ` u ) = ( abs ` ( a + ( _i x. b ) ) ) )
36 35 oveq1d 
 |-  ( u = ( a + ( _i x. b ) ) -> ( ( abs ` u ) ^ 2 ) = ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) )
37 36 oveq1d 
 |-  ( u = ( a + ( _i x. b ) ) -> ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
38 37 eqeq2d 
 |-  ( u = ( a + ( _i x. b ) ) -> ( ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) <-> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) ) )
39 fveq2 
 |-  ( v = ( c + ( _i x. d ) ) -> ( abs ` v ) = ( abs ` ( c + ( _i x. d ) ) ) )
40 39 oveq1d 
 |-  ( v = ( c + ( _i x. d ) ) -> ( ( abs ` v ) ^ 2 ) = ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) )
41 40 oveq2d 
 |-  ( v = ( c + ( _i x. d ) ) -> ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) ) )
42 41 eqeq2d 
 |-  ( v = ( c + ( _i x. d ) ) -> ( ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) <-> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) ) ) )
43 38 42 rspc2ev 
 |-  ( ( ( a + ( _i x. b ) ) e. Z[i] /\ ( c + ( _i x. d ) ) e. Z[i] /\ ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` ( a + ( _i x. b ) ) ) ^ 2 ) + ( ( abs ` ( c + ( _i x. d ) ) ) ^ 2 ) ) ) -> E. u e. Z[i] E. v e. Z[i] ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
44 4 6 34 43 syl3anc 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> E. u e. Z[i] E. v e. Z[i] ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
45 eqeq1 
 |-  ( A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> ( A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) <-> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) ) )
46 45 2rexbidv 
 |-  ( A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> ( E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) <-> E. u e. Z[i] E. v e. Z[i] ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) ) )
47 44 46 syl5ibrcom 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) ) )
48 47 rexlimdvva 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) ) )
49 48 rexlimivv 
 |-  ( E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
50 2 49 sylbi 
 |-  ( A e. S -> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
51 1 4sqlem4a 
 |-  ( ( u e. Z[i] /\ v e. Z[i] ) -> ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) e. S )
52 eleq1a 
 |-  ( ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) e. S -> ( A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) -> A e. S ) )
53 51 52 syl 
 |-  ( ( u e. Z[i] /\ v e. Z[i] ) -> ( A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) -> A e. S ) )
54 53 rexlimivv 
 |-  ( E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) -> A e. S )
55 50 54 impbii 
 |-  ( A e. S <-> E. u e. Z[i] E. v e. Z[i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )