Metamath Proof Explorer

Theorem 4sqlem18

Description: Lemma for 4sq . Inductive step, odd prime case. (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 4sqlem18 
|- ( ph -> P e. 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 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 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 4 8 syl 
 |-  ( ph -> P e. NN )
10 9 nncnd 
 |-  ( ph -> P e. CC )
11 10 mulid2d 
 |-  ( ph -> ( 1 x. P ) = P )
12 6 ssrab3 
 |-  T C_ NN
13 nnuz 
 |-  NN = ( ZZ>= ` 1 )
14 12 13 sseqtri 
 |-  T C_ ( ZZ>= ` 1 )
15 1 2 3 4 5 6 7 4sqlem13 
 |-  ( ph -> ( T =/= (/) /\ M < P ) )
16 15 simpld 
 |-  ( ph -> T =/= (/) )
17 infssuzcl 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )
18 14 16 17 sylancr 
 |-  ( ph -> inf ( T , RR , < ) e. T )
19 7 18 eqeltrid 
 |-  ( ph -> M e. T )
20 oveq1 
 |-  ( i = M -> ( i x. P ) = ( M x. P ) )
21 20 eleq1d 
 |-  ( i = M -> ( ( i x. P ) e. S <-> ( M x. P ) e. S ) )
22 21 6 elrab2 
 |-  ( M e. T <-> ( M e. NN /\ ( M x. P ) e. S ) )
23 19 22 sylib 
 |-  ( ph -> ( M e. NN /\ ( M x. P ) e. S ) )
24 23 simprd 
 |-  ( ph -> ( M x. P ) e. S )
25 1 4sqlem2 
 |-  ( ( M x. P ) e. S <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
26 24 25 sylib 
 |-  ( ph -> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ M e. ( ZZ>= ` 2 ) ) -> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
28 simp1l 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> ph )
29 28 2 syl 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> N e. NN )
30 28 3 syl 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> P = ( ( 2 x. N ) + 1 ) )
31 28 4 syl 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> P e. Prime )
32 28 5 syl 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> ( 0 ... ( 2 x. N ) ) C_ S )
33 simp1r 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> M e. ( ZZ>= ` 2 ) )
34 simp2ll 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> a e. ZZ )
35 simp2lr 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> b e. ZZ )
36 simp2rl 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> c e. ZZ )
37 simp2rr 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> d e. ZZ )
38 eqid 
 |-  ( ( ( a + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( a + ( M / 2 ) ) mod M ) - ( M / 2 ) )
39 eqid 
 |-  ( ( ( b + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( b + ( M / 2 ) ) mod M ) - ( M / 2 ) )
40 eqid 
 |-  ( ( ( c + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( c + ( M / 2 ) ) mod M ) - ( M / 2 ) )
41 eqid 
 |-  ( ( ( d + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( d + ( M / 2 ) ) mod M ) - ( M / 2 ) )
42 eqid 
 |-  ( ( ( ( ( ( ( a + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) + ( ( ( ( b + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) ) + ( ( ( ( ( c + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) + ( ( ( ( d + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) ) ) / M ) = ( ( ( ( ( ( ( a + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) + ( ( ( ( b + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) ) + ( ( ( ( ( c + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) + ( ( ( ( d + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ^ 2 ) ) ) / M )
43 simp3 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
44 1 29 30 31 32 6 7 33 34 35 36 37 38 39 40 41 42 43 4sqlem17 
 |-  -. ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
45 44 pm2.21i 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> -. M e. ( ZZ>= ` 2 ) )
46 45 3expia 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. ZZ /\ d e. ZZ ) ) ) -> ( ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> -. M e. ( ZZ>= ` 2 ) ) )
47 46 anassrs 
 |-  ( ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> -. M e. ( ZZ>= ` 2 ) ) )
48 47 rexlimdvva 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` 2 ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( E. c e. ZZ E. d e. ZZ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> -. M e. ( ZZ>= ` 2 ) ) )
49 48 rexlimdvva 
 |-  ( ( ph /\ M e. ( ZZ>= ` 2 ) ) -> ( E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( M x. P ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) -> -. M e. ( ZZ>= ` 2 ) ) )
50 27 49 mpd 
 |-  ( ( ph /\ M e. ( ZZ>= ` 2 ) ) -> -. M e. ( ZZ>= ` 2 ) )
51 50 pm2.01da 
 |-  ( ph -> -. M e. ( ZZ>= ` 2 ) )
52 23 simpld 
 |-  ( ph -> M e. NN )
53 elnn1uz2 
 |-  ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
54 52 53 sylib 
 |-  ( ph -> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
55 54 ord 
 |-  ( ph -> ( -. M = 1 -> M e. ( ZZ>= ` 2 ) ) )
56 51 55 mt3d 
 |-  ( ph -> M = 1 )
57 56 19 eqeltrrd 
 |-  ( ph -> 1 e. T )
58 oveq1 
 |-  ( i = 1 -> ( i x. P ) = ( 1 x. P ) )
59 58 eleq1d 
 |-  ( i = 1 -> ( ( i x. P ) e. S <-> ( 1 x. P ) e. S ) )
60 59 6 elrab2 
 |-  ( 1 e. T <-> ( 1 e. NN /\ ( 1 x. P ) e. S ) )
61 60 simprbi 
 |-  ( 1 e. T -> ( 1 x. P ) e. S )
62 57 61 syl 
 |-  ( ph -> ( 1 x. P ) e. S )
63 11 62 eqeltrrd 
 |-  ( ph -> P e. S )