MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem16 Structured version   Unicode version

Theorem 4sqlem16 14355
Description: Lemma for 4sq 14359. (Contributed by Mario Carneiro, 16-Jul-2014.)
Hypotheses
Ref Expression
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  =  sup ( 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
Ref Expression
4sqlem16  |-  ( ph  ->  ( R  <_  M  /\  ( ( R  =  0  \/  R  =  M )  ->  ( M ^ 2 )  ||  ( M  x.  P
) ) ) )
Distinct variable groups:    w, n, x, y, z    B, n   
n, E    n, G    n, H    A, n    C, n    D, n    n, F    i, n, M    n, N    P, i, n    ph, n    S, i, n    R, i
Allowed substitution hints:    ph( x, y, z, w, i)    A( x, y, z, w, i)    B( x, y, z, w, i)    C( x, y, z, w, i)    D( x, y, z, w, i)    P( x, y, z, w)    R( x, y, z, w, n)    S( x, y, z, w)    T( x, y, z, w, i, n)    E( x, y, z, w, i)    F( x, y, z, w, i)    G( x, y, z, w, i)    H( x, y, z, w, i)    M( x, y, z, w)    N( x, y, z, w, i)

Proof of Theorem 4sqlem16
StepHypRef Expression
1 4sq.r . . 3  |-  R  =  ( ( ( ( E ^ 2 )  +  ( F ^
2 ) )  +  ( ( G ^
2 )  +  ( H ^ 2 ) ) )  /  M
)
2 4sq.a . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  ZZ )
3 4sq.m . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
2 ) )
4 eluz2nn 11128 . . . . . . . . . . . . 13  |-  ( M  e.  ( ZZ>= `  2
)  ->  M  e.  NN )
53, 4syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
6 4sq.e . . . . . . . . . . . 12  |-  E  =  ( ( ( A  +  ( M  / 
2 ) )  mod 
M )  -  ( M  /  2 ) )
72, 5, 64sqlem5 14337 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  ZZ  /\  ( ( A  -  E )  /  M
)  e.  ZZ ) )
87simpld 459 . . . . . . . . . 10  |-  ( ph  ->  E  e.  ZZ )
9 zsqcl 12217 . . . . . . . . . 10  |-  ( E  e.  ZZ  ->  ( E ^ 2 )  e.  ZZ )
108, 9syl 16 . . . . . . . . 9  |-  ( ph  ->  ( E ^ 2 )  e.  ZZ )
1110zred 10974 . . . . . . . 8  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
12 4sq.b . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  ZZ )
13 4sq.f . . . . . . . . . . . 12  |-  F  =  ( ( ( B  +  ( M  / 
2 ) )  mod 
M )  -  ( M  /  2 ) )
1412, 5, 134sqlem5 14337 . . . . . . . . . . 11  |-  ( ph  ->  ( F  e.  ZZ  /\  ( ( B  -  F )  /  M
)  e.  ZZ ) )
1514simpld 459 . . . . . . . . . 10  |-  ( ph  ->  F  e.  ZZ )
16 zsqcl 12217 . . . . . . . . . 10  |-  ( F  e.  ZZ  ->  ( F ^ 2 )  e.  ZZ )
1715, 16syl 16 . . . . . . . . 9  |-  ( ph  ->  ( F ^ 2 )  e.  ZZ )
1817zred 10974 . . . . . . . 8  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
1911, 18readdcld 9626 . . . . . . 7  |-  ( ph  ->  ( ( E ^
2 )  +  ( F ^ 2 ) )  e.  RR )
20 4sq.c . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  ZZ )
21 4sq.g . . . . . . . . . . . 12  |-  G  =  ( ( ( C  +  ( M  / 
2 ) )  mod 
M )  -  ( M  /  2 ) )
2220, 5, 214sqlem5 14337 . . . . . . . . . . 11  |-  ( ph  ->  ( G  e.  ZZ  /\  ( ( C  -  G )  /  M
)  e.  ZZ ) )
2322simpld 459 . . . . . . . . . 10  |-  ( ph  ->  G  e.  ZZ )
24 zsqcl 12217 . . . . . . . . . 10  |-  ( G  e.  ZZ  ->  ( G ^ 2 )  e.  ZZ )
2523, 24syl 16 . . . . . . . . 9  |-  ( ph  ->  ( G ^ 2 )  e.  ZZ )
2625zred 10974 . . . . . . . 8  |-  ( ph  ->  ( G ^ 2 )  e.  RR )
27 4sq.d . . . . . . . . . . . 12  |-  ( ph  ->  D  e.  ZZ )
28 4sq.h . . . . . . . . . . . 12  |-  H  =  ( ( ( D  +  ( M  / 
2 ) )  mod 
M )  -  ( M  /  2 ) )
2927, 5, 284sqlem5 14337 . . . . . . . . . . 11  |-  ( ph  ->  ( H  e.  ZZ  /\  ( ( D  -  H )  /  M
)  e.  ZZ ) )
3029simpld 459 . . . . . . . . . 10  |-  ( ph  ->  H  e.  ZZ )
31 zsqcl 12217 . . . . . . . . . 10  |-  ( H  e.  ZZ  ->  ( H ^ 2 )  e.  ZZ )
3230, 31syl 16 . . . . . . . . 9  |-  ( ph  ->  ( H ^ 2 )  e.  ZZ )
3332zred 10974 . . . . . . . 8  |-  ( ph  ->  ( H ^ 2 )  e.  RR )
3426, 33readdcld 9626 . . . . . . 7  |-  ( ph  ->  ( ( G ^
2 )  +  ( H ^ 2 ) )  e.  RR )
355nnred 10557 . . . . . . . . 9  |-  ( ph  ->  M  e.  RR )
3635resqcld 12315 . . . . . . . 8  |-  ( ph  ->  ( M ^ 2 )  e.  RR )
3736rehalfcld 10791 . . . . . . 7  |-  ( ph  ->  ( ( M ^
2 )  /  2
)  e.  RR )
3837rehalfcld 10791 . . . . . . . . 9  |-  ( ph  ->  ( ( ( M ^ 2 )  / 
2 )  /  2
)  e.  RR )
392, 5, 64sqlem7 14339 . . . . . . . . 9  |-  ( ph  ->  ( E ^ 2 )  <_  ( (
( M ^ 2 )  /  2 )  /  2 ) )
4012, 5, 134sqlem7 14339 . . . . . . . . 9  |-  ( ph  ->  ( F ^ 2 )  <_  ( (
( M ^ 2 )  /  2 )  /  2 ) )
4111, 18, 38, 38, 39, 40le2addd 10176 . . . . . . . 8  |-  ( ph  ->  ( ( E ^
2 )  +  ( F ^ 2 ) )  <_  ( (
( ( M ^
2 )  /  2
)  /  2 )  +  ( ( ( M ^ 2 )  /  2 )  / 
2 ) ) )
4237recnd 9625 . . . . . . . . 9  |-  ( ph  ->  ( ( M ^
2 )  /  2
)  e.  CC )
43422halvesd 10790 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( M ^ 2 )  /  2 )  / 
2 )  +  ( ( ( M ^
2 )  /  2
)  /  2 ) )  =  ( ( M ^ 2 )  /  2 ) )
4441, 43breqtrd 4461 . . . . . . 7  |-  ( ph  ->  ( ( E ^
2 )  +  ( F ^ 2 ) )  <_  ( ( M ^ 2 )  / 
2 ) )
4520, 5, 214sqlem7 14339 . . . . . . . . 9  |-  ( ph  ->  ( G ^ 2 )  <_  ( (
( M ^ 2 )  /  2 )  /  2 ) )
4627, 5, 284sqlem7 14339 . . . . . . . . 9  |-  ( ph  ->  ( H ^ 2 )  <_  ( (
( M ^ 2 )  /  2 )  /  2 ) )
4726, 33, 38, 38, 45, 46le2addd 10176 . . . . . . . 8  |-  ( ph  ->  ( ( G ^
2 )  +  ( H ^ 2 ) )  <_  ( (
( ( M ^
2 )  /  2
)  /  2 )  +  ( ( ( M ^ 2 )  /  2 )  / 
2 ) ) )
4847, 43breqtrd 4461 . . . . . . 7  |-  ( ph  ->  ( ( G ^
2 )  +  ( H ^ 2 ) )  <_  ( ( M ^ 2 )  / 
2 ) )
4919, 34, 37, 37, 44, 48le2addd 10176 . . . . . 6  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  <_  ( (
( M ^ 2 )  /  2 )  +  ( ( M ^ 2 )  / 
2 ) ) )
5036recnd 9625 . . . . . . 7  |-  ( ph  ->  ( M ^ 2 )  e.  CC )
51502halvesd 10790 . . . . . 6  |-  ( ph  ->  ( ( ( M ^ 2 )  / 
2 )  +  ( ( M ^ 2 )  /  2 ) )  =  ( M ^ 2 ) )
5249, 51breqtrd 4461 . . . . 5  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  <_  ( M ^ 2 ) )
5335recnd 9625 . . . . . 6  |-  ( ph  ->  M  e.  CC )
5453sqvald 12286 . . . . 5  |-  ( ph  ->  ( M ^ 2 )  =  ( M  x.  M ) )
5552, 54breqtrd 4461 . . . 4  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  <_  ( M  x.  M ) )
5619, 34readdcld 9626 . . . . 5  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  e.  RR )
575nngt0d 10585 . . . . 5  |-  ( ph  ->  0  <  M )
58 ledivmul 10424 . . . . 5  |-  ( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  e.  RR  /\  M  e.  RR  /\  ( M  e.  RR  /\  0  <  M ) )  -> 
( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  /  M )  <_  M  <->  ( ( ( E ^
2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^
2 ) ) )  <_  ( M  x.  M ) ) )
5956, 35, 35, 57, 58syl112anc 1233 . . . 4  |-  ( ph  ->  ( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  /  M )  <_  M  <->  ( ( ( E ^
2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^
2 ) ) )  <_  ( M  x.  M ) ) )
6055, 59mpbird 232 . . 3  |-  ( ph  ->  ( ( ( ( E ^ 2 )  +  ( F ^
2 ) )  +  ( ( G ^
2 )  +  ( H ^ 2 ) ) )  /  M
)  <_  M )
611, 60syl5eqbr 4470 . 2  |-  ( ph  ->  R  <_  M )
62 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  R  = 
0 )  ->  R  =  0 )
631, 62syl5eqr 2498 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  = 
0 )  ->  (
( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  /  M )  =  0 )
6456recnd 9625 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  e.  CC )
655nnne0d 10586 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  =/=  0 )
6664, 53, 65diveq0ad 10336 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  /  M )  =  0  <-> 
( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  =  0 ) )
67 zsqcl2 12224 . . . . . . . . . . . . . . . . . 18  |-  ( E  e.  ZZ  ->  ( E ^ 2 )  e. 
NN0 )
688, 67syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  e.  NN0 )
69 zsqcl2 12224 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  ZZ  ->  ( F ^ 2 )  e. 
NN0 )
7015, 69syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F ^ 2 )  e.  NN0 )
7168, 70nn0addcld 10862 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E ^
2 )  +  ( F ^ 2 ) )  e.  NN0 )
7271nn0ge0d 10861 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( ( E ^ 2 )  +  ( F ^ 2 ) ) )
73 zsqcl2 12224 . . . . . . . . . . . . . . . . . 18  |-  ( G  e.  ZZ  ->  ( G ^ 2 )  e. 
NN0 )
7423, 73syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G ^ 2 )  e.  NN0 )
75 zsqcl2 12224 . . . . . . . . . . . . . . . . . 18  |-  ( H  e.  ZZ  ->  ( H ^ 2 )  e. 
NN0 )
7630, 75syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( H ^ 2 )  e.  NN0 )
7774, 76nn0addcld 10862 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( G ^
2 )  +  ( H ^ 2 ) )  e.  NN0 )
7877nn0ge0d 10861 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )
79 add20 10070 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  e.  RR  /\  0  <_  ( ( E ^ 2 )  +  ( F ^ 2 ) ) )  /\  ( ( ( G ^ 2 )  +  ( H ^ 2 ) )  e.  RR  /\  0  <_  ( ( G ^ 2 )  +  ( H ^ 2 ) ) ) )  ->  ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  =  0  <->  ( ( ( E ^ 2 )  +  ( F ^
2 ) )  =  0  /\  ( ( G ^ 2 )  +  ( H ^
2 ) )  =  0 ) ) )
8019, 72, 34, 78, 79syl22anc 1230 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( E ^ 2 )  +  ( F ^
2 ) )  +  ( ( G ^
2 )  +  ( H ^ 2 ) ) )  =  0  <-> 
( ( ( E ^ 2 )  +  ( F ^ 2 ) )  =  0  /\  ( ( G ^ 2 )  +  ( H ^ 2 ) )  =  0 ) ) )
8166, 80bitrd 253 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^ 2 ) ) )  /  M )  =  0  <-> 
( ( ( E ^ 2 )  +  ( F ^ 2 ) )  =  0  /\  ( ( G ^ 2 )  +  ( H ^ 2 ) )  =  0 ) ) )
8281biimpa 484 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
( ( E ^
2 )  +  ( F ^ 2 ) )  +  ( ( G ^ 2 )  +  ( H ^
2 ) ) )  /  M )  =  0 )  ->  (
( ( E ^
2 )  +  ( F ^ 2 ) )  =  0  /\  ( ( G ^
2 )  +  ( H ^ 2 ) )  =  0 ) )
8363, 82syldan 470 . . . . . . . . . . 11  |-  ( (
ph  /\  R  = 
0 )  ->  (
( ( E ^
2 )  +  ( F ^ 2 ) )  =  0  /\  ( ( G ^
2 )  +  ( H ^ 2 ) )  =  0 ) )
8483simpld 459 . . . . . . . . . 10  |-  ( (
ph  /\  R  = 
0 )  ->  (
( E ^ 2 )  +  ( F ^ 2 ) )  =  0 )
8568nn0ge0d 10861 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( E ^ 2 ) )
8670nn0ge0d 10861 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( F ^ 2 ) )
87 add20 10070 . . . . . . . . . . . 12  |-  ( ( ( ( E ^
2 )  e.  RR  /\  0  <_  ( E ^ 2 ) )  /\  ( ( F ^ 2 )  e.  RR  /\  0  <_ 
( F ^ 2 ) ) )  -> 
( ( ( E ^ 2 )  +  ( F ^ 2 ) )  =  0  <-> 
( ( E ^
2 )  =  0  /\  ( F ^
2 )  =  0 ) ) )
8811, 85, 18, 86, 87syl22anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E ^ 2 )  +  ( F ^ 2 ) )  =  0  <-> 
( ( E ^
2 )  =  0  /\  ( F ^
2 )  =  0 ) ) )
8988biimpa 484 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( E ^ 2 )  +  ( F ^ 2 ) )  =  0 )  ->  ( ( E ^ 2 )  =  0  /\  ( F ^ 2 )  =  0 ) )
9084, 89syldan 470 . . . . . . . . 9  |-  ( (
ph  /\  R  = 
0 )  ->  (
( E ^ 2 )  =  0  /\  ( F ^ 2 )  =  0 ) )
9190simpld 459 . . . . . . . 8  |-  ( (
ph  /\  R  = 
0 )  ->  ( E ^ 2 )  =  0 )
922, 5, 6, 914sqlem9 14341 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( A ^ 2 ) )
9390simprd 463 . . . . . . . 8  |-  ( (
ph  /\  R  = 
0 )  ->  ( F ^ 2 )  =  0 )
9412, 5, 13, 934sqlem9 14341 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( B ^ 2 ) )
955nnsqcld 12309 . . . . . . . . . 10  |-  ( ph  ->  ( M ^ 2 )  e.  NN )
9695nnzd 10973 . . . . . . . . 9  |-  ( ph  ->  ( M ^ 2 )  e.  ZZ )
97 zsqcl 12217 . . . . . . . . . 10  |-  ( A  e.  ZZ  ->  ( A ^ 2 )  e.  ZZ )
982, 97syl 16 . . . . . . . . 9  |-  ( ph  ->  ( A ^ 2 )  e.  ZZ )
99 zsqcl 12217 . . . . . . . . . 10  |-  ( B  e.  ZZ  ->  ( B ^ 2 )  e.  ZZ )
10012, 99syl 16 . . . . . . . . 9  |-  ( ph  ->  ( B ^ 2 )  e.  ZZ )
101 dvds2add 13892 . . . . . . . . 9  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( A ^ 2 )  e.  ZZ  /\  ( B ^ 2 )  e.  ZZ )  ->  (
( ( M ^
2 )  ||  ( A ^ 2 )  /\  ( M ^ 2 ) 
||  ( B ^
2 ) )  -> 
( M ^ 2 )  ||  ( ( A ^ 2 )  +  ( B ^
2 ) ) ) )
10296, 98, 100, 101syl3anc 1229 . . . . . . . 8  |-  ( ph  ->  ( ( ( M ^ 2 )  ||  ( A ^ 2 )  /\  ( M ^
2 )  ||  ( B ^ 2 ) )  ->  ( M ^
2 )  ||  (
( A ^ 2 )  +  ( B ^ 2 ) ) ) )
103102adantr 465 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  (
( ( M ^
2 )  ||  ( A ^ 2 )  /\  ( M ^ 2 ) 
||  ( B ^
2 ) )  -> 
( M ^ 2 )  ||  ( ( A ^ 2 )  +  ( B ^
2 ) ) ) )
10492, 94, 103mp2and 679 . . . . . 6  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( ( A ^
2 )  +  ( B ^ 2 ) ) )
10583simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  R  = 
0 )  ->  (
( G ^ 2 )  +  ( H ^ 2 ) )  =  0 )
10674nn0ge0d 10861 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( G ^ 2 ) )
10776nn0ge0d 10861 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( H ^ 2 ) )
108 add20 10070 . . . . . . . . . . . 12  |-  ( ( ( ( G ^
2 )  e.  RR  /\  0  <_  ( G ^ 2 ) )  /\  ( ( H ^ 2 )  e.  RR  /\  0  <_ 
( H ^ 2 ) ) )  -> 
( ( ( G ^ 2 )  +  ( H ^ 2 ) )  =  0  <-> 
( ( G ^
2 )  =  0  /\  ( H ^
2 )  =  0 ) ) )
10926, 106, 33, 107, 108syl22anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( G ^ 2 )  +  ( H ^ 2 ) )  =  0  <-> 
( ( G ^
2 )  =  0  /\  ( H ^
2 )  =  0 ) ) )
110109biimpa 484 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( G ^ 2 )  +  ( H ^ 2 ) )  =  0 )  ->  ( ( G ^ 2 )  =  0  /\  ( H ^ 2 )  =  0 ) )
111105, 110syldan 470 . . . . . . . . 9  |-  ( (
ph  /\  R  = 
0 )  ->  (
( G ^ 2 )  =  0  /\  ( H ^ 2 )  =  0 ) )
112111simpld 459 . . . . . . . 8  |-  ( (
ph  /\  R  = 
0 )  ->  ( G ^ 2 )  =  0 )
11320, 5, 21, 1124sqlem9 14341 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( C ^ 2 ) )
114111simprd 463 . . . . . . . 8  |-  ( (
ph  /\  R  = 
0 )  ->  ( H ^ 2 )  =  0 )
11527, 5, 28, 1144sqlem9 14341 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( D ^ 2 ) )
116 zsqcl 12217 . . . . . . . . . 10  |-  ( C  e.  ZZ  ->  ( C ^ 2 )  e.  ZZ )
11720, 116syl 16 . . . . . . . . 9  |-  ( ph  ->  ( C ^ 2 )  e.  ZZ )
118 zsqcl 12217 . . . . . . . . . 10  |-  ( D  e.  ZZ  ->  ( D ^ 2 )  e.  ZZ )
11927, 118syl 16 . . . . . . . . 9  |-  ( ph  ->  ( D ^ 2 )  e.  ZZ )
120 dvds2add 13892 . . . . . . . . 9  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( C ^ 2 )  e.  ZZ  /\  ( D ^ 2 )  e.  ZZ )  ->  (
( ( M ^
2 )  ||  ( C ^ 2 )  /\  ( M ^ 2 ) 
||  ( D ^
2 ) )  -> 
( M ^ 2 )  ||  ( ( C ^ 2 )  +  ( D ^
2 ) ) ) )
12196, 117, 119, 120syl3anc 1229 . . . . . . . 8  |-  ( ph  ->  ( ( ( M ^ 2 )  ||  ( C ^ 2 )  /\  ( M ^
2 )  ||  ( D ^ 2 ) )  ->  ( M ^
2 )  ||  (
( C ^ 2 )  +  ( D ^ 2 ) ) ) )
122121adantr 465 . . . . . . 7  |-  ( (
ph  /\  R  = 
0 )  ->  (
( ( M ^
2 )  ||  ( C ^ 2 )  /\  ( M ^ 2 ) 
||  ( D ^
2 ) )  -> 
( M ^ 2 )  ||  ( ( C ^ 2 )  +  ( D ^
2 ) ) ) )
123113, 115, 122mp2and 679 . . . . . 6  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( ( C ^
2 )  +  ( D ^ 2 ) ) )
12498, 100zaddcld 10978 . . . . . . . 8  |-  ( ph  ->  ( ( A ^
2 )  +  ( B ^ 2 ) )  e.  ZZ )
125117, 119zaddcld 10978 . . . . . . . 8  |-  ( ph  ->  ( ( C ^
2 )  +  ( D ^ 2 ) )  e.  ZZ )
126 dvds2add 13892 . . . . . . . 8  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( ( A ^
2 )  +  ( B ^ 2 ) )  e.  ZZ  /\  ( ( C ^
2 )  +  ( D ^ 2 ) )  e.  ZZ )  ->  ( ( ( M ^ 2 ) 
||  ( ( A ^ 2 )  +  ( B ^ 2 ) )  /\  ( M ^ 2 )  ||  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) ) )
12796, 124, 125, 126syl3anc 1229 . . . . . . 7  |-  ( ph  ->  ( ( ( M ^ 2 )  ||  ( ( A ^
2 )  +  ( B ^ 2 ) )  /\  ( M ^ 2 )  ||  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) ) )
128127adantr 465 . . . . . 6  |-  ( (
ph  /\  R  = 
0 )  ->  (
( ( M ^
2 )  ||  (
( A ^ 2 )  +  ( B ^ 2 ) )  /\  ( M ^
2 )  ||  (
( C ^ 2 )  +  ( D ^ 2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) ) )
129104, 123, 128mp2and 679 . . . . 5  |-  ( (
ph  /\  R  = 
0 )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) )
130 4sq.1 . . . . . . . . . . . . . 14  |-  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 ) ) ) }
131 4sq.2 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
132 4sq.3 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  =  ( ( 2  x.  N )  +  1 ) )
133 4sq.4 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  Prime )
134 4sq.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ... (
2  x.  N ) )  C_  S )
135 4sq.6 . . . . . . . . . . . . . 14  |-  T  =  { i  e.  NN  |  ( i  x.  P )  e.  S }
136 4sq.7 . . . . . . . . . . . . . 14  |-  M  =  sup ( T ,  RR ,  `'  <  )
137 4sq.p . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M  x.  P
)  =  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) )
138130, 131, 132, 133, 134, 135, 136, 3, 2, 12, 20, 27, 6, 13, 21, 28, 1, 1374sqlem15 14354 . . . . . . . . . . . . 13  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( ( ( M ^ 2 )  /  2 )  /  2 )  -  ( E ^ 2 ) )  =  0  /\  ( ( ( ( M ^ 2 )  /  2 )  / 
2 )  -  ( F ^ 2 ) )  =  0 )  /\  ( ( ( ( ( M ^ 2 )  /  2 )  /  2 )  -  ( G ^ 2 ) )  =  0  /\  ( ( ( ( M ^ 2 )  /  2 )  / 
2 )  -  ( H ^ 2 ) )  =  0 ) ) )
139138simpld 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( ( M ^ 2 )  /  2 )  / 
2 )  -  ( E ^ 2 ) )  =  0  /\  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( F ^ 2 ) )  =  0 ) )
140139simpld 459 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( E ^ 2 ) )  =  0 )
1412, 5, 6, 1404sqlem10 14342 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( A ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )
142139simprd 463 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( F ^ 2 ) )  =  0 )
14312, 5, 13, 1424sqlem10 14342 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( B ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )
14496adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  e.  ZZ )
14598adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  ( A ^ 2 )  e.  ZZ )
14638recnd 9625 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( M ^ 2 )  / 
2 )  /  2
)  e.  CC )
14710zcnd 10975 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
148146, 147subeq0ad 9946 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( ( M ^ 2 )  /  2 )  /  2 )  -  ( E ^ 2 ) )  =  0  <->  (
( ( M ^
2 )  /  2
)  /  2 )  =  ( E ^
2 ) ) )
149148adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( ( M ^ 2 )  /  2 )  / 
2 )  -  ( E ^ 2 ) )  =  0  <->  ( (
( M ^ 2 )  /  2 )  /  2 )  =  ( E ^ 2 ) ) )
150140, 149mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  R  =  M )  ->  (
( ( M ^
2 )  /  2
)  /  2 )  =  ( E ^
2 ) )
15110adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  R  =  M )  ->  ( E ^ 2 )  e.  ZZ )
152150, 151eqeltrd 2531 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  (
( ( M ^
2 )  /  2
)  /  2 )  e.  ZZ )
153145, 152zsubcld 10979 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( A ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  e.  ZZ )
154100adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  ( B ^ 2 )  e.  ZZ )
155154, 152zsubcld 10979 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  e.  ZZ )
156 dvds2add 13892 . . . . . . . . . . 11  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( ( A ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  e.  ZZ  /\  ( ( B ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  e.  ZZ )  ->  ( ( ( M ^ 2 ) 
||  ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  /\  ( M ^ 2 )  ||  ( ( B ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) ) )
157144, 153, 155, 156syl3anc 1229 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  (
( ( M ^
2 )  ||  (
( A ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  /\  ( M ^
2 )  ||  (
( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) ) )
158141, 143, 157mp2and 679 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) )
15998zcnd 10975 . . . . . . . . . . . 12  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
160100zcnd 10975 . . . . . . . . . . . 12  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
161159, 160, 146, 146addsub4d 9983 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) ) ) )
16243oveq2d 6297 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  ( ( M ^ 2 )  / 
2 ) ) )
163161, 162eqtr3d 2486 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  ( ( M ^ 2 )  / 
2 ) ) )
164163adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  (
( ( A ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  +  ( ( B ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  / 
2 ) ) )  =  ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) ) )
165158, 164breqtrd 4461 . . . . . . . 8  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) ) )
166138simprd 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( ( M ^ 2 )  /  2 )  / 
2 )  -  ( G ^ 2 ) )  =  0  /\  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( H ^ 2 ) )  =  0 ) )
167166simpld 459 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( G ^ 2 ) )  =  0 )
16820, 5, 21, 1674sqlem10 14342 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( C ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )
169166simprd 463 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  -  ( H ^ 2 ) )  =  0 )
17027, 5, 28, 1694sqlem10 14342 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( D ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )
171117adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  ( C ^ 2 )  e.  ZZ )
172171, 152zsubcld 10979 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( C ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  e.  ZZ )
173119adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  R  =  M )  ->  ( D ^ 2 )  e.  ZZ )
174173, 152zsubcld 10979 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  e.  ZZ )
175 dvds2add 13892 . . . . . . . . . . 11  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( ( C ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  e.  ZZ  /\  ( ( D ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  e.  ZZ )  ->  ( ( ( M ^ 2 ) 
||  ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  /\  ( M ^ 2 )  ||  ( ( D ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) ) )
176144, 172, 174, 175syl3anc 1229 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  (
( ( M ^
2 )  ||  (
( C ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  /\  ( M ^
2 )  ||  (
( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) ) )
177168, 170, 176mp2and 679 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) ) )
178117zcnd 10975 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
179119zcnd 10975 . . . . . . . . . . . 12  |-  ( ph  ->  ( D ^ 2 )  e.  CC )
180178, 179, 146, 146addsub4d 9983 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) ) ) )
18143oveq2d 6297 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  / 
2 ) ) )
182180, 181eqtr3d 2486 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( C ^ 2 )  -  ( ( ( M ^ 2 )  / 
2 )  /  2
) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  /  2 ) ) )  =  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  / 
2 ) ) )
183182adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  (
( ( C ^
2 )  -  (
( ( M ^
2 )  /  2
)  /  2 ) )  +  ( ( D ^ 2 )  -  ( ( ( M ^ 2 )  /  2 )  / 
2 ) ) )  =  ( ( ( C ^ 2 )  +  ( D ^
2 ) )  -  ( ( M ^
2 )  /  2
) ) )
184177, 183breqtrd 4461 . . . . . . . 8  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) ) )
185124adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  (
( A ^ 2 )  +  ( B ^ 2 ) )  e.  ZZ )
18643adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  =  ( ( M ^ 2 )  / 
2 ) )
187152, 152zaddcld 10978 . . . . . . . . . . 11  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( M ^ 2 )  / 
2 )  /  2
)  +  ( ( ( M ^ 2 )  /  2 )  /  2 ) )  e.  ZZ )
188186, 187eqeltrrd 2532 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  (
( M ^ 2 )  /  2 )  e.  ZZ )
189185, 188zsubcld 10979 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  (
( ( A ^
2 )  +  ( B ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) )  e.  ZZ )
190125adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  R  =  M )  ->  (
( C ^ 2 )  +  ( D ^ 2 ) )  e.  ZZ )
191190, 188zsubcld 10979 . . . . . . . . 9  |-  ( (
ph  /\  R  =  M )  ->  (
( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) )  e.  ZZ )
192 dvds2add 13892 . . . . . . . . 9  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) )  e.  ZZ  /\  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) )  e.  ZZ )  ->  ( ( ( M ^ 2 ) 
||  ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) )  /\  ( M ^ 2 )  ||  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) )  +  ( ( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) ) ) ) )
193144, 189, 191, 192syl3anc 1229 . . . . . . . 8  |-  ( (
ph  /\  R  =  M )  ->  (
( ( M ^
2 )  ||  (
( ( A ^
2 )  +  ( B ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) )  /\  ( M ^
2 )  ||  (
( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) ) )  ->  ( M ^ 2 )  ||  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) )  +  ( ( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) ) ) ) )
194165, 184, 193mp2and 679 . . . . . . 7  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) )  +  ( ( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) ) ) )
195124zcnd 10975 . . . . . . . . . 10  |-  ( ph  ->  ( ( A ^
2 )  +  ( B ^ 2 ) )  e.  CC )
196125zcnd 10975 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  +  ( D ^ 2 ) )  e.  CC )
197195, 196, 42, 42addsub4d 9983 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  +  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  -  (
( ( M ^
2 )  /  2
)  +  ( ( M ^ 2 )  /  2 ) ) )  =  ( ( ( ( A ^
2 )  +  ( B ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) )  +  ( ( ( C ^ 2 )  +  ( D ^
2 ) )  -  ( ( M ^
2 )  /  2
) ) ) )
19851oveq2d 6297 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  +  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  -  (
( ( M ^
2 )  /  2
)  +  ( ( M ^ 2 )  /  2 ) ) )  =  ( ( ( ( A ^
2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^
2 ) ) )  -  ( M ^
2 ) ) )
199197, 198eqtr3d 2486 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  -  ( ( M ^
2 )  /  2
) )  +  ( ( ( C ^
2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  /  2 ) ) )  =  ( ( ( ( A ^
2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^
2 ) ) )  -  ( M ^
2 ) ) )
200199adantr 465 . . . . . . 7  |-  ( (
ph  /\  R  =  M )  ->  (
( ( ( A ^ 2 )  +  ( B ^ 2 ) )  -  (
( M ^ 2 )  /  2 ) )  +  ( ( ( C ^ 2 )  +  ( D ^ 2 ) )  -  ( ( M ^ 2 )  / 
2 ) ) )  =  ( ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  -  ( M ^ 2 ) ) )
201194, 200breqtrd 4461 . . . . . 6  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  +  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  -  ( M ^ 2 ) ) )
202124, 125zaddcld 10978 . . . . . . . 8  |-  ( ph  ->  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  e.  ZZ )
203202adantr 465 . . . . . . 7  |-  ( (
ph  /\  R  =  M )  ->  (
( ( A ^
2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^
2 ) ) )  e.  ZZ )
204 dvdssubr 13904 . . . . . . 7  |-  ( ( ( M ^ 2 )  e.  ZZ  /\  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  e.  ZZ )  ->  ( ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  <->  ( M ^
2 )  ||  (
( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  -  ( M ^ 2 ) ) ) )
205144, 203, 204syl2anc 661 . . . . . 6  |-  ( (
ph  /\  R  =  M )  ->  (
( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) )  <->  ( M ^ 2 )  ||  ( ( ( ( A ^ 2 )  +  ( B ^
2 ) )  +  ( ( C ^
2 )  +  ( D ^ 2 ) ) )  -  ( M ^ 2 ) ) ) )
206201, 205mpbird 232 . . . . 5  |-  ( (
ph  /\  R  =  M )  ->  ( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) )
207129, 206jaodan 785 . . . 4  |-  ( (
ph  /\  ( R  =  0  \/  R  =  M ) )  -> 
( M ^ 2 )  ||  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) )
208137adantr 465 . . . 4  |-  ( (
ph  /\  ( R  =  0  \/  R  =  M ) )  -> 
( M  x.  P
)  =  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  +  ( ( C ^ 2 )  +  ( D ^ 2 ) ) ) )
209207, 208breqtrrd 4463 . . 3  |-  ( (
ph  /\  ( R  =  0  \/  R  =  M ) )  -> 
( M ^ 2 )  ||  ( M  x.  P ) )
210209ex 434 . 2  |-  ( ph  ->  ( ( R  =  0  \/  R  =  M )  ->  ( M ^ 2 )  ||  ( M  x.  P
) ) )
21161, 210jca 532 1  |-  ( ph  ->  ( R  <_  M  /\  ( ( R  =  0  \/  R  =  M )  ->  ( M ^ 2 )  ||  ( M  x.  P
) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1383    e. wcel 1804   {cab 2428   E.wrex 2794   {crab 2797    C_ wss 3461   class class class wbr 4437   `'ccnv 4988   ` cfv 5578  (class class class)co 6281   supcsup 7902   RRcr 9494   0cc0 9495   1c1 9496    + caddc 9498    x. cmul 9500    < clt 9631    <_ cle 9632    - cmin 9810    / cdiv 10212   NNcn 10542   2c2 10591   NN0cn0 10801   ZZcz 10870   ZZ>=cuz 11090   ...cfz 11681    mod cmo 11975   ^cexp 12145    || cdvds 13863   Primecprime 14094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-2nd 6786  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-sup 7903  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10213  df-nn 10543  df-2 10600  df-3 10601  df-n0 10802  df-z 10871  df-uz 11091  df-rp 11230  df-fl 11908  df-mod 11976  df-seq 12087  df-exp 12146  df-cj 12911  df-re 12912  df-im 12913  df-sqrt 13047  df-abs 13048  df-dvds 13864  df-gcd 14022
This theorem is referenced by:  4sqlem17  14356
  Copyright terms: Public domain W3C validator