Metamath Proof Explorer

Theorem 4sqlem19

Description: Lemma for 4sq . The proof is by strong induction - we show that if all the integers less than k are in S , then k is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 . If k is 0 , 1 , 2 , we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq k e. S . (Contributed by Mario Carneiro, 14-Jul-2014) (Revised by Mario Carneiro, 20-Jun-2015)

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 4sqlem19 
|- NN0 = S

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 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
3 eleq1 
 |-  ( j = 1 -> ( j e. S <-> 1 e. S ) )
4 eleq1 
 |-  ( j = m -> ( j e. S <-> m e. S ) )
5 eleq1 
 |-  ( j = i -> ( j e. S <-> i e. S ) )
6 eleq1 
 |-  ( j = ( m x. i ) -> ( j e. S <-> ( m x. i ) e. S ) )
7 eleq1 
 |-  ( j = k -> ( j e. S <-> k e. S ) )
8 abs1 
 |-  ( abs ` 1 ) = 1
9 8 oveq1i 
 |-  ( ( abs ` 1 ) ^ 2 ) = ( 1 ^ 2 )
10 sq1 
 |-  ( 1 ^ 2 ) = 1
11 9 10 eqtri 
 |-  ( ( abs ` 1 ) ^ 2 ) = 1
12 abs0 
 |-  ( abs ` 0 ) = 0
13 12 oveq1i 
 |-  ( ( abs ` 0 ) ^ 2 ) = ( 0 ^ 2 )
14 sq0 
 |-  ( 0 ^ 2 ) = 0
15 13 14 eqtri 
 |-  ( ( abs ` 0 ) ^ 2 ) = 0
16 11 15 oveq12i 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) = ( 1 + 0 )
17 1p0e1 
 |-  ( 1 + 0 ) = 1
18 16 17 eqtri 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) = 1
19 1z 
 |-  1 e. ZZ
20 zgz 
 |-  ( 1 e. ZZ -> 1 e. Z[i] )
21 19 20 ax-mp 
 |-  1 e. Z[i]
22 0z 
 |-  0 e. ZZ
23 zgz 
 |-  ( 0 e. ZZ -> 0 e. Z[i] )
24 22 23 ax-mp 
 |-  0 e. Z[i]
25 1 4sqlem4a 
 |-  ( ( 1 e. Z[i] /\ 0 e. Z[i] ) -> ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) e. S )
26 21 24 25 mp2an 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) e. S
27 18 26 eqeltrri 
 |-  1 e. S
28 eleq1 
 |-  ( j = 2 -> ( j e. S <-> 2 e. S ) )
29 eldifsn 
 |-  ( j e. ( Prime \ { 2 } ) <-> ( j e. Prime /\ j =/= 2 ) )
30 oddprm 
 |-  ( j e. ( Prime \ { 2 } ) -> ( ( j - 1 ) / 2 ) e. NN )
31 30 adantr 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( ( j - 1 ) / 2 ) e. NN )
32 eldifi 
 |-  ( j e. ( Prime \ { 2 } ) -> j e. Prime )
33 32 adantr 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j e. Prime )
34 prmnn 
 |-  ( j e. Prime -> j e. NN )
35 nncn 
 |-  ( j e. NN -> j e. CC )
36 33 34 35 3syl 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j e. CC )
37 ax-1cn 
 |-  1 e. CC
38 subcl 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( j - 1 ) e. CC )
39 36 37 38 sylancl 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( j - 1 ) e. CC )
40 2cnd 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> 2 e. CC )
41 2ne0 
 |-  2 =/= 0
