Metamath Proof Explorer

Theorem 4sqlem13

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses 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 ) ) ) }
4sq.2 
|- ( ph -> N e. NN )
4sq.3 
|- ( ph -> P = ( ( 2 x. N ) + 1 ) )
4sq.4 
|- ( ph -> P e. Prime )
4sq.5 
|- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
4sq.6 
|- T = { i e. NN | ( i x. P ) e. S }
4sq.7 
|- M = inf ( T , RR , < )
Assertion 4sqlem13 
|- ( ph -> ( T =/= (/) /\ M < P ) )

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 4sq.2 
 |-  ( ph -> N e. NN )
3 4sq.3 
 |-  ( ph -> P = ( ( 2 x. N ) + 1 ) )
4 4sq.4 
 |-  ( ph -> P e. Prime )
5 4sq.5 
 |-  ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
6 4sq.6 
 |-  T = { i e. NN | ( i x. P ) e. S }
7 4sq.7 
 |-  M = inf ( T , RR , < )
8 eqid 
 |-  { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) } = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }
9 eqid 
 |-  ( v e. { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) } |-> ( ( P - 1 ) - v ) ) = ( v e. { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) } |-> ( ( P - 1 ) - v ) )
10 1 2 3 4 8 9 4sqlem12 
 |-  ( ph -> E. k e. ( 1 ... ( P - 1 ) ) E. u e. Z[i] ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) )
11 simplrl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> k e. ( 1 ... ( P - 1 ) ) )
12 elfznn 
 |-  ( k e. ( 1 ... ( P - 1 ) ) -> k e. NN )
13 11 12 syl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> k e. NN )
14 simpr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) )
15 abs1 
 |-  ( abs ` 1 ) = 1
16 15 oveq1i 
 |-  ( ( abs ` 1 ) ^ 2 ) = ( 1 ^ 2 )
17 sq1 
 |-  ( 1 ^ 2 ) = 1
18 16 17 eqtri 
 |-  ( ( abs ` 1 ) ^ 2 ) = 1
19 18 oveq2i 
 |-  ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) = ( ( ( abs ` u ) ^ 2 ) + 1 )
20 simplrr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> u e. Z[i] )
21 1z 
 |-  1 e. ZZ
22 zgz 
 |-  ( 1 e. ZZ -> 1 e. Z[i] )
23 21 22 ax-mp 
 |-  1 e. Z[i]
24 1 4sqlem4a 
 |-  ( ( u e. Z[i] /\ 1 e. Z[i] ) -> ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) e. S )
25 20 23 24 sylancl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` 1 ) ^ 2 ) ) e. S )
26 19 25 eqeltrrid 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( ( ( abs ` u ) ^ 2 ) + 1 ) e. S )
27 14 26 eqeltrrd 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( k x. P ) e. S )
28 oveq1 
 |-  ( i = k -> ( i x. P ) = ( k x. P ) )
29 28 eleq1d 
 |-  ( i = k -> ( ( i x. P ) e. S <-> ( k x. P ) e. S ) )
30 29 6 elrab2 
 |-  ( k e. T <-> ( k e. NN /\ ( k x. P ) e. S ) )
31 13 27 30 sylanbrc 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> k e. T )
32 31 ne0d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> T =/= (/) )
33 6 ssrab3 
 |-  T C_ NN
34 nnuz 
 |-  NN = ( ZZ>= ` 1 )
35 33 34 sseqtri 
 |-  T C_ ( ZZ>= ` 1 )
36 infssuzcl 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )
37 35 32 36 sylancr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> inf ( T , RR , < ) e. T )
38 7 37 eqeltrid 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> M e. T )
39 33 38 sseldi 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> M e. NN )
40 39 nnred 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> M e. RR )
41 13 nnred 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> k e. RR )
42 4 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> P e. Prime )
43 prmnn 
 |-  ( P e. Prime -> P e. NN )
44 42 43 syl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> P e. NN )
45 44 nnred 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> P e. RR )
46 infssuzle 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ k e. T ) -> inf ( T , RR , < ) <_ k )
47 35 31 46 sylancr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> inf ( T , RR , < ) <_ k )
48 7 47 eqbrtrid 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> M <_ k )
49 prmz 
 |-  ( P e. Prime -> P e. ZZ )
50 42 49 syl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> P e. ZZ )
51 elfzm11 
 |-  ( ( 1 e. ZZ /\ P e. ZZ ) -> ( k e. ( 1 ... ( P - 1 ) ) <-> ( k e. ZZ /\ 1 <_ k /\ k < P ) ) )
52 21 50 51 sylancr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( k e. ( 1 ... ( P - 1 ) ) <-> ( k e. ZZ /\ 1 <_ k /\ k < P ) ) )
53 11 52 mpbid 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( k e. ZZ /\ 1 <_ k /\ k < P ) )
54 53 simp3d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> k < P )
55 40 41 45 48 54 lelttrd 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> M < P )
56 32 55 jca 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) /\ ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) -> ( T =/= (/) /\ M < P ) )
57 56 ex 
 |-  ( ( ph /\ ( k e. ( 1 ... ( P - 1 ) ) /\ u e. Z[i] ) ) -> ( ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) -> ( T =/= (/) /\ M < P ) ) )
58 57 rexlimdvva 
 |-  ( ph -> ( E. k e. ( 1 ... ( P - 1 ) ) E. u e. Z[i] ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) -> ( T =/= (/) /\ M < P ) ) )
59 10 58 mpd 
 |-  ( ph -> ( T =/= (/) /\ M < P ) )