This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem14

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 , < )
4sq.m 
|- ( ph -> M e. ( ZZ>= ` 2 ) )
4sq.a 
|- ( ph -> A e. ZZ )
4sq.b 
|- ( ph -> B e. ZZ )
4sq.c 
|- ( ph -> C e. ZZ )
4sq.d 
|- ( ph -> D e. ZZ )
4sq.e 
|- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.f 
|- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.g 
|- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.h 
|- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.r 
|- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
4sq.p 
|- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
Assertion 4sqlem14 
|- ( ph -> R e. NN0 )

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 4sq.m 
 |-  ( ph -> M e. ( ZZ>= ` 2 ) )
9 4sq.a 
 |-  ( ph -> A e. ZZ )
10 4sq.b 
 |-  ( ph -> B e. ZZ )
11 4sq.c 
 |-  ( ph -> C e. ZZ )
12 4sq.d 
 |-  ( ph -> D e. ZZ )
13 4sq.e 
 |-  E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
14 4sq.f 
 |-  F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
15 4sq.g 
 |-  G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
16 4sq.h 
 |-  H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
17 4sq.r 
 |-  R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
18 4sq.p 
 |-  ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
19 6 ssrab3 
 |-  T C_ NN
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 19 20 sseqtri 
 |-  T C_ ( ZZ>= ` 1 )
22 1 2 3 4 5 6 7 4sqlem13 
 |-  ( ph -> ( T =/= (/) /\ M < P ) )
23 22 simpld 
 |-  ( ph -> T =/= (/) )
24 infssuzcl 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )
25 21 23 24 sylancr 
 |-  ( ph -> inf ( T , RR , < ) e. T )
26 7 25 eqeltrid 
 |-  ( ph -> M e. T )
27 19 26 sselid 
 |-  ( ph -> M e. NN )
28 27 nnzd 
 |-  ( ph -> M e. ZZ )
29 prmz 
 |-  ( P e. Prime -> P e. ZZ )
30 4 29 syl 
 |-  ( ph -> P e. ZZ )
31 28 30 zmulcld 
 |-  ( ph -> ( M x. P ) e. ZZ )
32 9 27 13 4sqlem5 
 |-  ( ph -> ( E e. ZZ /\ ( ( A - E ) / M ) e. ZZ ) )
33 32 simpld 
 |-  ( ph -> E e. ZZ )
34 zsqcl2 
 |-  ( E e. ZZ -> ( E ^ 2 ) e. NN0 )
35 33 34 syl 
 |-  ( ph -> ( E ^ 2 ) e. NN0 )
36 10 27 14 4sqlem5 
 |-  ( ph -> ( F e. ZZ /\ ( ( B - F ) / M ) e. ZZ ) )
37 36 simpld 
 |-  ( ph -> F e. ZZ )
38 zsqcl2 
 |-  ( F e. ZZ -> ( F ^ 2 ) e. NN0 )
39 37 38 syl 
 |-  ( ph -> ( F ^ 2 ) e. NN0 )
40 35 39 nn0addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN0 )
41 40 nn0zd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ )
42 11 27 15 4sqlem5 
 |-  ( ph -> ( G e. ZZ /\ ( ( C - G ) / M ) e. ZZ ) )
43 42 simpld 
 |-  ( ph -> G e. ZZ )
44 zsqcl2 
 |-  ( G e. ZZ -> ( G ^ 2 ) e. NN0 )
45 43 44 syl 
 |-  ( ph -> ( G ^ 2 ) e. NN0 )
46 12 27 16 4sqlem5 
 |-  ( ph -> ( H e. ZZ /\ ( ( D - H ) / M ) e. ZZ ) )
47 46 simpld 
 |-  ( ph -> H e. ZZ )
48 zsqcl2 
 |-  ( H e. ZZ -> ( H ^ 2 ) e. NN0 )
49 47 48 syl 
 |-  ( ph -> ( H ^ 2 ) e. NN0 )
50 45 49 nn0addcld 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. NN0 )
51 50 nn0zd 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. ZZ )
52 41 51 zaddcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. ZZ )
53 31 52 zsubcld 
 |-  ( ph -> ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) e. ZZ )
54 dvdsmul1 
 |-  ( ( M e. ZZ /\ P e. ZZ ) -> M || ( M x. P ) )
55 28 30 54 syl2anc 
 |-  ( ph -> M || ( M x. P ) )
56 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
57 9 56 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
58 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
59 10 58 syl 
 |-  ( ph -> ( B ^ 2 ) e. ZZ )
60 57 59 zaddcld 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. ZZ )
61 60 41 zsubcld 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) e. ZZ )
62 zsqcl 
 |-  ( C e. ZZ -> ( C ^ 2 ) e. ZZ )
63 11 62 syl 
 |-  ( ph -> ( C ^ 2 ) e. ZZ )
64 zsqcl 
 |-  ( D e. ZZ -> ( D ^ 2 ) e. ZZ )
65 12 64 syl 
 |-  ( ph -> ( D ^ 2 ) e. ZZ )
66 63 65 zaddcld 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ )
67 66 51 zsubcld 
 |-  ( ph -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. ZZ )
68 35 nn0zd 
 |-  ( ph -> ( E ^ 2 ) e. ZZ )
69 57 68 zsubcld 
 |-  ( ph -> ( ( A ^ 2 ) - ( E ^ 2 ) ) e. ZZ )
70 39 nn0zd 
 |-  ( ph -> ( F ^ 2 ) e. ZZ )
71 59 70 zsubcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( F ^ 2 ) ) e. ZZ )
72 9 27 13 4sqlem8 
 |-  ( ph -> M || ( ( A ^ 2 ) - ( E ^ 2 ) ) )
73 10 27 14 4sqlem8 
 |-  ( ph -> M || ( ( B ^ 2 ) - ( F ^ 2 ) ) )
74 28 69 71 72 73 dvds2addd 
 |-  ( ph -> M || ( ( ( A ^ 2 ) - ( E ^ 2 ) ) + ( ( B ^ 2 ) - ( F ^ 2 ) ) ) )
75 9 zcnd 
 |-  ( ph -> A e. CC )
76 75 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
77 10 zcnd 
 |-  ( ph -> B e. CC )
78 77 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
79 33 zcnd 
 |-  ( ph -> E e. CC )
80 79 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
81 37 zcnd 
 |-  ( ph -> F e. CC )
82 81 sqcld 
 |-  ( ph -> ( F ^ 2 ) e. CC )
83 76 78 80 82 addsub4d 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( E ^ 2 ) ) + ( ( B ^ 2 ) - ( F ^ 2 ) ) ) )
84 74 83 breqtrrd 
 |-  ( ph -> M || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
85 45 nn0zd 
 |-  ( ph -> ( G ^ 2 ) e. ZZ )
86 63 85 zsubcld 
 |-  ( ph -> ( ( C ^ 2 ) - ( G ^ 2 ) ) e. ZZ )
87 49 nn0zd 
 |-  ( ph -> ( H ^ 2 ) e. ZZ )
88 65 87 zsubcld 
 |-  ( ph -> ( ( D ^ 2 ) - ( H ^ 2 ) ) e. ZZ )
89 11 27 15 4sqlem8 
 |-  ( ph -> M || ( ( C ^ 2 ) - ( G ^ 2 ) ) )
90 12 27 16 4sqlem8 
 |-  ( ph -> M || ( ( D ^ 2 ) - ( H ^ 2 ) ) )
91 28 86 88 89 90 dvds2addd 
 |-  ( ph -> M || ( ( ( C ^ 2 ) - ( G ^ 2 ) ) + ( ( D ^ 2 ) - ( H ^ 2 ) ) ) )
92 11 zcnd 
 |-  ( ph -> C e. CC )
93 92 sqcld 
 |-  ( ph -> ( C ^ 2 ) e. CC )
94 12 zcnd 
 |-  ( ph -> D e. CC )
95 94 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
96 43 zcnd 
 |-  ( ph -> G e. CC )
97 96 sqcld 
 |-  ( ph -> ( G ^ 2 ) e. CC )
98 47 zcnd 
 |-  ( ph -> H e. CC )
99 98 sqcld 
 |-  ( ph -> ( H ^ 2 ) e. CC )
100 93 95 97 99 addsub4d 
 |-  ( ph -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = ( ( ( C ^ 2 ) - ( G ^ 2 ) ) + ( ( D ^ 2 ) - ( H ^ 2 ) ) ) )
101 91 100 breqtrrd 
 |-  ( ph -> M || ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
102 28 61 67 84 101 dvds2addd 
 |-  ( ph -> M || ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
103 18 oveq1d 
 |-  ( ph -> ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
104 76 78 addcld 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC )
105 93 95 addcld 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. CC )
106 80 82 addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. CC )
107 97 99 addcld 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. CC )
108 104 105 106 107 addsub4d 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
109 103 108 eqtrd 
 |-  ( ph -> ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
110 102 109 breqtrrd 
 |-  ( ph -> M || ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
111 28 31 53 55 110 dvds2subd 
 |-  ( ph -> M || ( ( M x. P ) - ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) ) )
112 27 nncnd 
 |-  ( ph -> M e. CC )
113 prmnn 
 |-  ( P e. Prime -> P e. NN )
114 4 113 syl 
 |-  ( ph -> P e. NN )
115 114 nncnd 
 |-  ( ph -> P e. CC )
116 112 115 mulcld 
 |-  ( ph -> ( M x. P ) e. CC )
117 106 107 addcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. CC )
118 116 117 nncand 
 |-  ( ph -> ( ( M x. P ) - ( ( M x. P ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) ) = ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
119 111 118 breqtrd 
 |-  ( ph -> M || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
120 27 nnne0d 
 |-  ( ph -> M =/= 0 )
121 40 50 nn0addcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. NN0 )
122 121 nn0zd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. ZZ )
123 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. ZZ ) -> ( M || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <-> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. ZZ ) )
124 28 120 122 123 syl3anc 
 |-  ( ph -> ( M || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <-> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. ZZ ) )
125 119 124 mpbid 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. ZZ )
126 121 nn0red 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR )
127 121 nn0ge0d 
 |-  ( ph -> 0 <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
128 27 nnred 
 |-  ( ph -> M e. RR )
129 27 nngt0d 
 |-  ( ph -> 0 < M )
130 divge0 
 |-  ( ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR /\ 0 <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) /\ ( M e. RR /\ 0 < M ) ) -> 0 <_ ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) )
131 126 127 128 129 130 syl22anc 
 |-  ( ph -> 0 <_ ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) )
132 elnn0z 
 |-  ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. NN0 <-> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. ZZ /\ 0 <_ ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) ) )
133 125 131 132 sylanbrc 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) e. NN0 )
134 17 133 eqeltrid 
 |-  ( ph -> R e. NN0 )