42 41 a1i 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> 2 =/= 0 )
43 39 40 42 divcan2d 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 2 x. ( ( j - 1 ) / 2 ) ) = ( j - 1 ) )
44 43 oveq1d 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( ( 2 x. ( ( j - 1 ) / 2 ) ) + 1 ) = ( ( j - 1 ) + 1 ) )
45 npcan 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j - 1 ) + 1 ) = j )
46 36 37 45 sylancl 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( ( j - 1 ) + 1 ) = j )
47 44 46 eqtr2d 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j = ( ( 2 x. ( ( j - 1 ) / 2 ) ) + 1 ) )
48 43 oveq2d 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 0 ... ( 2 x. ( ( j - 1 ) / 2 ) ) ) = ( 0 ... ( j - 1 ) ) )
49 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
50 33 34 49 3syl 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( j - 1 ) e. NN0 )
51 elnn0uz 
 |-  ( ( j - 1 ) e. NN0 <-> ( j - 1 ) e. ( ZZ>= ` 0 ) )
52 50 51 sylib 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
53 eluzfz1 
 |-  ( ( j - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( j - 1 ) ) )
54 fzsplit 
 |-  ( 0 e. ( 0 ... ( j - 1 ) ) -> ( 0 ... ( j - 1 ) ) = ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... ( j - 1 ) ) ) )
55 52 53 54 3syl 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 0 ... ( j - 1 ) ) = ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... ( j - 1 ) ) ) )
56 48 55 eqtrd 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 0 ... ( 2 x. ( ( j - 1 ) / 2 ) ) ) = ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... ( j - 1 ) ) ) )
57 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
58 15 15 oveq12i 
 |-  ( ( ( abs ` 0 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) = ( 0 + 0 )
59 00id 
 |-  ( 0 + 0 ) = 0
60 58 59 eqtri 
 |-  ( ( ( abs ` 0 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) = 0
61 1 4sqlem4a 
 |-  ( ( 0 e. Z[i] /\ 0 e. Z[i] ) -> ( ( ( abs ` 0 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) e. S )
62 24 24 61 mp2an 
 |-  ( ( ( abs ` 0 ) ^ 2 ) + ( ( abs ` 0 ) ^ 2 ) ) e. S
63 60 62 eqeltrri 
 |-  0 e. S
64 snssi 
 |-  ( 0 e. S -> { 0 } C_ S )
65 63 64 ax-mp 
 |-  { 0 } C_ S
66 57 65 eqsstri 
 |-  ( 0 ... 0 ) C_ S
67 66 a1i 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 0 ... 0 ) C_ S )
68 0p1e1 
 |-  ( 0 + 1 ) = 1
69 68 oveq1i 
 |-  ( ( 0 + 1 ) ... ( j - 1 ) ) = ( 1 ... ( j - 1 ) )
70 simpr 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> A. m e. ( 1 ... ( j - 1 ) ) m e. S )
71 dfss3 
 |-  ( ( 1 ... ( j - 1 ) ) C_ S <-> A. m e. ( 1 ... ( j - 1 ) ) m e. S )
72 70 71 sylibr 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 1 ... ( j - 1 ) ) C_ S )
73 69 72 eqsstrid 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( ( 0 + 1 ) ... ( j - 1 ) ) C_ S )
74 67 73 unssd 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... ( j - 1 ) ) ) C_ S )
75 56 74 eqsstrd 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> ( 0 ... ( 2 x. ( ( j - 1 ) / 2 ) ) ) C_ S )
76 oveq1 
 |-  ( k = i -> ( k x. j ) = ( i x. j ) )
77 76 eleq1d 
 |-  ( k = i -> ( ( k x. j ) e. S <-> ( i x. j ) e. S ) )
78 77 cbvrabv 
 |-  { k e. NN | ( k x. j ) e. S } = { i e. NN | ( i x. j ) e. S }
79 eqid 
 |-  inf ( { k e. NN | ( k x. j ) e. S } , RR , < ) = inf ( { k e. NN | ( k x. j ) e. S } , RR , < )
80 1 31 47 33 75 78 79 4sqlem18 
 |-  ( ( j e. ( Prime \ { 2 } ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j e. S )
81 29 80 sylanbr 
 |-  ( ( ( j e. Prime /\ j =/= 2 ) /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j e. S )
82 81 an32s 
 |-  ( ( ( j e. Prime /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) /\ j =/= 2 ) -> j e. S )
83 11 11 oveq12i 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) = ( 1 + 1 )
84 df-2 
 |-  2 = ( 1 + 1 )
85 83 84 eqtr4i 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) = 2
86 1 4sqlem4a 
 |-  ( ( 1 e. Z[i] /\ 1 e. Z[i] ) -> ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) e. S )
87 21 21 86 mp2an 
 |-  ( ( ( abs ` 1 ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) e. S
88 85 87 eqeltrri 
 |-  2 e. S
89 88 a1i 
 |-  ( ( j e. Prime /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> 2 e. S )
90 28 82 89 pm2.61ne 
 |-  ( ( j e. Prime /\ A. m e. ( 1 ... ( j - 1 ) ) m e. S ) -> j e. S )
91 1 mul4sq 
 |-  ( ( m e. S /\ i e. S ) -> ( m x. i ) e. S )
92 91 a1i 
 |-  ( ( m e. ( ZZ>= ` 2 ) /\ i e. ( ZZ>= ` 2 ) ) -> ( ( m e. S /\ i e. S ) -> ( m x. i ) e. S ) )
93 3 4 5 6 7 27 90 92 prmind2 
 |-  ( k e. NN -> k e. S )
94 id 
 |-  ( k = 0 -> k = 0 )
95 94 63 eqeltrdi 
 |-  ( k = 0 -> k e. S )
96 93 95 jaoi 
 |-  ( ( k e. NN \/ k = 0 ) -> k e. S )
97 2 96 sylbi 
 |-  ( k e. NN0 -> k e. S )
98 97 ssriv 
 |-  NN0 C_ S
99 1 4sqlem1 
 |-  S C_ NN0
100 98 99 eqssi 
 |-  NN0 = S