int_5.miz

begin

 reserve i,i1,i2,i3,i4,i5,j,r,a,b,x,y for Integer,

d,e,k,n for Nat,

fp,fk for FinSequence of INT ,

f,f1,f2 for FinSequence of REAL ,

p for Prime;

 theorem :: INT_5:1



 Th1: i1 divides i2 & i1 divides i3 implies i1 divides (i2 - i3)

 proof

 assume that

 A1: i1 divides i2 and

 A2: i1 divides i3;

 consider i4 such that

 A3: i2 = (i1 * i4) by A1;

 consider i5 such that

 A4: i3 = (i1 * i5) by A2;

 (i2 - i3) = (i1 * (i4 - i5)) by A3, A4;

 hence thesis;

 end;

 theorem :: INT_5:2



 Th2: i divides a & i divides (a - b) implies i divides b

 proof

 assume that

 A1: i divides a and

 A2: i divides (a - b);



 A3: b = (( - (a - b)) + a);

 i divides ( - (a - b)) by A2, INT_2: 10;

 hence thesis by A1, A3, WSIERP_1: 4;

 end;



 Lm1: (x divides y implies (y mod x) = 0 ) & (x <> 0 & (y mod x) = 0 implies x divides y)

 proof

 thus x divides y implies (y mod x) = 0

 proof

 assume x divides y;

 then

 consider i such that

 A1: y = (x * i);

 (y mod x) = (((x * i) + 0 ) mod x) by A1

 .= ( 0 mod x) by EULER_1: 12

 .= 0 by INT_1: 73;

 hence thesis;

 end;

 assume that

 A2: x <> 0 and

 A3: (y mod x) = 0 ;

 y = (((y div x) * x) + (y mod x)) by A2, INT_1: 59

 .= ((y div x) * x) by A3;

 hence thesis;

 end;

 definition

 let fp;

 :: INT_5:def1

 func Poly-INT fp -> Function of INT , INT means

 : Def1: for x be Element of INT holds ex fr be FinSequence of INT st ( len fr) = ( len fp) & (for d st d in ( dom fr) holds (fr . d) = ((fp . d) * (x |^ (d -' 1)))) & (it . x) = ( Sum fr);

 existence

 proof

 defpred F[ Element of INT , set] means ex fr be FinSequence of INT st ( len fr) = ( len fp) & (for d st d in ( dom fr) holds (fr . d) = ((fp . d) * ($1 |^ (d -' 1)))) & $2 = ( Sum fr);



 A1: for x be Element of INT holds ex y be Element of INT st F[x, y]

 proof

 let x be Element of INT ;

 deffunc G( Nat) = ((fp . $1) * (x |^ ($1 -' 1)));

 consider fr be FinSequence such that

 A2: ( len fr) = ( len fp) & for d be Nat st d in ( dom fr) holds (fr . d) = G(d) from FINSEQ_1:sch 2;

 for d be Nat st d in ( dom fr) holds (fr . d) in INT

 proof

 let d be Nat;

 assume d in ( dom fr);

 then (fr . d) = ((fp . d) * (x |^ (d -' 1))) by A2;

 hence thesis by INT_1:def 2;

 end;

 then

 reconsider fr as FinSequence of INT by FINSEQ_2: 12;

 take ( Sum fr);

 take fr;

 thus thesis by A2;

 end;

 consider f be Function of INT , INT such that

 A3: for x be Element of INT holds F[x, (f . x)] from FUNCT_2:sch 3( A1);

 take f;

 thus thesis by A3;

 end;

 uniqueness

 proof

 let f1 be Function of INT , INT ;

 let f2 be Function of INT , INT ;

 assume that

 A4: for x be Element of INT holds ex fr1 be FinSequence of INT st ( len fr1) = ( len fp) & (for d st d in ( dom fr1) holds (fr1 . d) = ((fp . d) * (x |^ (d -' 1)))) & (f1 . x) = ( Sum fr1) and

 A5: for x be Element of INT holds ex fr2 be FinSequence of INT st ( len fr2) = ( len fp) & (for d st d in ( dom fr2) holds (fr2 . d) = ((fp . d) * (x |^ (d -' 1)))) & (f2 . x) = ( Sum fr2);

 for x be Element of INT holds (f1 . x) = (f2 . x)

 proof

 let x be Element of INT ;

 consider fr1 be FinSequence of INT such that

 A6: ( len fr1) = ( len fp) and

 A7: for d st d in ( dom fr1) holds (fr1 . d) = ((fp . d) * (x |^ (d -' 1))) and

 A8: (f1 . x) = ( Sum fr1) by A4;

 consider fr2 be FinSequence of INT such that

 A9: ( len fr2) = ( len fp) and

 A10: for d st d in ( dom fr2) holds (fr2 . d) = ((fp . d) * (x |^ (d -' 1))) and

 A11: (f2 . x) = ( Sum fr2) by A5;



 A12: ( dom fr1) = ( dom fr2) by A6, A9, FINSEQ_3: 29;

 for d be Nat st d in ( dom fr1) holds (fr1 . d) = (fr2 . d)

 proof

 let d be Nat;

 assume

 A13: d in ( dom fr1);



 hence (fr2 . d) = ((fp . d) * (x |^ (d -' 1))) by A10, A12

 .= (fr1 . d) by A7, A13;

 end;

 hence thesis by A8, A11, A12, FINSEQ_1: 13;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 theorem :: INT_5:3



 Th3: ( len fp) = 1 implies ( Poly-INT fp) = ( INT --> (fp . 1))

 proof

 assume

 A1: ( len fp) = 1;

 for x be object st x in ( dom ( Poly-INT fp)) holds (( Poly-INT fp) . x) = (fp . 1)

 proof

 let x be object;

 assume x in ( dom ( Poly-INT fp));

 then

 reconsider x as Element of INT ;

 consider fr be FinSequence of INT such that

 A2: ( len fr) = ( len fp) and

 A3: for d st d in ( dom fr) holds (fr . d) = ((fp . d) * (x |^ (d -' 1))) and

 A4: (( Poly-INT fp) . x) = ( Sum fr) by Def1;

 1 in ( dom fr) by A1, A2, FINSEQ_3: 25;



 then

 A5: (fr . 1) = ((fp . 1) * (x |^ (1 -' 1))) by A3

 .= ((fp . 1) * (x |^ 0 )) by XREAL_1: 232

 .= ((fp . 1) * 1) by NEWTON: 4;

 fr = <*(fr . 1)*> by A1, A2, FINSEQ_1: 40;

 hence thesis by A4, A5, RVSUM_1: 73;

 end;

 then ( Poly-INT fp) = (( dom ( Poly-INT fp)) --> (fp . 1)) by FUNCOP_1: 11;

 hence thesis by FUNCT_2:def 1;

 end;

 theorem :: INT_5:4

 ( len fp) = 1 implies for x be Element of INT holds (( Poly-INT fp) . x) = (fp . 1)

 proof

 assume

 A1: ( len fp) = 1;

 let x be Element of INT ;

 consider fr be FinSequence of INT such that

 A2: ( len fr) = ( len fp) and

 A3: for d st d in ( dom fr) holds (fr . d) = ((fp . d) * (x |^ (d -' 1))) and

 A4: (( Poly-INT fp) . x) = ( Sum fr) by Def1;

 1 in ( dom fr) by A1, A2, FINSEQ_3: 25;



 then

 A5: (fr . 1) = ((fp . 1) * (x |^ (1 -' 1))) by A3

 .= ((fp . 1) * (x |^ 0 )) by XREAL_1: 232

 .= ((fp . 1) * 1) by NEWTON: 4;

 fr = <*(fr . 1)*> by A1, A2, FINSEQ_1: 40;

 hence thesis by A4, A5, RVSUM_1: 73;

 end;

 reserve fr for FinSequence of REAL ;

 theorem :: INT_5:5



 Th5: for f, f1, f2 st ( len f) = (n + 1) & ( len f1) = ( len f) & ( len f2) = ( len f) & (for d st d in ( dom f) holds (f . d) = ((f1 . d) - (f2 . d))) holds ex fr st ( len fr) = (( len f) - 1) & (for d st d in ( dom fr) holds (fr . d) = ((f1 . d) - (f2 . (d + 1)))) & ( Sum f) = ((( Sum fr) + (f1 . (n + 1))) - (f2 . 1))

 proof

 defpred P[ Nat] means for f, f1, f2 st ( len f) = ($1 + 1) & ( len f1) = ( len f) & ( len f2) = ( len f) & (for d st d in ( dom f) holds (f . d) = ((f1 . d) - (f2 . d))) holds ex fr st ( len fr) = (( len f) - 1) & (for d st d in ( dom fr) holds (fr . d) = ((f1 . d) - (f2 . (d + 1)))) & ( Sum f) = ((( Sum fr) + (f1 . ($1 + 1))) - (f2 . 1));



 A1: for n st P[n] holds P[(n + 1)]

 proof

 let n;

 assume

 A2: P[n];

 let f, f1, f2;

 assume that

 A3: ( len f) = ((n + 1) + 1) and

 A4: ( len f1) = ( len f) and

 A5: ( len f2) = ( len f) and

 A6: for d st d in ( dom f) holds (f . d) = ((f1 . d) - (f2 . d));

 set ff1 = (f1 | ( Seg (n + 1)));

 reconsider ff1 as FinSequence of REAL by FINSEQ_1: 18;



 A7: ( len ff1) = (n + 1) by A3, A4, FINSEQ_3: 53;

 set ff2 = (f2 | ( Seg (n + 1)));

 reconsider ff2 as FinSequence of REAL by FINSEQ_1: 18;



 A8: f2 = (ff2 ^ <*(f2 . ((n + 1) + 1))*>) by A3, A5, FINSEQ_3: 55;



 A9: ( len ff2) = (n + 1) by A3, A5, FINSEQ_3: 53;

 then ff2 <> {} ;

 then 1 in ( dom ff2) by FINSEQ_5: 6;

 then

 A10: (ff2 . 1) = (f2 . 1) by A8, FINSEQ_1:def 7;



 A11: f1 = (ff1 ^ <*(f1 . ((n + 1) + 1))*>) by A3, A4, FINSEQ_3: 55;

 ((n + 1) + 1) in ( Seg ((n + 1) + 1)) by FINSEQ_1: 4;

 then ((n + 1) + 1) in ( dom f) by A3, FINSEQ_1:def 3;

 then

 A12: (f . ((n + 1) + 1)) = ((f1 . ((n + 1) + 1)) - (f2 . ((n + 1) + 1))) by A6;

 set f3 = (f | ( Seg (n + 1)));

 reconsider f3 as FinSequence of REAL by FINSEQ_1: 18;



 A13: ( dom f3) = ( Seg (n + 1)) by A3, FINSEQ_3: 54;

 then

 A14: ( len f3) = (n + 1) by FINSEQ_1:def 3;



 A15: f = (f3 ^ <*(f . ((n + 1) + 1))*>) by A3, FINSEQ_3: 55;



 A16: for d st d in ( dom f3) holds (f3 . d) = ((ff1 . d) - (ff2 . d))

 proof

 let d;



 A17: ( dom f3) c= ( dom f) by A15, FINSEQ_1: 26;

 assume

 A18: d in ( dom f3);

 then

 A19: d in ( dom ff2) by A13, A9, FINSEQ_1:def 3;

 d in ( dom ff1) by A13, A7, A18, FINSEQ_1:def 3;

 then

 A20: (f1 . d) = (ff1 . d) by A11, FINSEQ_1:def 7;

 (f3 . d) = (f . d) by A15, A18, FINSEQ_1:def 7

 .= ((f1 . d) - (f2 . d)) by A6, A18, A17;

 hence thesis by A8, A19, A20, FINSEQ_1:def 7;

 end;

 ff1 <> {} by A7;

 then (n + 1) in ( dom ff1) by A7, FINSEQ_5: 6;

 then (ff1 . (n + 1)) = (f1 . (n + 1)) by A11, FINSEQ_1:def 7;

 then

 consider f4 be FinSequence of REAL such that

 A21: ( len f4) = (( len f3) - 1) and

 A22: for d st d in ( dom f4) holds (f4 . d) = ((ff1 . d) - (ff2 . (d + 1))) and

 A23: ( Sum f3) = ((( Sum f4) + (f1 . (n + 1))) - (f2 . 1)) by A2, A14, A7, A9, A16, A10;

 take f5 = (f4 ^ <*((f1 . (n + 1)) - (f2 . (n + 2)))*>);

 ((f1 . (n + 1)) - (f2 . (n + 2))) is Element of REAL by XREAL_0:def 1;

 then <*((f1 . (n + 1)) - (f2 . (n + 2)))*> is FinSequence of REAL by FINSEQ_1: 74;

 then

 reconsider f5 as FinSequence of REAL by FINSEQ_1: 75;



 A24: ( Sum f) = (((( Sum f4) + (f1 . (n + 1))) - (f2 . 1)) + (f . ((n + 1) + 1))) by A15, A23, RVSUM_1: 74

 .= (((( Sum f4) + ((f1 . (n + 1)) - (f2 . (n + 2)))) + (f1 . ((n + 1) + 1))) - (f2 . 1)) by A12

 .= ((( Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1)) by RVSUM_1: 74;



 A25: (( len f4) + 1) = (n + 1) by A13, A21, FINSEQ_1:def 3;



 A26: for d st d in ( dom f5) holds (f5 . d) = ((f1 . d) - (f2 . (d + 1)))

 proof

 let d;

 assume d in ( dom f5);

 then d in ( Seg ( len f5)) by FINSEQ_1:def 3;

 then d in ( Seg (( len f4) + 1)) by FINSEQ_2: 16;

 then d in (( Seg ( len f4)) \/ {(( len f4) + 1)}) by FINSEQ_1: 9;

 then

 A27: d in ( Seg ( len f4)) or d in {(( len f4) + 1)} by XBOOLE_0:def 3;

 per cases by A27, TARSKI:def 1;

 suppose

 A28: d in ( Seg ( len f4));

 then (d + 1) in ( Seg (( len f4) + 1)) by FINSEQ_1: 60;

 then (d + 1) in ( Seg ( len ff2)) by A3, A5, A14, A21, FINSEQ_3: 53;

 then

 A29: (d + 1) in ( dom ff2) by FINSEQ_1:def 3;



 A30: d in ( dom f4) by A28, FINSEQ_1:def 3;

 ( len f4) <= ( len ff1) by A14, A7, A21, XREAL_1: 147;

 then ( dom f4) c= ( dom ff1) by FINSEQ_3: 30;

 then

 A31: (f1 . d) = (ff1 . d) by A11, A30, FINSEQ_1:def 7;

 (f5 . d) = (f4 . d) by A30, FINSEQ_1:def 7

 .= ((ff1 . d) - (ff2 . (d + 1))) by A22, A30;

 hence thesis by A8, A31, A29, FINSEQ_1:def 7;

 end;

 suppose

 A32: d = (( len f4) + 1);

 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

 then 1 in ( dom <*((f1 . (n + 1)) - (f2 . (n + 2)))*>) by FINSEQ_1: 38;



 then (f5 . d) = ( <*((f1 . (n + 1)) - (f2 . (n + 2)))*> . 1) by A32, FINSEQ_1:def 7

 .= ((f1 . d) - (f2 . (d + 1))) by A25, A32, FINSEQ_1: 40;

 hence thesis;

 end;

 end;

 ( len f5) = (( len f4) + 1) by FINSEQ_2: 16

 .= (( len f) - 1) by A3, A13, A21, FINSEQ_1:def 3;

 hence thesis by A26, A24;

 end;



 A33: P[ 0 ]

 proof

 let f, f1, f2;

 assume that

 A34: ( len f) = ( 0 + 1) and ( len f1) = ( len f) and ( len f2) = ( len f) and

 A35: for d st d in ( dom f) holds (f . d) = ((f1 . d) - (f2 . d));

 take ( <*> REAL );

 ( 0 + 1) in ( Seg ( 0 + 1)) by FINSEQ_1: 4;

 then 1 in ( dom f) by A34, FINSEQ_1:def 3;

 then (f . 1) = ((f1 . 1) - (f2 . 1)) by A35;

 then f = <*((f1 . 1) - (f2 . 1))*> by A34, FINSEQ_1: 40;

 hence thesis by A34, RVSUM_1: 72, RVSUM_1: 73;

 end;

 for n holds P[n] from NAT_1:sch 2( A33, A1);

 hence thesis;

 end;

 theorem :: INT_5:6



 Th6: ( len fp) = (n + 2) implies for a be Integer holds ex fr be FinSequence of INT , r be Integer st ( len fr) = (n + 1) & (for x be Element of INT holds (( Poly-INT fp) . x) = (((x - a) * (( Poly-INT fr) . x)) + r)) & (fp . (n + 2)) = (fr . (n + 1))

 proof

 assume

 A1: ( len fp) = (n + 2);

 ((n + 1) + 1) in ( Seg ((n + 1) + 1)) by FINSEQ_1: 4;

 then (n + 2) in ( dom fp) by A1, FINSEQ_1:def 3;

 then

 reconsider A = (fp . (n + 2)) as Element of INT by FINSEQ_2: 11;

 reconsider n1 = (n + 1) as Element of NAT ;

 let a be Integer;

 defpred P[ Nat, Integer, set] means $3 = ((fp . ((n + 2) - $1)) + (a * $2));



 A2: for d be Nat st 1 <= d & d < n1 holds for x be Element of INT holds ex y be Element of INT st P[d, x, y]

 proof

 let d be Nat;

 assume that 1 <= d and d < n1;

 let x be Element of INT ;

 set y = ((fp . ((n + 2) - d)) + (a * x));

 reconsider y as Element of INT by INT_1:def 2;

 take y;

 thus thesis;

 end;

 consider p be FinSequence of INT such that

 A3: ( len p) = n1 & ((p . 1) = A or n1 = 0 ) & for d be Nat st 1 <= d & d < n1 holds P[d, (p . d), (p . (d + 1))] from RECDEF_1:sch 4( A2);

 take fr = ( Rev p);

 take r = ((fp . 1) + (a * (fr . 1)));



 A4: ( len fr) = (n + 1) by A3, FINSEQ_5:def 3;

 for x be Element of INT holds (( Poly-INT fp) . x) = (((x - a) * (( Poly-INT fr) . x)) + r)

 proof

 let x be Element of INT ;

 deffunc F( Nat) = ((fr . $1) * (x |^ $1));

 deffunc FF( Nat) = ((a * (fr . $1)) * (x |^ ($1 -' 1)));

 consider f1 be FinSequence of INT such that

 A5: ( len f1) = ( len fp) and

 A6: for d st d in ( dom f1) holds (f1 . d) = ((fp . d) * (x |^ (d -' 1))) and

 A7: (( Poly-INT fp) . x) = ( Sum f1) by Def1;



 A8: f1 <> {} by A1, A5;

 then (n + 2) in ( dom f1) by A1, A5, FINSEQ_5: 6;

 then (f1 . (n + 2)) = ((fp . (n + 2)) * (x |^ (((n + 1) + 1) -' 1))) by A6;

 then

 A9: (f1 . (n + 2)) = ((fp . (n + 2)) * (x |^ (n + 1))) by NAT_D: 34;

 (f1 . 1) = ((fp . 1) * (x |^ (1 -' 1))) by A6, A8, FINSEQ_5: 6;

 then (f1 . 1) = ((fp . 1) * (x |^ 0 )) by XREAL_1: 232;

 then

 A10: (f1 . 1) = ((fp . 1) * 1) by NEWTON: 4;

 reconsider n as Element of NAT by ORDINAL1:def 12;

 consider f4 be FinSequence such that

 A11: ( len f4) = (n + 1) & for d be Nat st d in ( dom f4) holds (f4 . d) = F(d) from FINSEQ_1:sch 2;



 A12: for d be Nat st d in ( dom f4) holds (f4 . d) in INT

 proof

 let d be Nat;

 reconsider d1 = d as Element of NAT by ORDINAL1:def 12;

 assume d in ( dom f4);

 then (f4 . d1) = ((fr . d1) * (x |^ d1)) by A11;

 hence thesis by INT_1:def 2;

 end;

 f4 <> {} by A11;

 then (n + 1) in ( dom f4) by A11, FINSEQ_5: 6;

 then (f4 . (n + 1)) = ((fr . (n + 1)) * (x |^ (n + 1))) by A11;

 then

 A13: (f4 . (n + 1)) = ((fp . (n + 2)) * (x |^ (n + 1))) by A3, FINSEQ_5: 62;

 reconsider f4 as FinSequence of INT by A12, FINSEQ_2: 12;

 consider f5 be FinSequence such that

 A14: ( len f5) = (n + 1) & for d be Nat st d in ( dom f5) holds (f5 . d) = FF(d) from FINSEQ_1:sch 2;



 A15: for d be Nat st d in ( dom f5) holds (f5 . d) in INT

 proof

 let d be Nat;

 assume d in ( dom f5);

 then (f5 . d) = ((a * (fr . d)) * (x |^ (d -' 1))) by A14;

 hence thesis by INT_1:def 2;

 end;

 f5 <> {} by A14;

 then 1 in ( dom f5) by FINSEQ_5: 6;

 then (f5 . 1) = ((a * (fr . 1)) * (x |^ (1 -' 1))) by A14;

 then (f5 . 1) = ((a * (fr . 1)) * (x |^ 0 )) by XREAL_1: 232;

 then

 A16: (f5 . 1) = ((a * (fr . 1)) * 1) by NEWTON: 4;

 reconsider f5 as FinSequence of INT by A15, FINSEQ_2: 12;



 A17: f4 is FinSequence of REAL by FINSEQ_3: 117;

 consider f2 be FinSequence of INT such that

 A18: ( len f2) = ( len fr) and

 A19: for d st d in ( dom f2) holds (f2 . d) = ((fr . d) * (x |^ (d -' 1))) and

 A20: (( Poly-INT fr) . x) = ( Sum f2) by Def1;

 set f3 = ((x - a) * f2);



 A21: ( dom f3) = ( dom f2) by VALUED_1:def 5;

 then

 A22: ( len f3) = ( len f2) by FINSEQ_3: 29;



 A23: ( dom f3) = ( dom f4) by A4, A18, A11, A21, FINSEQ_3: 29;



 A24: for k be Element of NAT st k in ( dom f3) holds (f3 . k) = (((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1))))

 proof

 let k be Element of NAT ;

 assume

 A25: k in ( dom f3);

 then

 A26: k >= 1 by FINSEQ_3: 25;



 A27: k in ( dom f2) by A25, VALUED_1:def 5;



 thus (f3 . k) = ((x - a) * (f2 . k)) by A25, VALUED_1:def 5

 .= ((x - a) * ((fr . k) * (x |^ (k -' 1)))) by A19, A27

 .= (((fr . k) * ((x |^ (k -' 1)) * x)) - ((a * (fr . k)) * (x |^ (k -' 1))))

 .= (((fr . k) * (x |^ ((k -' 1) + 1))) - ((a * (fr . k)) * (x |^ (k -' 1)))) by NEWTON: 6

 .= (((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1)))) by A26, XREAL_1: 235;

 end;



 A28: ( dom f3) = ( dom f5) by A4, A18, A14, A21, FINSEQ_3: 29;



 A29: for d st d in ( dom f3) holds (f3 . d) = ((f4 . d) - (f5 . d))

 proof

 let d;

 assume

 A30: d in ( dom f3);

 then

 A31: (f5 . d) = ((a * (fr . d)) * (x |^ (d -' 1))) by A14, A28;

 (f4 . d) = ((fr . d) * (x |^ d)) by A11, A23, A30;

 hence thesis by A24, A30, A31;

 end;

 f5 is FinSequence of REAL by FINSEQ_3: 117;

 then

 consider f6 be FinSequence of REAL such that

 A32: ( len f6) = (( len f3) - 1) and

 A33: for d st d in ( dom f6) holds (f6 . d) = ((f4 . d) - (f5 . (d + 1))) and

 A34: ( Sum f3) = ((( Sum f6) + (f4 . (n + 1))) - (f5 . 1)) by A4, A18, A11, A14, A22, A29, A17, Th5;



 A35: ( len f6) <= ( len f3) by A4, A18, A22, A32, XREAL_1: 145;

 then

 A36: ( dom f6) c= ( dom f3) by FINSEQ_3: 30;



 A37: for d be Element of NAT st d in ( dom f6) holds (f6 . d) = (f1 . (d + 1))

 proof

 let d be Element of NAT ;



 A38: ( dom f6) c= ( dom p) by A3, A4, A18, A22, A35, FINSEQ_3: 30;

 assume

 A39: d in ( dom f6);

 then

 A40: d in ( Seg n) by A4, A18, A22, A32, FINSEQ_1:def 3;

 then

 A41: d <= n by FINSEQ_1: 1;

 then

 A42: (n - d) >= 0 by XREAL_1: 48;

 then

 reconsider d9 = ((n - d) + 1) as Element of NAT by INT_1: 3;

 d >= 1 by A40, FINSEQ_1: 1;

 then (n - d) <= (n - 1) by XREAL_1: 10;

 then d9 <= ((n - 1) + 1) by XREAL_1: 6;

 then

 A43: d9 < (n + 1) by XREAL_1: 145;

 d9 >= ( 0 + 1) by A42, XREAL_1: 6;

 then

 A44: (p . (d9 + 1)) = ((fp . ((n + 2) - d9)) + (a * (p . d9))) by A3, A43;

 d < (n + 1) by A41, XREAL_1: 145;

 then

 A45: (d + 1) in ( Seg (n + 1)) by FINSEQ_3: 11;

 then

 A46: (d + 1) in ( dom f5) by A14, FINSEQ_1:def 3;

 (d + 0 ) < (n + 2) by A41, XREAL_1: 8;

 then (d + 1) in ( Seg (n + 2)) by FINSEQ_3: 11;

 then

 A47: (d + 1) in ( dom f1) by A1, A5, FINSEQ_1:def 3;



 A48: (d + 1) in ( dom p) by A3, A45, FINSEQ_1:def 3;



 thus (f6 . d) = ((f4 . d) - (f5 . (d + 1))) by A33, A39

 .= (((fr . d) * (x |^ d)) - (f5 . (d + 1))) by A11, A23, A36, A39

 .= (((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ ((d + 1) -' 1)))) by A14, A46

 .= (((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ d))) by NAT_D: 34

 .= (((fr . d) - (a * (fr . (d + 1)))) * (x |^ d))

 .= (((p . (((n + 1) - d) + 1)) - (a * (fr . (d + 1)))) * (x |^ d)) by A3, A39, A38, FINSEQ_5: 58

 .= (((p . (((n - d) + 1) + 1)) - (a * (p . (((n + 1) - (d + 1)) + 1)))) * (x |^ d)) by A3, A48, FINSEQ_5: 58

 .= ((fp . (d + 1)) * (x |^ ((d + 1) -' 1))) by A44, NAT_D: 34

 .= (f1 . (d + 1)) by A6, A47;

 end;

 f1 = (( <*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>)

 proof

 set K = (( <*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>);



 A49: for d be Nat st d in ( dom f1) holds (f1 . d) = (K . d)

 proof

 let d be Nat;

 assume

 A50: d in ( dom f1);

 then

 A51: d >= 1 by FINSEQ_3: 25;



 A52: d <= (n + 2) by A1, A5, A50, FINSEQ_3: 25;

 per cases by A51, A52, XXREAL_0: 1;

 suppose

 A53: d = 1;



 hence (K . d) = (( <*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . 1) by FINSEQ_1: 32

 .= (f1 . d) by A53, FINSEQ_1: 41;

 end;

 suppose

 A54: d > 1 & d < (n + 2);

 then

 reconsider w = (d - 1) as Element of NAT by INT_1: 3;

 (d - 1) < ((n + 2) - 1) by A54, XREAL_1: 9;

 then

 A55: (d - 1) <= ((n + 1) - 1) by INT_1: 7;

 (d - 1) >= ( 0 + 1) by A54, INT_1: 7, XREAL_1: 50;

 then w in ( Seg n) by A55, FINSEQ_1: 1;

 then

 A56: w in ( dom f6) by A4, A18, A22, A32, FINSEQ_1:def 3;

 then

 A57: w in ( dom (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_2: 15;



 thus (K . d) = (( <*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . (w + 1)) by FINSEQ_1: 32

 .= ((f6 ^ <*(f1 . (n + 2))*>) . w) by A57, FINSEQ_3: 103

 .= (f6 . w) by A56, FINSEQ_1:def 7

 .= (f1 . (w + 1)) by A37, A56

 .= (f1 . d);

 end;

 suppose

 A58: d = (n + 2);

 set K1 = ( <*(f1 . 1)*> ^ f6);



 thus (K . d) = (K . ((n + 1) + 1)) by A58

 .= (K . (( len K1) + 1)) by A4, A18, A22, A32, FINSEQ_5: 8

 .= (f1 . d) by A58, FINSEQ_1: 42;

 end;

 end;

 ( len K) = ( len ( <*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))) by FINSEQ_1: 32

 .= (1 + ( len (f6 ^ <*(f1 . (n + 2))*>))) by FINSEQ_5: 8

 .= ((1 + ( len f6)) + 1) by FINSEQ_2: 16

 .= ( len f1) by A1, A4, A5, A18, A22, A32;

 hence thesis by A49, FINSEQ_3: 29;

 end;



 then ( Sum f1) = ( Sum ( <*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))) by FINSEQ_1: 32

 .= ((f1 . 1) + ( Sum (f6 ^ <*(f1 . (n + 2))*>))) by RVSUM_1: 76

 .= ((f1 . 1) + (( Sum f6) + (f1 . (n + 2)))) by RVSUM_1: 74

 .= (( Sum ((x - a) * f2)) + r) by A10, A9, A13, A16, A34

 .= (((x - a) * (( Poly-INT fr) . x)) + r) by A20, RVSUM_1: 87;

 hence thesis by A7;

 end;

 hence thesis by A3, FINSEQ_5: 62, FINSEQ_5:def 3;

 end;

 theorem :: INT_5:7



 Th7: p divides (i * j) implies p divides i or p divides j

 proof

 assume

 A1: p divides (i * j);

 per cases ;

 suppose i >= 0 & j >= 0 ;

 then

 reconsider i, j as Element of NAT by INT_1: 3;

 p divides (i * j) by A1;

 hence thesis by NEWTON: 80;

 end;

 suppose i >= 0 & j < 0 ;

 then

 reconsider i, j9 = ( - j) as Element of NAT by INT_1: 3;

 p divides ( - (i * j)) by A1, INT_2: 10;

 then p divides (i * j9);

 then p divides i or p divides j9 by NEWTON: 80;

 hence thesis by INT_2: 10;

 end;

 suppose i < 0 & j >= 0 ;

 then

 reconsider i9 = ( - i), j as Element of NAT by INT_1: 3;

 p divides ( - (i * j)) by A1, INT_2: 10;

 then p divides (i9 * j);

 then p divides i9 or p divides j by NEWTON: 80;

 hence thesis by INT_2: 10;

 end;

 suppose i < 0 & j < 0 ;

 then

 reconsider i9 = ( - i), j9 = ( - j) as Element of NAT by INT_1: 3;

 p divides (i9 * j9) by A1;

 then p divides i9 or p divides j9 by NEWTON: 80;

 hence thesis by INT_2: 10;

 end;

 end;

 reserve fr,f for FinSequence of INT ;

 theorem :: INT_5:8



 Th8: for fp st ( len fp) = (n + 1) & p > 2 & not p divides (fp . (n + 1)) holds for fr st (for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 ) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p) holds ( len fr) <= n

 proof

 defpred P[ Nat] means for fp st ( len fp) = ($1 + 1) & p > 2 & not p divides (fp . ($1 + 1)) holds for fr st (for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 ) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p) holds ( len fr) <= $1;



 A1: for n st P[n] holds P[(n + 1)]

 proof

 let n;

 assume

 A2: P[n];

 let fp;

 assume that

 A3: ( len fp) = ((n + 1) + 1) and

 A4: p > 2 and

 A5: not p divides (fp . ((n + 1) + 1));

 per cases ;

 suppose

 A6: for x holds ((( Poly-INT fp) . x) mod p) <> 0 ;

 assume ex fr st (for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 ) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p) & ( len fr) > (n + 1);

 then

 consider fr such that

 A7: for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 and for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p and

 A8: ( len fr) > (n + 1);

 fr <> {} by A8;

 then ((( Poly-INT fp) . (fr . 1)) mod p) = 0 by A7, FINSEQ_5: 6;

 hence contradiction by A6;

 end;

 suppose ex a be Integer st ((( Poly-INT fp) . a) mod p) = 0 ;

 then

 consider a be Integer such that

 A9: ((( Poly-INT fp) . a) mod p) = 0 ;

 assume ex f st (for d st d in ( dom f) holds ((( Poly-INT fp) . (f . d)) mod p) = 0 ) & (for d, e st d in ( dom f) & e in ( dom f) & d <> e holds not ((f . d),(f . e)) are_congruent_mod p) & ( len f) > (n + 1);

 then

 consider f such that

 A10: for d st d in ( dom f) holds ((( Poly-INT fp) . (f . d)) mod p) = 0 and

 A11: for d, e st d in ( dom f) & e in ( dom f) & d <> e holds not ((f . d),(f . e)) are_congruent_mod p and

 A12: ( len f) > (n + 1);

 consider fk, r such that

 A13: ( len fk) = (n + 1) and

 A14: for x be Element of INT holds (( Poly-INT fp) . x) = (((x - a) * (( Poly-INT fk) . x)) + r) and

 A15: (fp . (n + 2)) = (fk . (n + 1)) by A3, Th6;

 a is Element of INT by INT_1:def 2;



 then

 A16: ((( Poly-INT fp) . a) mod p) = ((((a - a) * (( Poly-INT fk) . a)) + r) mod p) by A14

 .= (r mod p);



 A17: for d be Element of NAT st d in ( dom f) holds p divides (((f . d) - a) * (( Poly-INT fk) . (f . d)))

 proof

 let d be Element of NAT ;

 (f . d) is Element of INT by INT_1:def 2;



 then

 A18: ((( Poly-INT fp) . (f . d)) mod p) = (((((f . d) - a) * (( Poly-INT fk) . (f . d))) + r) mod p) by A14

 .= ((((((f . d) - a) * (( Poly-INT fk) . (f . d))) mod p) + (r mod p)) mod p) by NAT_D: 66

 .= ((((f . d) - a) * (( Poly-INT fk) . (f . d))) mod p) by A9, A16, NAT_D: 65;

 assume d in ( dom f);

 then ((((f . d) - a) * (( Poly-INT fk) . (f . d))) mod p) = 0 by A10, A18;

 hence thesis by INT_1: 62;

 end;

 per cases ;

 suppose

 A19: for d st d in ( dom f) holds not p divides ((f . d) - a);

 for d st d in ( dom f) holds ((( Poly-INT fk) . (f . d)) mod p) = 0

 proof

 let d;

 assume

 A20: d in ( dom f);

 then p divides (((f . d) - a) * (( Poly-INT fk) . (f . d))) by A17;

 then p divides ((f . d) - a) or p divides (( Poly-INT fk) . (f . d)) by Th7;

 hence thesis by A19, A20, INT_1: 62;

 end;

 then ( len f) <= n by A2, A4, A5, A13, A15, A11;

 hence contradiction by A12, XREAL_1: 145;

 end;

 suppose ex d st d in ( dom f) & p divides ((f . d) - a);

 then

 consider d9 be Element of NAT such that

 A21: d9 in ( dom f) and

 A22: p divides ((f . d9) - a);

 set f9 = (f - {(f . d9)});



 A23: for d st d in ( dom f9) holds not p divides ((f9 . d) - a)

 proof

 given k be Nat such that

 A24: k in ( dom f9) and

 A25: p divides ((f9 . k) - a);

 (f9 . k) in ( rng f9) by A24, FUNCT_1: 3;

 then

 A26: (f9 . k) in (( rng f) \ {(f . d9)}) by FINSEQ_3: 65;

 then (f9 . k) in ( rng f) by XBOOLE_0:def 5;

 then

 consider w be object such that

 A27: w in ( dom f) and

 A28: (f . w) = (f9 . k) by FUNCT_1:def 3;

 reconsider w as Element of NAT by A27;

 p divides (((f . w) - a) - ((f . d9) - a)) by A22, A25, A28, Th1;

 then

 A29: ((f . w),(f . d9)) are_congruent_mod p;

 not (f9 . k) in {(f . d9)} by A26, XBOOLE_0:def 5;

 then w <> d9 by A28, TARSKI:def 1;

 hence contradiction by A11, A21, A27, A29;

 end;



 A30: for d st d in ( dom f9) holds ((( Poly-INT fk) . (f9 . d)) mod p) = 0

 proof

 let d;

 assume

 A31: d in ( dom f9);

 then (f9 . d) in ( rng f9) by FUNCT_1: 3;

 then (f9 . d) in (( rng f) \ {(f . d9)}) by FINSEQ_3: 65;

 then (f9 . d) in ( rng f) by XBOOLE_0:def 5;

 then ex w be object st w in ( dom f) & (f . w) = (f9 . d) by FUNCT_1:def 3;

 then p divides (((f9 . d) - a) * (( Poly-INT fk) . (f9 . d))) by A17;

 then p divides ((f9 . d) - a) or p divides (( Poly-INT fk) . (f9 . d)) by Th7;

 hence thesis by A23, A31, INT_1: 62;

 end;



 A32: f is one-to-one by A11, INT_1: 11;

 then

 A33: f9 is one-to-one by FINSEQ_3: 87;



 A34: for d, e st d in ( dom f9) & e in ( dom f9) & d <> e holds not ((f9 . d),(f9 . e)) are_congruent_mod p

 proof

 let d, e;

 assume that

 A35: d in ( dom f9) and

 A36: e in ( dom f9) and

 A37: d <> e;

 (f9 . e) in ( rng f9) by A36, FUNCT_1: 3;

 then (f9 . e) in (( rng f) \ {(f . d9)}) by FINSEQ_3: 65;

 then (f9 . e) in ( rng f) by XBOOLE_0:def 5;

 then

 consider w2 be object such that

 A38: w2 in ( dom f) and

 A39: (f9 . e) = (f . w2) by FUNCT_1:def 3;

 (f9 . d) in ( rng f9) by A35, FUNCT_1: 3;

 then (f9 . d) in (( rng f) \ {(f . d9)}) by FINSEQ_3: 65;

 then (f9 . d) in ( rng f) by XBOOLE_0:def 5;

 then

 consider w1 be object such that

 A40: w1 in ( dom f) and

 A41: (f9 . d) = (f . w1) by FUNCT_1:def 3;

 reconsider w1, w2 as Element of NAT by A40, A38;

 w1 <> w2 by A33, A35, A36, A37, A41, A39;

 hence thesis by A11, A40, A41, A38, A39;

 end;

 (f . d9) in ( rng f) by A21, FUNCT_1: 3;

 then ( len f9) = (( len f) - 1) by A32, FINSEQ_3: 90;

 then ( len f9) > ((n + 1) - 1) by A12, XREAL_1: 9;

 hence contradiction by A2, A4, A5, A13, A15, A30, A34;

 end;

 end;

 end;



 A42: P[ 0 ]

 proof

 let fp;

 assume that

 A43: ( len fp) = ( 0 + 1) and p > 2 and

 A44: not p divides (fp . ( 0 + 1));

 assume ex fr st (for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 ) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p) & ( len fr) > 0 ;

 then

 consider fr such that

 A45: for d st d in ( dom fr) holds ((( Poly-INT fp) . (fr . d)) mod p) = 0 and for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds not ((fr . d),(fr . e)) are_congruent_mod p and

 A46: ( len fr) > 0 ;

 fr <> {} by A46;

 then

 A47: ((( Poly-INT fp) . (fr . 1)) mod p) = 0 by A45, FINSEQ_5: 6;



 A48: (fr . 1) in INT by INT_1:def 2;

 (( Poly-INT fp) . (fr . 1)) = (( INT --> (fp . 1)) . (fr . 1)) by A43, Th3

 .= (fp . 1) by A48, FUNCOP_1: 7;

 hence contradiction by A44, A47, Lm1;

 end;

 for n holds P[n] from NAT_1:sch 2( A42, A1);

 hence thesis;

 end;

 definition

 let a be Integer, m be natural Number;

 :: INT_5:def2

 pred a is_quadratic_residue_mod m means ex x be Integer st (((x ^2 ) - a) mod m) = 0 ;

 end

 reserve b,m for Nat;

 theorem :: INT_5:9



 Th9: (a ^2 ) is_quadratic_residue_mod m

 proof

 (((a ^2 ) - (a ^2 )) mod m) = 0 by INT_1: 73;

 hence thesis;

 end;

 theorem :: INT_5:10

 1 is_quadratic_residue_mod 2

 proof

 (1 ^2 ) is_quadratic_residue_mod 2 by Th9;

 hence thesis;

 end;

 theorem :: INT_5:11



 Th11: i is_quadratic_residue_mod m & (i,j) are_congruent_mod m implies j is_quadratic_residue_mod m

 proof

 assume that

 A1: i is_quadratic_residue_mod m and

 A2: (i,j) are_congruent_mod m;

 consider x be Integer such that

 A3: (((x ^2 ) - i) mod m) = 0 by A1;



 A4: ((i - j) mod m) = 0 by Lm1, A2;

 (((x ^2 ) - j) mod m) = ((((x ^2 ) - i) + (i - j)) mod m)

 .= (((((x ^2 ) - i) mod m) + ((i - j) mod m)) mod m) by NAT_D: 66

 .= 0 by A3, A4, NAT_D: 65;

 hence thesis;

 end;



 Lm2: (i,p) are_coprime or p divides i

 proof

 per cases ;

 suppose i >= 0 ;

 then

 reconsider i as Element of NAT by INT_1: 3;

 (i,p) are_coprime or (i gcd p) = p by PEPIN: 2;

 hence thesis by NAT_D:def 5;

 end;

 suppose

 A1: i < 0 ;

 then

 reconsider m = ( - i) as Element of NAT by INT_1: 3;



 A2: (m,p) are_coprime or (m gcd p) = p by PEPIN: 2;

 per cases by A2, NAT_D:def 5;

 suppose

 A3: (m,p) are_coprime ;

 m = |.i.| by A1, ABSVALUE:def 1;



 then (i gcd p) = (m gcd |.p.|) by INT_2: 34

 .= (m gcd p) by ABSVALUE:def 1

 .= 1 by A3, INT_2:def 3;

 hence thesis by INT_2:def 3;

 end;

 suppose p divides m;

 then

 consider t be Nat such that

 A4: m = (p * t) by NAT_D:def 3;

 i = (p * ( - t)) by A4;

 hence thesis;

 end;

 end;

 end;

 theorem :: INT_5:12



 Th12: i divides j implies (i gcd j) = |.i.|

 proof

 assume i divides j;

 then ( |.i.| gcd |.j.|) = |.i.| by NEWTON: 49, INT_2: 16;

 hence thesis by INT_2: 34;

 end;

 theorem :: INT_5:13



 Th13: for i,j,m be Integer st (i mod m) = (j mod m) holds ((i |^ n) mod m) = ((j |^ n) mod m)

 proof

 let i,j,m be Integer;

 defpred P[ Nat] means ((i |^ $1) mod m) = ((j |^ $1) mod m);

 assume

 A1: (i mod m) = (j mod m);



 A2: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A3: P[n];



 thus ((i |^ (n + 1)) mod m) = (((i |^ n) * i) mod m) by NEWTON: 6

 .= ((((j |^ n) mod m) * (j mod m)) mod m) by A1, A3, NAT_D: 67

 .= (((j |^ n) * j) mod m) by NAT_D: 67

 .= ((j |^ (n + 1)) mod m) by NEWTON: 6;

 end;

 (i |^ 0 ) = 1 by NEWTON: 4;

 then

 A4: P[ 0 ] by NEWTON: 4;

 for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

 hence thesis;

 end;

 theorem :: INT_5:14



 Th14: (a gcd p) = 1 & (((x ^2 ) - a) mod p) = 0 implies (x,p) are_coprime

 proof

 assume that

 A1: (a gcd p) = 1 and

 A2: (((x ^2 ) - a) mod p) = 0 ;

 assume not (x,p) are_coprime ;

 then

 A3: p divides (x ^2 ) by Lm2, INT_2: 2;

 p divides ((x ^2 ) - a) by A2, Lm1;

 then p divides ((x ^2 ) - ((x ^2 ) - a)) by A3, Th1;



 then (p gcd a) = |.p.| by Th12

 .= p by ABSVALUE:def 1;

 hence contradiction by A1, INT_2:def 4;

 end;

 theorem :: INT_5:15

 p > 2 & (a gcd p) = 1 & a is_quadratic_residue_mod p implies ex x,y be Integer st (((x ^2 ) - a) mod p) = 0 & (((y ^2 ) - a) mod p) = 0 & not (x,y) are_congruent_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: a is_quadratic_residue_mod p;

 consider x such that

 A4: (((x ^2 ) - a) mod p) = 0 by A3;

 take x;

 take ( - x);

 not (x,( - x)) are_congruent_mod p

 proof

 assume (x,( - x)) are_congruent_mod p;

 then

 A5: p divides (2 * x);

 (2,p) are_coprime by A1, INT_2: 28, INT_2: 30;

 then (2 gcd p) = 1 by INT_2:def 3;

 then p divides x by A5, WSIERP_1: 29;

 then

 consider i be Integer such that

 A6: x = (p * i);

 (x gcd p) = ((p * i) gcd (p * 1)) by A6

 .= (p * (i gcd 1)) by EULER_1: 15

 .= (p * 1) by WSIERP_1: 8;

 then (x gcd p) <> 1 by INT_2:def 4;

 then not (x,p) are_coprime by INT_2:def 3;

 hence contradiction by A2, A4, Th14;

 end;

 hence thesis by A4;

 end;

 theorem :: INT_5:16



 Th16: p > 2 implies ex fp be FinSequence of NAT st ( len fp) = ((p -' 1) div 2) & (for d st d in ( dom fp) holds ((fp . d) gcd p) = 1) & (for d st d in ( dom fp) holds (fp . d) is_quadratic_residue_mod p) & for d, e st d in ( dom fp) & e in ( dom fp) & d <> e holds not ((fp . d),(fp . e)) are_congruent_mod p

 proof

 deffunc F( Nat) = ($1 ^2 );

 consider fp be FinSequence such that

 A1: ( len fp) = ((p -' 1) div 2) & for d be Nat st d in ( dom fp) holds (fp . d) = F(d) from FINSEQ_1:sch 2;

 for d be Nat st d in ( dom fp) holds (fp . d) in NAT

 proof

 let d be Nat;

 assume d in ( dom fp);

 then (fp . d) = (d ^2 ) by A1;

 hence thesis;

 end;

 then

 reconsider fp as FinSequence of NAT by FINSEQ_2: 12;



 A2: p > 1 by INT_2:def 4;

 then

 A3: (p -' 1) = (p - 1) by XREAL_1: 233;

 assume p > 2;

 then p is odd by PEPIN: 17;

 then (p - 1) is even by HILBERT3: 2;

 then 2 divides (p -' 1) by A3, PEPIN: 22;

 then ((p -' 1) mod 2) = 0 by PEPIN: 6;

 then

 A4: ((p -' 1) div 2) = ((p -' 1) / 2) by PEPIN: 63;



 A5: for d, e st d in ( dom fp) & e in ( dom fp) & d <> e holds not ((fp . d),(fp . e)) are_congruent_mod p

 proof

 (p - 1) > 0 by A2, XREAL_1: 50;

 then ((p - 1) / 2) < ((p - 1) / 1) by XREAL_1: 76;

 then ((p -' 1) div 2) < p by A3, A4, XREAL_1: 147;

 then

 A6: (((p -' 1) div 2) - 1) e;



 A10: e in ( Seg ((p -' 1) div 2)) by A1, A8, FINSEQ_1:def 3;

 then

 A11: e <= ((p -' 1) div 2) by FINSEQ_1: 1;



 A12: d in ( Seg ((p -' 1) div 2)) by A1, A7, FINSEQ_1:def 3;

 then

 A13: d >= 1 by FINSEQ_1: 1;

 then (1 - ((p -' 1) div 2)) <= (d - e) by A11, XREAL_1: 13;

 then

 A14: ( - (((p -' 1) div 2) - 1)) <= (d - e);



 A15: d <= ((p -' 1) div 2) by A12, FINSEQ_1: 1;

 then (d + e) <= (((p -' 1) div 2) + ((p -' 1) div 2)) by A11, XREAL_1: 7;

 then (d + e) < p by A3, A4, XREAL_1: 147;

 then ((d + e),p) are_coprime by A13, EULER_1: 2;

 then

 A16: ((d + e) gcd p) = 1 by INT_2:def 3;

 assume ((fp . d),(fp . e)) are_congruent_mod p;

 then p divides ((d ^2 ) - (fp . e)) by A1, A7;

 then p divides ((d ^2 ) - (e ^2 )) by A1, A8;

 then

 A17: p divides ((d - e) * (d + e));

 (d - e) <> 0 by A9;

 then |.p.| <= |.(d - e).| by A16, A17, INT_4: 6, WSIERP_1: 29;

 then

 A18: p <= |.(d - e).| by ABSVALUE:def 1;

 e >= 1 by A10, FINSEQ_1: 1;

 then (d - e) <= (((p -' 1) div 2) - 1) by A15, XREAL_1: 13;

 then |.(d - e).| <= (((p -' 1) div 2) - 1) by A14, ABSVALUE: 5;

 hence contradiction by A18, A6, XXREAL_0: 2;

 end;



 A19: for d st d in ( dom fp) holds (d gcd p) = 1

 proof

 let d;



 A20: (1 * d) <= (2 * d) by XREAL_1: 64;

 assume d in ( dom fp);

 then

 A21: d in ( Seg ((p -' 1) div 2)) by A1, FINSEQ_1:def 3;

 then d <= ((p -' 1) div 2) by FINSEQ_1: 1;

 then (2 * d) <= (((p -' 1) / 2) * 2) by A4, XREAL_1: 64;

 then d <= (p -' 1) by A20, XXREAL_0: 2;

 then

 A22: d = 1 by A21, FINSEQ_1: 1;

 then (d,p) are_coprime by A22, EULER_1: 2;

 hence thesis by INT_2:def 3;

 end;



 A23: for d st d in ( dom fp) holds ((fp . d) gcd p) = 1

 proof

 let d;

 assume

 A24: d in ( dom fp);

 then (d gcd p) = 1 by A19;

 then ((d ^2 ) gcd p) = 1 by WSIERP_1: 7;

 hence thesis by A1, A24;

 end;

 take fp;

 for d st d in ( dom fp) holds (fp . d) is_quadratic_residue_mod p

 proof

 let d;

 assume

 A25: d in ( dom fp);

 (d ^2 ) is_quadratic_residue_mod p by Th9;

 hence thesis by A1, A25;

 end;

 hence thesis by A1, A23, A5;

 end;

 theorem :: INT_5:17



 Th17: p > 2 & (a gcd p) = 1 & a is_quadratic_residue_mod p implies ((a |^ ((p -' 1) div 2)) mod p) = 1

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: a is_quadratic_residue_mod p;

 consider s be Integer such that

 A4: (((s ^2 ) - a) mod p) = 0 by A3;



 A5: p > 1 by INT_2:def 4;

 p is odd by A1, PEPIN: 17;

 then (p - 1) is even by HILBERT3: 2;

 then (p -' 1) is even by A5, XREAL_1: 233;

 then 2 divides (p -' 1) by PEPIN: 22;

 then

 A6: (p -' 1) = (2 * ((p -' 1) div 2)) by NAT_D: 3;

 ((s ^2 ),a) are_congruent_mod p by A4, INT_1: 62;

 then (a mod p) = ((s ^2 ) mod p) by NAT_D: 64;



 then

 A7: ((a |^ ((p -' 1) div 2)) mod p) = (((s ^2 ) |^ ((p -' 1) div 2)) mod p) by Th13

 .= (((s |^ 2) |^ ((p -' 1) div 2)) mod p) by NEWTON: 81

 .= ((s |^ (p -' 1)) mod p) by A6, NEWTON: 9;



 A8: (s,p) are_coprime by A2, A4, Th14;

 per cases ;

 suppose s >= 0 ;

 then

 reconsider s as Element of NAT by INT_1: 3;

 (s,p) are_coprime by A2, A4, Th14;

 hence thesis by A7, PEPIN: 37;

 end;

 suppose

 A9: s < 0 ;

 then

 reconsider s9 = ( - s) as Element of NAT by INT_1: 3;



 A10: |.p.| = p by ABSVALUE:def 1;

 (s9 gcd p) = ( |.s.| gcd p) by A9, ABSVALUE:def 1

 .= (s gcd p) by A10, INT_2: 34

 .= 1 by A8, INT_2:def 3;

 then (s9,p) are_coprime by INT_2:def 3;

 then

 A11: ((s9 |^ (p -' 1)) mod p) = 1 by PEPIN: 37;

 ((s |^ (p -' 1)) mod p) = (((s |^ 2) |^ ((p -' 1) div 2)) mod p) by A6, NEWTON: 9

 .= (((( - s) |^ 2) |^ ((p -' 1) div 2)) mod p) by WSIERP_1: 1

 .= 1 by A6, A11, NEWTON: 9;

 hence thesis by A7;

 end;

 end;

 theorem :: INT_5:18



 Th18: p > 2 & (b gcd p) = 1 & not b is_quadratic_residue_mod p implies ((b |^ ((p -' 1) div 2)) mod p) = (p - 1)

 proof

 assume that

 A1: p > 2 and

 A2: (b gcd p) = 1 and

 A3: not b is_quadratic_residue_mod p;

 reconsider b as Element of NAT by ORDINAL1:def 12;



 A4: p > 1 by INT_2:def 4;

 then

 A5: (1 mod p) = 1 by NAT_D: 14;

 p is odd by A1, PEPIN: 17;

 then (p - 1) is even by HILBERT3: 2;

 then (p -' 1) is even by A4, XREAL_1: 233;

 then 2 divides (p -' 1) by PEPIN: 22;

 then (p -' 1) = (2 * ((p -' 1) div 2)) by NAT_D: 3;



 then

 A6: ((b |^ (p -' 1)) - 1) = (((b |^ ((p -' 1) div 2)) |^ 2) - 1) by NEWTON: 9

 .= (((b |^ ((p -' 1) div 2)) ^2 ) - 1) by NEWTON: 81

 .= (((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1));

 (b,p) are_coprime by A2, INT_2:def 3;

 then ((b |^ (p -' 1)) mod p) = 1 by PEPIN: 37;

 then (((b |^ (p -' 1)) - 1) mod p) = 0 by A5, INT_4: 22;

 then

 A7: p divides (((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1)) by A6, Lm1;

 (p - 1) > (2 - 1) by A1, XREAL_1: 9;

 then (p - 1) >= (1 + 1) by INT_1: 7;

 then (p -' 1) >= 2 by A4, XREAL_1: 233;

 then ((p -' 1) div 2) >= (2 div 2) by NAT_2: 24;

 then

 A8: ((p -' 1) div 2) >= 1 by PEPIN: 44;

 per cases by A8, XXREAL_0: 1;

 suppose

 A9: ((p -' 1) div 2) = 1;

 A10:

 now

 assume p divides (b - 1);

 then p divides ( - (b - 1)) by INT_2: 10;

 then (((1 ^2 ) - b) mod p) = 0 by Lm1;

 hence contradiction by A3;

 end;

 p divides ((b + 1) * ((b |^ 1) - 1)) by A7, A9;

 then p divides (b - ( - 1)) by A10, Th7;

 then (b,( - 1)) are_congruent_mod p;

 then

 A11: (b mod p) = (( - 1) mod p) by NAT_D: 64;

 ( - p) < ( - 2) by A1, XREAL_1: 24;

 then ( - p) < (( - 2) + 1) by XREAL_1: 39;

 then (b mod p) = (p - 1) by A11, NAT_D: 63;

 hence thesis by A9;

 end;

 suppose

 A12: ((p -' 1) div 2) > 1;

 set l = ((p -' 1) div 2);

 0 is Element of INT by INT_1:def 2;

 then

 A13: ((l -' 1) |-> 0 ) is FinSequence of INT by FINSEQ_2: 63;

 set K1 = ( <*( - 1)*> ^ ((l -' 1) |-> 0 ));



 A14: ( len ((l -' 1) |-> 0 )) = (l -' 1) by CARD_1:def 7;



 A15: ( len K1) = (1 + (l -' 1)) by CARD_1:def 7

 .= l by A12, XREAL_1: 235;

 set fs = (( <*( - 1)*> ^ ((l -' 1) |-> 0 )) ^ <*1*>);

 1 is Element of INT by INT_1:def 2;

 then

 A16: <*1*> is FinSequence of INT by FINSEQ_1: 74;

 ( - 1) is Element of INT by INT_1:def 2;

 then <*( - 1)*> is FinSequence of INT by FINSEQ_1: 74;

 then ( <*( - 1)*> ^ ((l -' 1) |-> 0 )) is FinSequence of INT by A13, FINSEQ_1: 75;

 then

 reconsider fs as FinSequence of INT by A16, FINSEQ_1: 75;



 A17: ( len fs) = (1 + ((l -' 1) + 1)) by CARD_1:def 7

 .= (1 + l) by A12, XREAL_1: 235;



 A18: (fs . 1) = (( <*( - 1)*> ^ (((l -' 1) |-> 0 ) ^ <*1*>)) . 1) by FINSEQ_1: 32

 .= ( - 1) by FINSEQ_1: 41;



 A19: for x be Element of INT holds (( Poly-INT fs) . x) = ((x |^ l) - 1)

 proof

 let x be Element of INT ;

 consider fr such that

 A20: ( len fr) = ( len fs) and

 A21: for d st d in ( dom fr) holds (fr . d) = ((fs . d) * (x |^ (d -' 1))) and

 A22: (( Poly-INT fs) . x) = ( Sum fr) by Def1;

 fr = (( <*( - 1)*> ^ ((l -' 1) |-> 0 )) ^ <*(x |^ l)*>)

 proof

 set K = (( <*( - 1)*> ^ ((l -' 1) |-> 0 )) ^ <*(x |^ l)*>);



 A23: for d be Nat st d in ( dom fr) holds (fr . d) = (K . d)

 proof

 let d be Nat;

 assume

 A24: d in ( dom fr);

 then

 A25: d in ( Seg (l + 1)) by A17, A20, FINSEQ_1:def 3;

 then

 A26: d >= 1 by FINSEQ_1: 1;



 A27: d <= (l + 1) by A25, FINSEQ_1: 1;

 per cases by A26, A27, XXREAL_0: 1;

 suppose

 A28: d = 1;



 then

 A29: (fr . 1) = ((fs . 1) * (x |^ (1 -' 1))) by A21, A24

 .= ((fs . 1) * (x |^ 0 )) by XREAL_1: 232

 .= ((fs . 1) * 1) by NEWTON: 4

 .= ( - 1) by A18;

 (K . 1) = (( <*( - 1)*> ^ (((l -' 1) |-> 0 ) ^ <*(x |^ l)*>)) . 1) by FINSEQ_1: 32

 .= (fr . 1) by A29, FINSEQ_1: 41;

 hence thesis by A28;

 end;

 suppose

 A30: d > 1 & d < (l + 1);

 then

 reconsider w = (d - 1) as Element of NAT by INT_1: 3;

 (d - 1) < ((l + 1) - 1) by A30, XREAL_1: 9;

 then

 A31: w <= (l -' 1) by NAT_D: 49;



 A32: w >= ( 0 + 1) by A30, INT_1: 7, XREAL_1: 50;



 A33: (((l -' 1) |-> 0 ) . w) = 0 ;

 w in ( Seg (l -' 1)) by A31, A32, FINSEQ_1: 1;

 then

 A34: w in ( dom ((l -' 1) |-> 0 )) by A14, FINSEQ_1:def 3;

 then

 A35: w in ( dom (((l -' 1) |-> 0 ) ^ <*1*>)) by FINSEQ_2: 15;



 A36: w in ( dom (((l -' 1) |-> 0 ) ^ <*(x |^ l)*>)) by A34, FINSEQ_2: 15;



 A37: (fs . d) = (( <*( - 1)*> ^ (((l -' 1) |-> 0 ) ^ <*1*>)) . (w + 1)) by FINSEQ_1: 32

 .= ((((l -' 1) |-> 0 ) ^ <*1*>) . w) by A35, FINSEQ_3: 103

 .= 0 by A33, A34, FINSEQ_1:def 7;



 thus (K . d) = (( <*( - 1)*> ^ (((l -' 1) |-> 0 ) ^ <*(x |^ l)*>)) . (w + 1)) by FINSEQ_1: 32

 .= ((((l -' 1) |-> 0 ) ^ <*(x |^ l)*>) . w) by A36, FINSEQ_3: 103

 .= ((fs . d) * (x |^ (d -' 1))) by A33, A34, A37, FINSEQ_1:def 7

 .= (fr . d) by A21, A24;

 end;

 suppose

 A38: d = (l + 1);

 then d in ( dom fs) by A17, FINSEQ_5: 6;

 then

 A39: d in ( dom fr) by A20, FINSEQ_3: 29;

 (fs . d) = 1 by A15, A38, FINSEQ_1: 42;



 hence (fr . d) = (1 * (x |^ ((l + 1) -' 1))) by A21, A38, A39

 .= (x |^ l) by NAT_D: 34

 .= (K . d) by A15, A38, FINSEQ_1: 42;

 end;

 end;

 ( len K) = (1 + ((l -' 1) + 1)) by CARD_1:def 7

 .= ( len fr) by A12, A17, A20, XREAL_1: 235;

 hence thesis by A23, FINSEQ_3: 29;

 end;



 then ( Sum fr) = ( Sum ( <*( - 1)*> ^ (((l -' 1) |-> 0 ) ^ <*(x |^ l)*>))) by FINSEQ_1: 32

 .= (( - 1) + ( Sum (((l -' 1) |-> 0 ) ^ <*(x |^ l)*>))) by RVSUM_1: 76

 .= (( - 1) + (( Sum ((l -' 1) |-> 0 )) + (x |^ l))) by RVSUM_1: 74

 .= (( - 1) + (((l -' 1) * 0 ) + (x |^ l))) by RVSUM_1: 80;

 hence thesis by A22;

 end;

 consider fp be FinSequence of NAT such that

 A40: ( len fp) = l and

 A41: for d st d in ( dom fp) holds ((fp . d) gcd p) = 1 and

 A42: for d st d in ( dom fp) holds (fp . d) is_quadratic_residue_mod p and

 A43: for d, e st d in ( dom fp) & e in ( dom fp) & d <> e holds not ((fp . d),(fp . e)) are_congruent_mod p by A1, Th16;



 A44: (fs . (l + 1)) = 1 by A15, FINSEQ_1: 42;

 now

 assume p divides ((b |^ l) - 1);

 then

 A45: (((b |^ l) - 1) mod p) = 0 by Lm1;

 reconsider b as Element of INT by INT_1:def 2;

 set f = (fp ^ <*b*>);

 <*b*> is FinSequence of NAT by FINSEQ_1: 74;

 then

 reconsider f as FinSequence of NAT by FINSEQ_1: 75;



 A46: ( len f) = (l + 1) by A40, FINSEQ_2: 16;



 A47: for d, e st d in ( dom f) & e in ( dom f) & d <> e holds not ((f . d),(f . e)) are_congruent_mod p

 proof

 let d, e;

 assume that

 A48: d in ( dom f) and

 A49: e in ( dom f) and

 A50: d <> e;



 A51: e >= 1 by A49, FINSEQ_3: 25;



 A52: d <= (l + 1) by A46, A48, FINSEQ_3: 25;



 A53: e <= (l + 1) by A46, A49, FINSEQ_3: 25;

 per cases by A48, A52, FINSEQ_3: 25, XXREAL_0: 1;

 suppose

 A54: d >= 1 & d < (l + 1);

 then d <= l by NAT_1: 13;

 then

 A55: d in ( dom fp) by A40, A54, FINSEQ_3: 25;

 then

 A56: (f . d) = (fp . d) by FINSEQ_1:def 7;

 per cases by A49, A53, FINSEQ_3: 25, XXREAL_0: 1;

 suppose

 A57: e >= 1 & e < (l + 1);

 then e <= l by NAT_1: 13;

 then

 A58: e in ( dom fp) by A40, A57, FINSEQ_3: 25;

 then not ((fp . d),(fp . e)) are_congruent_mod p by A43, A50, A55;

 hence thesis by A56, A58, FINSEQ_1:def 7;

 end;

 suppose

 A59: e = (l + 1);

 not ((f . d),b) are_congruent_mod p

 proof

 (f . d) is_quadratic_residue_mod p by A42, A55, A56;

 then

 consider j be Integer such that

 A60: (((j ^2 ) - (f . d)) mod p) = 0 ;

 assume

 a61: ((f . d),b) are_congruent_mod p;

 p divides ((j ^2 ) - (f . d)) by A60, INT_1: 62;

 then p divides (((j ^2 ) - (f . d)) + ((f . d) - b)) by a61, WSIERP_1: 4;

 then (((j ^2 ) - b) mod p) = 0 by INT_1: 62;

 hence contradiction by A3;

 end;

 hence thesis by A40, A59, FINSEQ_1: 42;

 end;

 end;

 suppose

 A62: d = (l + 1);

 then e <= l by A50, A53, NAT_1: 8;

 then

 A63: e in ( dom fp) by A40, A51, FINSEQ_3: 25;

 then (f . e) = (fp . e) by FINSEQ_1:def 7;

 then (f . e) is_quadratic_residue_mod p by A42, A63;

 then

 consider j be Integer such that

 A64: (((j ^2 ) - (f . e)) mod p) = 0 ;



 A65: p divides ((j ^2 ) - (f . e)) by A64, INT_1: 62;

 not (b,(f . e)) are_congruent_mod p

 proof

 assume (b,(f . e)) are_congruent_mod p;

 then p divides (((j ^2 ) - (f . e)) - (b - (f . e))) by A65, Th1;

 then (((j ^2 ) - b) mod p) = 0 by INT_1: 62;

 hence contradiction by A3;

 end;

 hence thesis by A40, A62, FINSEQ_1: 42;

 end;

 end;



 A66: ((( Poly-INT fs) . b) mod p) = 0 by A19, A45;



 A67: for d st d in ( dom f) holds ((( Poly-INT fs) . (f . d)) mod p) = 0

 proof

 let d;

 assume d in ( dom f);

 then

 A68: d in ( Seg (l + 1)) by A46, FINSEQ_1:def 3;

 then

 A69: d <= (l + 1) by FINSEQ_1: 1;

 per cases by A68, A69, FINSEQ_1: 1, XXREAL_0: 1;

 suppose

 A70: d >= 1 & d < (l + 1);

 reconsider k = (fp . d) as Element of INT by INT_1:def 2;

 d <= l by A70, NAT_1: 13;

 then

 A71: d in ( dom fp) by A40, A70, FINSEQ_3: 25;

 then ((fp . d) gcd p) = 1 by A41;

 then (((fp . d) |^ l) mod p) = (1 mod p) by A1, A5, A42, A71, Th17;

 then (((k |^ l) - 1) mod p) = 0 by INT_4: 22;

 then ((( Poly-INT fs) . k) mod p) = 0 by A19;

 hence thesis by A71, FINSEQ_1:def 7;

 end;

 suppose d = (l + 1);

 hence thesis by A40, A66, FINSEQ_1: 42;

 end;

 end;

 reconsider f as FinSequence of INT by FINSEQ_2: 24, NUMBERS: 17;

 not p divides (fs . (l + 1)) by A4, A44, NAT_D: 7;

 then ( len f) <= l by A1, A17, A67, A47, Th8;

 hence contradiction by A46, XREAL_1: 29;

 end;

 then p divides ((b |^ l) + 1) by A7, Th7;

 then

 consider k be Nat such that

 A72: ((b |^ l) + 1) = (p * k) by NAT_D:def 3;

 ( - p) < ( - 1) by A4, XREAL_1: 24;

 then

 A73: (( - 1) mod p) = (( - 1) + p) by NAT_D: 63;

 ((b |^ l) mod p) = (((p * k) + ( - 1)) mod p) by A72

 .= (p - 1) by A73, NAT_D: 61;

 hence thesis;

 end;

 end;

 theorem :: INT_5:19



 Th19: p > 2 & (a gcd p) = 1 & not a is_quadratic_residue_mod p implies ((a |^ ((p -' 1) div 2)) mod p) = (p - 1)

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: not a is_quadratic_residue_mod p;

 set l = (a mod p);

 reconsider l as Element of NAT by INT_1: 3, INT_1: 57;



 A4: (l mod p) = (a mod p) by NAT_D: 65;

 then

 A5: (l,a) are_congruent_mod p by NAT_D: 64;

 then (l gcd p) = 1 by A2, WSIERP_1: 43;

 then ((l |^ ((p -' 1) div 2)) mod p) = (p - 1) by A1, A3, A5, Th11, Th18;

 hence thesis by A4, Th13;

 end;

 theorem :: INT_5:20



 Th20: p > 2 & (a gcd p) = 1 & a is_quadratic_residue_mod p implies (((a |^ ((p -' 1) div 2)) - 1) mod p) = 0

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: a is_quadratic_residue_mod p;



 A4: p > 1 by INT_2:def 4;

 ((a |^ ((p -' 1) div 2)) mod p) = 1 by A1, A2, A3, Th17;

 then ((a |^ ((p -' 1) div 2)) mod p) = (1 mod p) by A4, NAT_D: 14;

 then ((a |^ ((p -' 1) div 2)),1) are_congruent_mod p by NAT_D: 64;

 hence thesis by INT_1: 62;

 end;

 theorem :: INT_5:21



 Th21: p > 2 & (a gcd p) = 1 & not a is_quadratic_residue_mod p implies (((a |^ ((p -' 1) div 2)) + 1) mod p) = 0

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: not a is_quadratic_residue_mod p;



 A4: (p - 1) < p by XREAL_1: 146;

 ((a |^ ((p -' 1) div 2)) mod p) = (p - 1) by A1, A2, A3, Th19;

 then ((a |^ ((p -' 1) div 2)) mod p) = ((p - 1) mod p) by A4, NAT_D: 63;

 then ((a |^ ((p -' 1) div 2)),(p - 1)) are_congruent_mod p by NAT_D: 64;

 then p divides ( - (((a |^ ((p -' 1) div 2)) + 1) - p)) by INT_2: 10;

 then p divides (p - ((a |^ ((p -' 1) div 2)) + 1));

 then p divides ((a |^ ((p -' 1) div 2)) + 1) by Th2;

 hence thesis by INT_1: 62;

 end;

 reserve b for Integer;

 theorem :: INT_5:22

 a is_quadratic_residue_mod p & b is_quadratic_residue_mod p implies (a * b) is_quadratic_residue_mod p

 proof

 assume that

 A1: a is_quadratic_residue_mod p and

 A2: b is_quadratic_residue_mod p;

 consider i be Integer such that

 A3: (((i ^2 ) - a) mod p) = 0 by A1;

 consider j be Integer such that

 A4: (((j ^2 ) - b) mod p) = 0 by A2;



 A5: ((j ^2 ),b) are_congruent_mod p by A4, INT_1: 62;

 ((i ^2 ),a) are_congruent_mod p by A3, INT_1: 62;

 then (((i ^2 ) * (j ^2 )),(a * b)) are_congruent_mod p by A5, INT_1: 18;

 then ((((i * j) ^2 ) - (a * b)) mod p) = 0 by INT_1: 62;

 hence thesis;

 end;

 theorem :: INT_5:23

 p > 2 & (a gcd p) = 1 & (b gcd p) = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies not (a * b) is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: (b gcd p) = 1 and

 A4: a is_quadratic_residue_mod p and

 A5: not b is_quadratic_residue_mod p;



 A6: ((a * b) gcd p) = 1 by A2, A3, WSIERP_1: 6;

 set l = ((p -' 1) div 2);

 (((b |^ l) + 1) mod p) = 0 by A1, A3, A5, Th21;

 then

 A7: p divides ((b |^ l) + 1) by INT_1: 62;



 A8: (((a |^ l) - 1) * ((b |^ l) + 1)) = (((((a |^ l) * (b |^ l)) + ((a |^ l) * 1)) - (1 * (b |^ l))) - (1 * 1))

 .= (((((a * b) |^ l) + ((a |^ l) * 1)) - (1 * (b |^ l))) - (1 * 1)) by NEWTON: 7

 .= (((((a * b) |^ l) - 1) + ((a |^ l) - 1)) - ((b |^ l) - 1));

 (((a |^ l) - 1) mod p) = 0 by A1, A2, A4, Th20;

 then

 A9: p divides ((a |^ l) - 1) by INT_1: 62;

 then

 A10: p divides (((a |^ l) - 1) * ((b |^ l) + 1)) by INT_2: 2;

 assume (a * b) is_quadratic_residue_mod p;

 then ((((a * b) |^ l) - 1) mod p) = 0 by A1, A6, Th20;

 then p divides (((a * b) |^ l) - 1) by INT_1: 62;

 then p divides ((((a * b) |^ l) - 1) + ((a |^ l) - 1)) by A9, WSIERP_1: 4;

 then p divides ((b |^ l) - 1) by A10, A8, Th2;

 then p divides (((b |^ l) + 1) - ((b |^ l) - 1)) by A7, Th1;

 hence contradiction by A1, NAT_D: 7;

 end;

 theorem :: INT_5:24

 p > 2 & (a gcd p) = 1 & (b gcd p) = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies (a * b) is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: (b gcd p) = 1 and

 A4: not a is_quadratic_residue_mod p and

 A5: not b is_quadratic_residue_mod p;



 A6: ((a * b) gcd p) = 1 by A2, A3, WSIERP_1: 6;

 set l = ((p -' 1) div 2);

 (((b |^ l) + 1) mod p) = 0 by A1, A3, A5, Th21;

 then

 A7: p divides ((b |^ l) + 1) by INT_1: 62;



 A8: (((a |^ l) + 1) * ((b |^ l) + 1)) = (((((a |^ l) * (b |^ l)) + ((a |^ l) * 1)) + (1 * (b |^ l))) + (1 * 1))

 .= (((((a * b) |^ l) + (a |^ l)) + (b |^ l)) + 1) by NEWTON: 7

 .= (((((a * b) |^ l) + 1) + ((a |^ l) + 1)) - (1 - (b |^ l)));

 (((a |^ l) + 1) mod p) = 0 by A1, A2, A4, Th21;

 then

 A9: p divides ((a |^ l) + 1) by INT_1: 62;

 then

 A10: p divides (((a |^ l) + 1) * ((b |^ l) + 1)) by INT_2: 2;

 now

 assume not (a * b) is_quadratic_residue_mod p;

 then ((((a * b) |^ l) + 1) mod p) = 0 by A1, A6, Th21;

 then p divides (((a * b) |^ l) + 1) by INT_1: 62;

 then p divides ((((a * b) |^ l) + 1) + ((a |^ l) + 1)) by A9, WSIERP_1: 4;

 then p divides (1 - (b |^ l)) by A10, A8, Th2;

 then p divides (((b |^ l) + 1) + (1 - (b |^ l))) by A7, WSIERP_1: 4;

 hence contradiction by A1, NAT_D: 7;

 end;

 hence thesis;

 end;

 definition

 ::$Notion-Name

 let a be Integer, p be Prime;

 :: INT_5:def3

 func Lege (a,p) -> Integer equals

 : Def3: 1 if (a is_quadratic_residue_mod p & (a mod p) <> 0 ),

0 if (a is_quadratic_residue_mod p & (a mod p) = 0 )

 otherwise ( - 1);

 coherence ;

 consistency ;

 end

 theorem :: INT_5:25



 Th25: ( Lege (a,p)) = 1 or ( Lege (a,p)) = 0 or ( Lege (a,p)) = ( - 1)

 proof

 per cases ;

 suppose a is_quadratic_residue_mod p & (a mod p) <> 0 ;

 hence thesis by Def3;

 end;

 suppose a is_quadratic_residue_mod p & (a mod p) = 0 ;

 hence thesis by Def3;

 end;

 suppose not a is_quadratic_residue_mod p;

 hence thesis by Def3;

 end;

 end;

 theorem :: INT_5:26



 Th26: (a mod p) <> 0 implies ( Lege ((a ^2 ),p)) = 1

 proof

 assume (a mod p) <> 0 ;

 then not p divides a by INT_1: 62;

 then not p divides (a ^2 ) by Th7;

 then ((a ^2 ) mod p) <> 0 by INT_1: 62;

 hence thesis by Def3, Th9;

 end;

 theorem :: INT_5:27

 ( Lege (1,p)) = 1

 proof

 1 0 by NAT_D: 14;

 then ( Lege ((1 ^2 ),p)) = 1 by Th26;

 hence thesis;

 end;



 Lm3: (a gcd p) = 1 implies not p divides a

 proof

 assume

 A1: (a gcd p) = 1;

 assume p divides a;

 then p divides (p gcd a) by INT_2:def 2;

 then p = 1 by A1, WSIERP_1: 15;

 hence thesis by INT_2:def 4;

 end;

 theorem :: INT_5:28



 Th28: p > 2 & (a gcd p) = 1 implies (( Lege (a,p)),(a |^ ((p -' 1) div 2))) are_congruent_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1;

 not p divides a by Lm3, A2;

 then

 A3: (a mod p) <> 0 by INT_1: 62;



 A4: p > 1 by INT_2:def 4;

 then ( - p) < ( - 1) by XREAL_1: 24;

 then

 A5: (( - 1) mod p) = (p + ( - 1)) by NAT_D: 63;

 per cases ;

 suppose

 A6: a is_quadratic_residue_mod p;

 then ((a |^ ((p -' 1) div 2)) mod p) = 1 by A1, A2, Th17;

 then ((a |^ ((p -' 1) div 2)) mod p) = (1 mod p) by A4, NAT_D: 14;

 then ((a |^ ((p -' 1) div 2)) mod p) = (( Lege (a,p)) mod p) by A6, Def3, A3;

 hence thesis by NAT_D: 64;

 end;

 suppose

 A7: not a is_quadratic_residue_mod p;



 then ((a |^ ((p -' 1) div 2)) mod p) = (p - 1) by A1, A2, Th19

 .= (( Lege (a,p)) mod p) by A5, A7, Def3;

 hence thesis by NAT_D: 64;

 end;

 end;

 theorem :: INT_5:29

 p > 2 & (a gcd p) = 1 & (a,b) are_congruent_mod p implies ( Lege (a,p)) = ( Lege (b,p))

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: (a,b) are_congruent_mod p;

 (( Lege (a,p)),(a |^ ((p -' 1) div 2))) are_congruent_mod p by A1, A2, Th28;

 then

 A4: (( Lege (a,p)) mod p) = ((a |^ ((p -' 1) div 2)) mod p) by NAT_D: 64;

 (b gcd p) = 1 by A2, A3, WSIERP_1: 43;

 then (( Lege (b,p)),(b |^ ((p -' 1) div 2))) are_congruent_mod p by A1, Th28;

 then

 A5: (( Lege (b,p)) mod p) = ((b |^ ((p -' 1) div 2)) mod p) by NAT_D: 64;

 (a mod p) = (b mod p) by A3, NAT_D: 64;

 then (( Lege (a,p)) mod p) = (( Lege (b,p)) mod p) by A4, A5, Th13;

 then (( Lege (a,p)),( Lege (b,p))) are_congruent_mod p by NAT_D: 64;

 then

 A6: p divides (( Lege (a,p)) - ( Lege (b,p)));

 per cases by Th25;

 suppose

 A7: ( Lege (a,p)) = 1;

 A8:

 now

 assume ( Lege (b,p)) = 0 ;

 then p = 1 by A6, A7, WSIERP_1: 15;

 hence contradiction by A1;

 end;

 ( Lege (b,p)) <> ( - 1) by A7, A1, A6, NAT_D: 7;

 hence thesis by A7, A8, Th25;

 end;

 suppose

 A9: ( Lege (a,p)) = 0 ;

 A10:

 now

 assume ( Lege (b,p)) = 1;

 then p = 1 by WSIERP_1: 15, A6, A9, INT_2: 10;

 hence contradiction by A1;

 end;

 now

 assume ( Lege (b,p)) = ( - 1);

 then p = 1 by A6, A9, WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A9, Th25, A10;

 end;

 suppose

 A11: ( Lege (a,p)) = ( - 1);

 A12:

 now

 assume ( Lege (b,p)) = 1;

 then p divides ( - 2) by A6, A11;

 then p divides 2 by INT_2: 10;

 hence contradiction by A1, NAT_D: 7;

 end;

 now

 assume ( Lege (b,p)) = 0 ;

 then p = 1 by WSIERP_1: 15, A6, A11, INT_2: 10;

 hence contradiction by A1;

 end;

 hence thesis by A11, Th25, A12;

 end;

 end;

 theorem :: INT_5:30

 p > 2 & (a gcd p) = 1 & (b gcd p) = 1 implies ( Lege ((a * b),p)) = (( Lege (a,p)) * ( Lege (b,p)))

 proof

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: (b gcd p) = 1;



 A4: (( Lege (b,p)),(b |^ ((p -' 1) div 2))) are_congruent_mod p by A1, A3, Th28;

 (( Lege (a,p)),(a |^ ((p -' 1) div 2))) are_congruent_mod p by A1, A2, Th28;

 then ((( Lege (a,p)) * ( Lege (b,p))),((a |^ ((p -' 1) div 2)) * (b |^ ((p -' 1) div 2)))) are_congruent_mod p by A4, INT_1: 18;

 then ((( Lege (a,p)) * ( Lege (b,p))),((a * b) |^ ((p -' 1) div 2))) are_congruent_mod p by NEWTON: 7;

 then

 A5: (((a * b) |^ ((p -' 1) div 2)),(( Lege (a,p)) * ( Lege (b,p)))) are_congruent_mod p by INT_1: 14;

 ((a * b) gcd p) = 1 by A2, A3, WSIERP_1: 6;

 then (( Lege ((a * b),p)),((a * b) |^ ((p -' 1) div 2))) are_congruent_mod p by A1, Th28;

 then (( Lege ((a * b),p)),(( Lege (a,p)) * ( Lege (b,p)))) are_congruent_mod p by A5, INT_1: 15;

 then

 A6: p divides (( Lege ((a * b),p)) - (( Lege (a,p)) * ( Lege (b,p))));



 A7: ( Lege (b,p)) = 1 or ( Lege (b,p)) = ( - 1) or ( Lege (b,p)) = 0 by Th25;



 A8: ( Lege (a,p)) = 1 or ( Lege (a,p)) = ( - 1) or ( Lege (a,p)) = 0 by Th25;

 per cases by Th25;

 suppose

 A9: ( Lege ((a * b),p)) = 1;

 now

 assume ( Lege (a,p)) = 0 or ( Lege (b,p)) = 0 ;

 then p = 1 by A6, A9, WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A8, A7, A1, A6, A9, NAT_D: 7;

 end;

 suppose

 A10: ( Lege ((a * b),p)) = 0 ;

 A11:

 now

 assume (( Lege (a,p)) * ( Lege (b,p))) = ( - 1);

 then p <= 1 by A6, A10, NAT_D: 7;

 then p < (1 + 1) by NAT_1: 13;

 hence contradiction by A1;

 end;

 now

 assume (( Lege (a,p)) * ( Lege (b,p))) = 1;

 then p divides 1 by A6, A10, INT_2: 10;

 then p <= 1 by NAT_D: 7;

 then p < (1 + 1) by NAT_1: 13;

 hence contradiction by A1;

 end;

 hence thesis by A8, A7, A11, A10;

 end;

 suppose

 A12: ( Lege ((a * b),p)) = ( - 1);

 A13:

 now

 assume ( Lege (a,p)) = 0 or ( Lege (b,p)) = 0 ;

 then p = 1 or p = ( - 1) by A6, A12, INT_2: 13;

 hence contradiction by INT_2:def 4;

 end;

 now

 assume (( Lege (a,p)) * ( Lege (b,p))) = 1;

 then p divides ( - 2) by A6, A12;

 then p divides 2 by INT_2: 10;

 hence contradiction by A1, NAT_D: 7;

 end;

 hence thesis by A12, A13, A7, A8;

 end;

 end;

 theorem :: INT_5:31



 Th31: (for d st d in ( dom fr) holds (fr . d) = 1 or (fr . d) = 0 or (fr . d) = ( - 1)) implies ( Product fr) = 1 or ( Product fr) = 0 or ( Product fr) = ( - 1)

 proof

 defpred P[ FinSequence of INT ] means (for d st d in ( dom $1) holds ($1 . d) = 1 or ($1 . d) = 0 or ($1 . d) = ( - 1)) implies ( Product $1) = 1 or ( Product $1) = 0 or ( Product $1) = ( - 1);



 A1: for p be FinSequence of INT , n be Element of INT st P[p] holds P[(p ^ <*n*>)]

 proof

 let p be FinSequence of INT , i be Element of INT ;

 set p1 = (p ^ <*i*>);

 assume

 A2: P[p];

 P[p1]

 proof

 assume

 A3: for d st d in ( dom p1) holds (p1 . d) = 1 or (p1 . d) = 0 or (p1 . d) = ( - 1);



 A4: for d st d in ( dom p) holds (p . d) = 1 or (p . d) = 0 or (p . d) = ( - 1)

 proof

 let d;

 assume

 A5: d in ( dom p);

 then (p1 . d) = 1 or (p1 . d) = 0 or (p1 . d) = ( - 1) by A3, FINSEQ_2: 15;

 hence thesis by A5, FINSEQ_1:def 7;

 end;



 A6: ( len p1) in ( dom p1) by FINSEQ_5: 6;



 A7: ( Product p1) = (( Product p) * i) by RVSUM_1: 96;

 ( len p1) = (( len p) + 1) by FINSEQ_2: 16;

 then

 A8: (p1 . (( len p) + 1)) = 1 or (p1 . (( len p) + 1)) = 0 or (p1 . (( len p) + 1)) = ( - 1) by A3, A6;

 per cases by A2, A4, A8, FINSEQ_1: 42;

 suppose ( Product p) = 1 & i = 1;

 hence thesis by A7;

 end;

 suppose ( Product p) = 1 & i = 0 ;

 hence thesis by A7;

 end;

 suppose ( Product p) = 1 & i = ( - 1);

 hence thesis by A7;

 end;

 suppose ( Product p) = ( - 1) & i = 1;

 hence thesis by A7;

 end;

 suppose ( Product p) = ( - 1) & i = 0 ;

 hence thesis by A7;

 end;

 suppose ( Product p) = ( - 1) & i = ( - 1);

 hence thesis by A7;

 end;

 suppose ( Product p) = 0 & i = 1;

 hence thesis by A7;

 end;

 suppose ( Product p) = 0 & i = 0 ;

 hence thesis by A7;

 end;

 suppose ( Product p) = 0 & i = ( - 1);

 hence thesis by A7;

 end;

 end;

 hence thesis;

 end;



 A9: P[( <*> INT )] by RVSUM_1: 94;

 for p be FinSequence of INT holds P[p] from FINSEQ_2:sch 2( A9, A1);

 hence thesis;

 end;

 reserve m for Integer;

 theorem :: INT_5:32



 Th32: for f, fr st ( len f) = ( len fr) & (for d st d in ( dom f) holds ((f . d),(fr . d)) are_congruent_mod m) holds (( Product f),( Product fr)) are_congruent_mod m

 proof

 defpred P[ Nat] means for f, fr st ( len f) = $1 & ( len f) = ( len fr) & (for d st d in ( dom f) holds ((f . d),(fr . d)) are_congruent_mod m) holds (( Product f),( Product fr)) are_congruent_mod m;



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 P[(n + 1)]

 proof

 let f, fr;

 assume that

 A3: ( len f) = (n + 1) and

 A4: ( len f) = ( len fr) and

 A5: for d st d in ( dom f) holds ((f . d),(fr . d)) are_congruent_mod m;

 consider fr1 be FinSequence of INT , b be Element of INT such that

 A6: fr = (fr1 ^ <*b*>) by A3, A4, FINSEQ_2: 19;

 f <> {} by A3;

 then

 A7: (n + 1) in ( dom f) by A3, FINSEQ_5: 6;

 consider f1 be FinSequence of INT , a be Element of INT such that

 A8: f = (f1 ^ <*a*>) by A3, FINSEQ_2: 19;



 A9: (n + 1) = (( len fr1) + 1) by A3, A4, A6, FINSEQ_2: 16;

 then

 A10: (fr . (n + 1)) = b by A6, FINSEQ_1: 42;



 A11: (n + 1) = (( len f1) + 1) by A3, A8, FINSEQ_2: 16;

 then

 A12: ( dom f1) = ( dom fr1) by A9, FINSEQ_3: 29;

 for d st d in ( dom f1) holds ((f1 . d),(fr1 . d)) are_congruent_mod m

 proof

 let d;

 assume

 A13: d in ( dom f1);

 then

 A14: (f . d) = (f1 . d) by A8, FINSEQ_1:def 7;

 (fr . d) = (fr1 . d) by A6, A12, A13, FINSEQ_1:def 7;

 hence thesis by A5, A8, A13, A14, FINSEQ_2: 15;

 end;

 then

 A15: (( Product f1),( Product fr1)) are_congruent_mod m by A2, A11, A9;

 (f . (n + 1)) = a by A8, A11, FINSEQ_1: 42;

 then (a,b) are_congruent_mod m by A5, A7, A10;

 then ((( Product f1) * a),(( Product fr1) * b)) are_congruent_mod m by A15, INT_1: 18;

 then (( Product f),(( Product fr1) * b)) are_congruent_mod m by A8, RVSUM_1: 96;

 hence thesis by A6, RVSUM_1: 96;

 end;

 hence thesis;

 end;



 A16: P[ 0 ]

 proof

 let f, fr;

 assume that

 A17: ( len f) = 0 and

 A18: ( len f) = ( len fr);



 A19: f = ( <*> INT ) by A17;

 fr = ( <*> INT ) by A17, A18;

 hence thesis by A19, INT_1: 11;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A16, A1);

 hence thesis;

 end;

 theorem :: INT_5:33



 Th33: for f, fr st ( len f) = ( len fr) & (for d st d in ( dom f) holds ((f . d),( - (fr . d))) are_congruent_mod m) holds (( Product f),((( - 1) |^ ( len f)) * ( Product fr))) are_congruent_mod m

 proof

 defpred P[ Nat] means for f, fr st ( len f) = $1 & ( len f) = ( len fr) & (for d st d in ( dom f) holds ((f . d),( - (fr . d))) are_congruent_mod m) holds (( Product f),((( - 1) |^ ( len f)) * ( Product fr))) are_congruent_mod m;



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 P[(n + 1)]

 proof

 let f, fr;

 assume that

 A3: ( len f) = (n + 1) and

 A4: ( len f) = ( len fr) and

 A5: for d st d in ( dom f) holds ((f . d),( - (fr . d))) are_congruent_mod m;

 consider fr1 be FinSequence of INT , b be Element of INT such that

 A6: fr = (fr1 ^ <*b*>) by A3, A4, FINSEQ_2: 19;

 f <> {} by A3;

 then

 A7: (n + 1) in ( dom f) by A3, FINSEQ_5: 6;

 consider f1 be FinSequence of INT , a be Element of INT such that

 A8: f = (f1 ^ <*a*>) by A3, FINSEQ_2: 19;



 A9: (n + 1) = (( len fr1) + 1) by A3, A4, A6, FINSEQ_2: 16;

 then

 A10: (fr . (n + 1)) = b by A6, FINSEQ_1: 42;



 A11: (n + 1) = (( len f1) + 1) by A3, A8, FINSEQ_2: 16;

 then

 A12: ( dom f1) = ( dom fr1) by A9, FINSEQ_3: 29;

 for d st d in ( dom f1) holds ((f1 . d),( - (fr1 . d))) are_congruent_mod m

 proof

 let d;

 assume

 A13: d in ( dom f1);

 then

 A14: (f . d) = (f1 . d) by A8, FINSEQ_1:def 7;

 (fr . d) = (fr1 . d) by A6, A12, A13, FINSEQ_1:def 7;

 hence thesis by A5, A8, A13, A14, FINSEQ_2: 15;

 end;

 then

 A15: (( Product f1),((( - 1) |^ ( len f1)) * ( Product fr1))) are_congruent_mod m by A2, A11, A9;

 (f . (n + 1)) = a by A8, A11, FINSEQ_1: 42;

 then (a,( - b)) are_congruent_mod m by A5, A7, A10;

 then ((( Product f1) * a),(((( - 1) |^ ( len f1)) * ( Product fr1)) * ( - b))) are_congruent_mod m by A15, INT_1: 18;

 then (( Product f),(((( - 1) |^ ( len f1)) * ( - 1)) * (( Product fr1) * b))) are_congruent_mod m by A8, RVSUM_1: 96;

 then (( Product f),((( - 1) |^ (( len f1) + 1)) * (( Product fr1) * b))) are_congruent_mod m by NEWTON: 6;

 hence thesis by A3, A6, A11, RVSUM_1: 96;

 end;

 hence thesis;

 end;



 A16: P[ 0 ]

 proof

 let f, fr;

 assume that

 A17: ( len f) = 0 and

 A18: ( len f) = ( len fr);



 A19: f = ( <*> INT ) by A17;



 A20: (( - 1) |^ ( len f)) = 1 by A17, NEWTON: 4;

 fr = ( <*> INT ) by A17, A18;

 hence thesis by A19, A20, INT_1: 11;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A16, A1);

 hence thesis;

 end;

 reserve fp for FinSequence of NAT ;

 theorem :: INT_5:34



 Th34: p > 2 & (for d st d in ( dom fp) holds ((fp . d) gcd p) = 1) implies ex fr be FinSequence of INT st ( len fr) = ( len fp) & (for d st d in ( dom fr) holds (fr . d) = ( Lege ((fp . d),p))) & ( Lege (( Product fp),p)) = ( Product fr)

 proof

 assume

 A1: p > 2;

 deffunc F( Nat) = ( Lege ((fp . $1),p));

 set k = ((p -' 1) div 2);

 assume

 A2: for d st d in ( dom fp) holds ((fp . d) gcd p) = 1;

 set f = (fp |^ k);

 reconsider f as FinSequence of INT by FINSEQ_2: 24, NUMBERS: 17;

 consider fr be FinSequence such that

 A3: ( len fr) = ( len fp) & for d be Nat st d in ( dom fr) holds (fr . d) = F(d) from FINSEQ_1:sch 2;

 for d be Nat st d in ( dom fr) holds (fr . d) in INT

 proof

 let d be Nat;

 assume d in ( dom fr);

 then (fr . d) = ( Lege ((fp . d),p)) by A3;

 hence thesis by INT_1:def 2;

 end;

 then

 reconsider fr as FinSequence of INT by FINSEQ_2: 12;



 A4: fp is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A5: ( len f) = ( len fp) by NAT_3:def 1;

 for d st d in ( dom fr) holds ((fr . d),(f . d)) are_congruent_mod p

 proof

 let d;

 assume

 A6: d in ( dom fr);

 then d in ( dom fp) by A3, FINSEQ_3: 29;

 then ((fp . d) gcd p) = 1 by A2;

 then (( Lege ((fp . d),p)),((fp . d) |^ k)) are_congruent_mod p by A1, Th28;

 then

 A7: ((fr . d),((fp . d) |^ k)) are_congruent_mod p by A3, A6;

 d in ( dom f) by A3, A5, A6, FINSEQ_3: 29;

 hence thesis by A7, NAT_3:def 1;

 end;

 then

 A8: (( Product f),( Product fr)) are_congruent_mod p by A3, A5, Th32, INT_1: 14;

 (( Product fp) gcd p) = 1 by A2, WSIERP_1: 36;

 then (( Lege (( Product fp),p)),(( Product fp) |^ ((p -' 1) div 2))) are_congruent_mod p by A1, Th28;

 then (( Lege (( Product fp),p)),( Product f)) are_congruent_mod p by A4, NAT_3: 15;

 then (( Lege (( Product fp),p)),( Product fr)) are_congruent_mod p by A8, INT_1: 15;

 then

 A9: p divides (( Lege (( Product fp),p)) - ( Product fr));

 take fr;



 A10: for d st d in ( dom fr) holds (fr . d) = 1 or (fr . d) = 0 or (fr . d) = ( - 1)

 proof

 let d;

 assume d in ( dom fr);

 then (fr . d) = ( Lege ((fp . d),p)) by A3;

 hence thesis by Th25;

 end;

 per cases by Th25;

 suppose

 A11: ( Lege (( Product fp),p)) = 1;

 then

 A12: ( Product fr) <> ( - 1) by A1, A9, NAT_D: 7;

 now

 assume ( Product fr) = 0 ;

 then p = 1 by A9, A11, WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A3, A10, A11, Th31, A12;

 end;

 suppose

 A13: ( Lege (( Product fp),p)) = 0 ;

 A14:

 now

 assume ( Product fr) = ( - 1);

 then p = 1 by A9, A13, WSIERP_1: 15;

 hence contradiction by A1;

 end;

 now

 assume ( Product fr) = 1;

 then p divides 1 by A9, A13, INT_2: 10;

 then p = 1 by WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A3, A10, A13, Th31, A14;

 end;

 suppose

 A15: ( Lege (( Product fp),p)) = ( - 1);

 A16:

 now

 assume ( Product fr) = 1;

 then p divides ( - 2) by A9, A15;

 then p divides 2 by INT_2: 10;

 hence contradiction by A1, NAT_D: 7;

 end;

 now

 assume ( Product fr) = 0 ;

 then p divides 1 by A9, A15, INT_2: 10;

 then p = 1 by WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A3, A10, A15, Th31, A16;

 end;

 end;

 theorem :: INT_5:35

 p > 2 & (d gcd p) = 1 & (e gcd p) = 1 implies ( Lege (((d ^2 ) * e),p)) = ( Lege (e,p))

 proof

 assume that

 A1: p > 2 and

 A2: (d gcd p) = 1 and

 A3: (e gcd p) = 1;

 reconsider d2 = (d ^2 ), e as Element of NAT by ORDINAL1:def 12;

 set fp = <*d2, e*>;

 reconsider fp as FinSequence of NAT by FINSEQ_2: 13;

 not p divides d by A2, Lm3;

 then (d mod p) <> 0 by INT_1: 62;

 then

 A4: ( Lege ((d ^2 ),p)) = 1 by Th26;

 reconsider p as prime Element of NAT by ORDINAL1:def 12;

 for k st k in ( dom fp) holds ((fp . k) gcd p) = 1

 proof

 let k;

 assume k in ( dom fp);

 then k in ( Seg ( len fp)) by FINSEQ_1:def 3;

 then

 A5: k in ( Seg 2) by FINSEQ_1: 44;

 per cases by A5, FINSEQ_1: 2, TARSKI:def 2;

 suppose k = 1;

 then (fp . k) = (d ^2 ) by FINSEQ_1: 44;

 hence thesis by A2, WSIERP_1: 7;

 end;

 suppose k = 2;

 hence thesis by A3, FINSEQ_1: 44;

 end;

 end;

 then

 consider fr be FinSequence of INT such that

 A6: ( len fr) = ( len fp) and

 A7: for k be Nat st k in ( dom fr) holds (fr . k) = ( Lege ((fp . k),p)) and

 A8: ( Lege (( Product fp),p)) = ( Product fr) by A1, Th34;



 A9: ( len fr) = 2 by A6, FINSEQ_1: 44;

 then 2 in ( dom fr) by FINSEQ_3: 25;

 then (fr . 2) = ( Lege ((fp . 2),p)) by A7;

 then

 A10: (fr . 2) = ( Lege (e,p)) by FINSEQ_1: 44;

 (fr . 1) = ( Lege ((fp . 1),p)) by A7, A9, FINSEQ_3: 25;

 then (fr . 1) = ( Lege ((d ^2 ),p)) by FINSEQ_1: 44;

 then fr = <*1, ( Lege (e,p))*> by A4, A9, A10, FINSEQ_1: 44;

 then ( Product fr) = (1 * ( Lege (e,p))) by RVSUM_1: 99;

 hence thesis by A8, RVSUM_1: 99;

 end;

 theorem :: INT_5:36



 Th36: p > 2 implies ( Lege (( - 1),p)) = (( - 1) |^ ((p -' 1) div 2))

 proof

 assume

 A1: p > 2;

 |.(( - 1) |^ ((p -' 1) div 2)).| = 1 by SERIES_2: 1;

 then

 A2: (( - 1) |^ ((p -' 1) div 2)) = 1 or ( - (( - 1) |^ ((p -' 1) div 2))) = 1 by ABSVALUE: 1;

 (( - 1) gcd p) = ( |.(( - 1) |^ 1).| gcd |.p.|) by INT_2: 34

 .= (1 gcd |.p.|) by SERIES_2: 1

 .= 1 by NEWTON: 51;

 then

 A3: (( Lege (( - 1),p)),(( - 1) |^ ((p -' 1) div 2))) are_congruent_mod p by A1, Th28;

 per cases by A2;

 suppose

 A4: (( - 1) |^ ((p -' 1) div 2)) = 1;

 then

 A5: p divides (( Lege (( - 1),p)) - 1) by A3;

 A6:

 now

 assume ( Lege (( - 1),p)) = ( - 1);

 then p divides ( - 2) by A5;

 then p divides 2 by INT_2: 10;

 hence contradiction by A1, NAT_D: 7;

 end;

 now

 assume ( Lege (( - 1),p)) = 0 ;

 then p divides 1 by A5, INT_2: 10;

 then p <= 1 by NAT_D: 7;

 then p < (1 + 1) by NAT_1: 13;

 hence contradiction by A1;

 end;

 hence thesis by A4, Th25, A6;

 end;

 suppose

 A7: (( - 1) |^ ((p -' 1) div 2)) = ( - 1);

 then

 A8: p divides (( Lege (( - 1),p)) - ( - 1)) by A3;

 then

 A9: ( Lege (( - 1),p)) <> 1 by A1, NAT_D: 7;

 now

 assume ( Lege (( - 1),p)) = 0 ;

 then p <= 1 by A8, NAT_D: 7;

 then p < (1 + 1) by NAT_1: 13;

 hence contradiction by A1;

 end;

 hence thesis by A7, Th25, A9;

 end;

 end;

 theorem :: INT_5:37

 p > 2 & (p mod 4) = 1 implies ( - 1) is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (p mod 4) = 1;

 p > 1 by INT_2:def 4;

 then

 A3: (p -' 1) = (p - 1) by XREAL_1: 233;

 p = (((p div 4) * 4) + 1) by A2, NAT_D: 2;

 then (p -' 1) = (2 * (2 * (p div 4))) by A3;



 then (( - 1) |^ ((p -' 1) div 2)) = (( - 1) |^ (2 * (p div 4))) by NAT_D: 18

 .= ((( - 1) |^ 2) |^ (p div 4)) by NEWTON: 9

 .= ((1 |^ 2) |^ (p div 4)) by WSIERP_1: 1

 .= 1;

 then ( Lege (( - 1),p)) = 1 by A1, Th36;

 hence thesis by Def3;

 end;

 theorem :: INT_5:38

 p > 2 & (p mod 4) = 3 implies not ( - 1) is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (p mod 4) = 3;

 p > 1 by INT_2:def 4;

 then

 A3: (p -' 1) = (p - 1) by XREAL_1: 233;

 p = (((p div 4) * 4) + 3) by A2, NAT_D: 2;

 then (p -' 1) = (2 * ((2 * (p div 4)) + 1)) by A3;



 then (( - 1) |^ ((p -' 1) div 2)) = (( - 1) |^ ((2 * (p div 4)) + 1)) by NAT_D: 18

 .= ((( - 1) |^ (2 * (p div 4))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ (p div 4)) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ (p div 4)) * ( - 1)) by WSIERP_1: 1

 .= (1 * ( - 1));

 then ( Lege (( - 1),p)) = ( - 1) by A1, Th36;

 then not (( - 1) is_quadratic_residue_mod p & (( - 1) mod p) <> 0 ) & not (( - 1) is_quadratic_residue_mod p & (( - 1) mod p) = 0 ) by Def3;

 hence thesis;

 end;

 begin

 theorem :: INT_5:39



 Th39: for D be non empty set, f be FinSequence of D, i,j be Nat holds f is one-to-one iff ( Swap (f,i,j)) is one-to-one

 proof

 let D be non empty set, f be FinSequence of D, i,j be Nat;

 thus f is one-to-one implies ( Swap (f,i,j)) is one-to-one

 proof

 set ff = ( Swap (f,i,j));



 A1: ( rng ff) = ( rng f) by FINSEQ_7: 22;

 assume f is one-to-one;

 then

 A2: ( card ( rng f)) = ( len f) by FINSEQ_4: 62;

 ( len ff) = ( len f) by FINSEQ_7: 18;

 hence thesis by A2, A1, FINSEQ_4: 62;

 end;

 assume ( Swap (f,i,j)) is one-to-one;

 then ( card ( rng ( Swap (f,i,j)))) = ( len ( Swap (f,i,j))) by FINSEQ_4: 62;

 then ( card ( rng f)) = ( len ( Swap (f,i,j))) by FINSEQ_7: 22;

 then ( card ( rng f)) = ( len f) by FINSEQ_7: 18;

 hence thesis by FINSEQ_4: 62;

 end;

 theorem :: INT_5:40



 Th40: for f be FinSequence of NAT st ( len f) = n & (for d st d in ( dom f) holds (f . d) > 0 & (f . d) <= n) & f is one-to-one holds ( rng f) = ( Seg n)

 proof

 defpred P[ Nat] means for f be FinSequence of NAT st ( len f) = $1 & (for d st d in ( dom f) holds (f . d) > 0 & (f . d) <= $1) & f is one-to-one holds ( rng f) = ( Seg $1);



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 P[(n + 1)]

 proof

 let f be FinSequence of NAT ;

 assume that

 A3: ( len f) = (n + 1) and

 A4: for d st d in ( dom f) holds (f . d) > 0 & (f . d) <= (n + 1) and

 A5: f is one-to-one;



 A6: f <> {} by A3;

 then

 A7: (n + 1) in ( dom f) by A3, FINSEQ_5: 6;

 then

 A8: (f . (n + 1)) > 0 by A4;

 consider f1 be FinSequence of NAT , a be Element of NAT such that

 A9: f = (f1 ^ <*a*>) by A6, HILBERT2: 4;



 A10: f1 is one-to-one by A5, A9, FINSEQ_3: 91;



 A11: ( len f) = (( len f1) + 1) by A9, FINSEQ_2: 16;

 (f . (n + 1)) <= (n + 1) by A4, A7;

 then

 A12: a <= (n + 1) by A3, A9, A11, FINSEQ_1: 42;

 per cases by A3, A9, A11, A8, A12, FINSEQ_1: 42, XXREAL_0: 1;

 suppose

 A13: a = (n + 1);

 for d st d in ( dom f1) holds (f1 . d) > 0 & (f1 . d) <= n

 proof

 let d;

 assume

 A14: d in ( dom f1);

 then

 A15: d in ( dom f) by A9, FINSEQ_2: 15;

 A16:

 now

 d <= n by A3, A11, A14, FINSEQ_3: 25;

 then d < (n + 1) by XREAL_1: 145;

 then (f . d) <> (f . (n + 1)) by A5, A7, A15;

 then

 A17: (f1 . d) <> (f . (n + 1)) by A9, A14, FINSEQ_1:def 7;

 assume (f1 . d) = (n + 1);

 hence contradiction by A3, A9, A11, A13, A17, FINSEQ_1: 42;

 end;

 (f . d) <= (n + 1) by A4, A15;

 then (f1 . d) <= (n + 1) by A9, A14, FINSEQ_1:def 7;

 then

 A18: (f1 . d) < (n + 1) by A16, XXREAL_0: 1;

 (f . d) > 0 by A4, A15;

 hence thesis by A9, A14, A18, FINSEQ_1:def 7, NAT_1: 13;

 end;

 then ( rng f1) = ( Seg n) by A2, A3, A11, A10;

 then (( rng f1) \/ {a}) = ( Seg (n + 1)) by A13, FINSEQ_1: 9;

 then (( rng f1) \/ ( rng <*a*>)) = ( Seg (n + 1)) by FINSEQ_1: 38;

 hence thesis by A9, FINSEQ_1: 31;

 end;

 suppose

 A19: a > 0 & a < (n + 1);

 ex d st d in ( dom f1) & (f1 . d) = (n + 1)

 proof

 assume

 A20: for d st d in ( dom f1) holds (f1 . d) <> (n + 1);

 for d be Nat st d in ( dom f) holds (f . d) in ( Seg n)

 proof

 let d be Nat;

 assume

 A21: d in ( dom f);

 then

 A22: d in ( Seg (n + 1)) by A3, FINSEQ_1:def 3;

 then

 A23: d <= (n + 1) by FINSEQ_1: 1;

 per cases by A22, A23, FINSEQ_1: 1, XXREAL_0: 1;

 suppose d = (n + 1);

 then

 A24: (f . d) = a by A3, A9, A11, FINSEQ_1: 42;

 then

 A25: (f . d) <= n by A19, NAT_1: 13;

 (f . d) >= ( 0 + 1) by A19, A24, NAT_1: 13;

 hence thesis by A25, FINSEQ_1: 1;

 end;

 suppose

 A26: d >= 1 & d < (n + 1);

 then d <= n by NAT_1: 13;

 then d in ( Seg n) by A26, FINSEQ_1: 1;

 then

 A27: d in ( dom f1) by A3, A11, FINSEQ_1:def 3;

 then (f1 . d) <> (n + 1) by A20;

 then

 A28: (f . d) <> (n + 1) by A9, A27, FINSEQ_1:def 7;

 (f . d) <= (n + 1) by A4, A21;

 then (f . d) < (n + 1) by A28, XXREAL_0: 1;

 then

 A29: (f . d) <= n by NAT_1: 13;

 (f . d) > 0 by A4, A21;

 then (f . d) >= ( 0 + 1) by NAT_1: 13;

 hence thesis by A29, FINSEQ_1: 1;

 end;

 end;

 then f is FinSequence of ( Seg n) by FINSEQ_2: 12;

 then ( rng f) c= ( Seg n) by FINSEQ_1:def 4;

 then ( card ( rng f)) <= ( card ( Seg n)) by NAT_1: 43;

 then (n + 1) <= ( card ( Seg n)) by A3, A5, FINSEQ_4: 62;

 then (n + 1) <= (n + 0 ) by FINSEQ_1: 57;

 hence contradiction by XREAL_1: 6;

 end;

 then

 consider d1 be Element of NAT such that

 A30: d1 in ( dom f1) and

 A31: (f1 . d1) = (n + 1);

 d1 <= n by A3, A11, A30, FINSEQ_3: 25;

 then

 A32: d1 <= ( len f) by A3, NAT_1: 13;



 A33: ( 0 + 1) <= (n + 1) by XREAL_1: 6;

 set f2 = ( Swap (f,d1,(n + 1)));



 A34: ( len f2) = (n + 1) by A3, FINSEQ_7: 18;

 then

 A35: f2 <> {} ;

 then

 consider f3 be FinSequence of NAT , b be Element of NAT such that

 A36: f2 = (f3 ^ <*b*>) by HILBERT2: 4;



 A37: (n + 1) = (( len f3) + 1) by A34, A36, FINSEQ_2: 16;



 A38: 1 <= d1 by A30, FINSEQ_3: 25;

 then (f2 /. (n + 1)) = (f /. d1) by A3, A32, A33, FINSEQ_7: 31;

 then (f2 /. (n + 1)) = (f . d1) by A38, A32, FINSEQ_4: 15;

 then (f2 . (n + 1)) = (f . d1) by A34, A33, FINSEQ_4: 15;

 then

 A39: (f2 . (n + 1)) = (n + 1) by A9, A30, A31, FINSEQ_1:def 7;

 then

 A40: b = (n + 1) by A36, A37, FINSEQ_1: 42;



 A41: f2 is one-to-one by A5, Th39;



 A42: for d st d in ( dom f3) holds (f3 . d) > 0 & (f3 . d) <= n

 proof

 let d;

 assume

 A43: d in ( dom f3);

 then

 A44: d in ( dom f2) by A36, FINSEQ_2: 15;

 A45:

 now

 d <= n by A37, A43, FINSEQ_3: 25;

 then

 A46: d < (n + 1) by XREAL_1: 145;

 assume (f3 . d) = (n + 1);

 then

 A47: (f2 . d) = (n + 1) by A36, A43, FINSEQ_1:def 7;

 (n + 1) in ( dom f2) by A34, A35, FINSEQ_5: 6;

 hence contradiction by A39, A41, A44, A47, A46;

 end;

 (f2 . d) in ( rng f2) by A44, FUNCT_1: 3;

 then (f2 . d) in ( rng f) by FINSEQ_7: 22;

 then

 A48: ex e be Nat st e in ( dom f) & (f2 . d) = (f . e) by FINSEQ_2: 10;

 then (f2 . d) <= (n + 1) by A4;

 then (f3 . d) <= (n + 1) by A36, A43, FINSEQ_1:def 7;

 then

 A49: (f3 . d) < (n + 1) by A45, XXREAL_0: 1;

 (f2 . d) > 0 by A4, A48;

 hence thesis by A36, A43, A49, FINSEQ_1:def 7, NAT_1: 13;

 end;

 f3 is one-to-one by A36, A41, FINSEQ_3: 91;

 then

 A50: ( rng f3) = ( Seg n) by A2, A37, A42;

 ( rng f2) = (( rng f3) \/ ( rng <*b*>)) by A36, FINSEQ_1: 31

 .= (( Seg n) \/ {(n + 1)}) by A40, A50, FINSEQ_1: 38

 .= ( Seg (n + 1)) by FINSEQ_1: 9;

 hence thesis by FINSEQ_7: 22;

 end;

 end;

 hence thesis;

 end;



 A51: P[ 0 ]

 proof

 let f be FinSequence of NAT ;

 assume ( len f) = 0 ;

 then f = {} ;

 hence thesis;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A51, A1);

 hence thesis;

 end;

 reserve a,m for Nat;

 theorem :: INT_5:41



 Th41: for f be FinSequence of NAT st p > 2 & (a gcd p) = 1 & f = (a * ( idseq ((p -' 1) div 2))) & m = ( card { k where k be Element of NAT : k in ( rng (f mod p)) & k > (p / 2) }) holds ( Lege (a,p)) = (( - 1) |^ m)

 proof

 let f be FinSequence of NAT ;

 assume that

 A1: p > 2 and

 A2: (a gcd p) = 1 and

 A3: f = (a * ( idseq ((p -' 1) div 2))) and

 A4: m = ( card { k where k be Element of NAT : k in ( rng (f mod p)) & k > (p / 2) });

 set f1 = (f mod p);



 A5: ( len f1) = ( len f) by EULER_2:def 1;

 set X = { k where k be Element of NAT : k in ( rng f1) & k > (p / 2) };

 for x be object st x in X holds x in ( rng f1)

 proof

 let x be object;

 assume x in X;

 then ex k be Element of NAT st x = k & k in ( rng f1) & k > (p / 2);

 hence thesis;

 end;

 then

 A6: X c= ( rng f1);

 then

 reconsider X as finite set;

 reconsider X as finite Subset of NAT by A6, XBOOLE_1: 1;

 ( card X) is Element of NAT ;

 then

 reconsider m as Element of NAT by A4;



 A7: (( rng f1) \ X) c= ( rng f1) by XBOOLE_1: 36;

 reconsider Y = (( rng f1) \ X) as finite Subset of NAT ;



 A8: ((a |^ ((p -' 1) div 2)),( Lege (a,p))) are_congruent_mod p by A1, A2, Th28, INT_1: 14;

 set f2 = ( Sgm ( rng f1));

 (( Product f1) mod p) = (( Product f) mod p) by EULER_2: 11;

 then

 A9: (( Product f1),( Product f)) are_congruent_mod p by NAT_D: 64;



 A10: p > 1 by INT_2:def 4;

 then

 A11: (p -' 1) = (p - 1) by XREAL_1: 233;

 then

 A12: (p -' 1) > 0 by A10, XREAL_1: 50;

 set p9 = ((p -' 1) div 2);

 ( rng ( idseq p9)) = ( Seg p9);

 then

 reconsider I = ( idseq p9) as FinSequence of NAT by FINSEQ_1:def 4;

 ( dom f) = ( dom I) by A3, VALUED_1:def 5;



 then

 A13: ( len f) = ( len I) by FINSEQ_3: 29

 .= p9 by CARD_1:def 7;

 p >= (2 + 1) by A1, NAT_1: 13;

 then (p - 1) >= (3 - 1) by XREAL_1: 9;

 then f1 <> {} by A13, A11, A5, NAT_2: 13;

 then ( rng f1) is non empty Subset of NAT ;

 then

 consider n1 be Element of NAT such that

 A14: ( rng f1) c= (( Seg n1) \/ { 0 }) by HEYTING3: 1;

 I is Element of (p9 -tuples_on REAL ) by FINSEQ_2: 109, NUMBERS: 19;



 then

 A15: ( Product f) = (( Product (p9 |-> a)) * ( Product I)) by A3, RVSUM_1: 108

 .= ((a |^ p9) * ( Product I)) by NEWTON:def 1;

 p is odd by A1, PEPIN: 17;

 then

 A16: (p -' 1) is even by A11, HILBERT3: 2;



 then

 A17: p9 = (((p -' 1) + 1) div 2) by NAT_2: 26

 .= (p div 2) by A10, XREAL_1: 235;

 2 divides (p -' 1) by A16, PEPIN: 22;

 then

 A18: (p -' 1) = (2 * p9) by NAT_D: 3;

 then p9 divides (p -' 1);

 then p9 <= (p -' 1) by A12, NAT_D: 7;

 then

 A19: p9 < p by A11, XREAL_1: 146, XXREAL_0: 2;

 for d be Nat st d in ( dom I) holds ((I . d) gcd p) = 1

 proof

 let d be Nat;

 assume d in ( dom I);

 then

 A20: d in ( Seg ( len I)) by FINSEQ_1:def 3;

 then

 A21: d in ( Seg p9) by CARD_1:def 7;

 then

 A22: (I . d) = d by FINSEQ_2: 49;

 d <= p9 by A21, FINSEQ_1: 1;

 then

 A23: d = 1 by A20, FINSEQ_1: 1;

 then (d,p) are_coprime by A23, EULER_1: 2;

 hence thesis by A22, INT_2:def 3;

 end;

 then

 A24: (( Product I) gcd p) = 1 by WSIERP_1: 36;



 A25: for d st d in ( dom f) holds (f . d) = (a * d)

 proof

 let d;

 assume

 A26: d in ( dom f);

 then d in ( dom I) by A3, VALUED_1:def 5;

 then d in ( Seg ( len I)) by FINSEQ_1:def 3;

 then

 A27: d is Element of ( Seg p9) by CARD_1:def 7;



 thus (f . d) = (a * (I . d)) by A3, A26, VALUED_1:def 5

 .= (a * d) by A27;

 end;



 A28: for d,e be Nat st 1 <= d & d < e & e <= ( len f1) holds (f1 . d) <> (f1 . e)

 proof

 let d,e be Nat;

 assume that

 A29: 1 <= d and

 A30: d < e and

 A31: e <= ( len f1);



 A32: e <= ( len f) by A31, EULER_2:def 1;

 1 <= e by A29, A30, XXREAL_0: 2;

 then

 A33: e in ( dom f) by A32, FINSEQ_3: 25;

 then

 A34: (f1 . e) = ((f . e) mod p) by EULER_2:def 1;

 d < ( len f) by A30, A32, XXREAL_0: 2;

 then

 A35: d in ( dom f) by A29, FINSEQ_3: 25;

 then

 A36: (f1 . d) = ((f . d) mod p) by EULER_2:def 1;

 now

 assume (f1 . d) = (f1 . e);

 then ((f . e),(f . d)) are_congruent_mod p by A36, A34, NAT_D: 64;

 then p divides ((a * e) - (f . d)) by A25, A33;

 then p divides ((a * e) - (a * d)) by A25, A35;

 then

 A37: p divides (a * (e - d));



 A38: (p9 - 1) < p by A19, XREAL_1: 147;

 reconsider dd = (e - d) as Element of NAT by A30, NAT_1: 21;



 A39: |.p.| = p by ABSVALUE:def 1;



 A40: |.dd.| = dd by ABSVALUE:def 1;



 A41: dd <= (p9 - 1) by A13, A5, A29, A31, XREAL_1: 13;

 dd <> 0 by A30;

 then p <= dd by A2, A37, A39, A40, INT_4: 6, WSIERP_1: 29;

 hence contradiction by A41, A38, XXREAL_0: 2;

 end;

 hence thesis;

 end;

 then

 A42: ( len f1) = ( card ( rng f1)) by GRAPH_5: 7;

 then

 A43: f1 is one-to-one by FINSEQ_4: 62;



 A44: ( dom f1) = ( dom f) by A5, FINSEQ_3: 29;

 not 0 in ( rng f1)

 proof

 reconsider a as Element of NAT by ORDINAL1:def 12;

 assume 0 in ( rng f1);

 then

 consider n be Nat such that

 A45: n in ( dom f1) and

 A46: (f1 . n) = 0 by FINSEQ_2: 10;

 0 = ((f . n) mod p) by A44, A45, A46, EULER_2:def 1

 .= ((a * n) mod p) by A25, A44, A45;

 then

 A47: p divides (a * n) by PEPIN: 6;

 n >= 1 by A45, FINSEQ_3: 25;

 then

 A48: p <= n by A2, A47, NAT_D: 7, WSIERP_1: 30;

 n <= p9 by A13, A5, A45, FINSEQ_3: 25;

 hence contradiction by A19, A48, XXREAL_0: 2;

 end;

 then

 A49: { 0 } misses ( rng f1) by ZFMISC_1: 50;

 then

 A50: f2 is one-to-one by A14, FINSEQ_3: 92, XBOOLE_1: 73;



 A51: ( rng f1) c= ( Seg n1) by A14, A49, XBOOLE_1: 73;

 then

 A52: X c= ( Seg n1) by A6;

 ( len f) = ( card ( rng f1)) by A5, A28, GRAPH_5: 7;

 then

 reconsider n = (p9 - m) as Element of NAT by A4, A13, A6, NAT_1: 21, NAT_1: 43;



 A53: Y c= ( Seg n1) by A51, A7;



 A54: ( rng f1) = ( rng f2) by A51, FINSEQ_1:def 13;

 then

 A55: ( Product f1) = ( Product f2) by A43, A50, EULER_2: 10, RFINSEQ: 26;

 set f3 = ((( len (f2 /^ n)) |-> p) - (f2 /^ n));

 set f4 = ((f2 | n) ^ f3);



 A56: (f2 /^ n) is FinSequence of INT by FINSEQ_2: 24, NUMBERS: 17;



 A57: ( dom f3) = (( dom (( len (f2 /^ n)) |-> p)) /\ ( dom (f2 /^ n))) by VALUED_1: 12

 .= (( Seg ( len (( len (f2 /^ n)) |-> p))) /\ ( dom (f2 /^ n))) by FINSEQ_1:def 3

 .= (( dom (f2 /^ n)) /\ ( dom (f2 /^ n))) by FINSEQ_1:def 3, CARD_1:def 7

 .= ( dom (f2 /^ n));

 then

 A58: ( len f3) = ( len (f2 /^ n)) by FINSEQ_3: 29;

 for k,l be Nat st k in Y & l in X holds k < l

 proof

 let k,l be Nat;

 assume that

 A59: k in Y and

 A60: l in X;



 A61: not k in X by A59, XBOOLE_0:def 5;



 A62: ex l1 be Element of NAT st l1 = l & l1 in ( rng f1) & l1 > (p / 2) by A60;

 k in ( rng f1) by A59, XBOOLE_0:def 5;

 then k <= (p / 2) by A61;

 hence thesis by A62, XXREAL_0: 2;

 end;

 then ( Sgm (Y \/ X)) = (( Sgm Y) ^ ( Sgm X)) by A52, A53, FINSEQ_3: 42;

 then ( Sgm (( rng f1) \/ X)) = (( Sgm Y) ^ ( Sgm X)) by XBOOLE_1: 39;

 then

 A63: f2 = (( Sgm Y) ^ ( Sgm X)) by A6, XBOOLE_1: 12;



 A64: for d st d in ( dom f3) holds (f3 . d) = (p - ((f2 /^ n) . d))

 proof

 let d;

 assume

 A65: d in ( dom f3);

 then d in ( Seg ( len (f2 /^ n))) by A57, FINSEQ_1:def 3;

 then ((( len (f2 /^ n)) |-> p) . d) = p by FINSEQ_2: 57;

 hence thesis by A65, VALUED_1: 13;

 end;



 A66: ( len ( Sgm Y)) = ( card Y) by A51, A7, FINSEQ_3: 39, XBOOLE_1: 1

 .= (p9 - m) by A4, A13, A5, A6, A42, CARD_2: 44;

 then

 A67: (f2 /^ n) = ( Sgm X) by A63, FINSEQ_5: 37;



 A68: for d st d in ( dom f3) holds (f3 . d) > 0 & (f3 . d) <= p9

 proof

 let d;

 reconsider w = (f3 . d) as Element of INT by INT_1:def 2;

 assume

 A69: d in ( dom f3);

 then (( Sgm X) . d) in ( rng ( Sgm X)) by A67, A57, FUNCT_1: 3;

 then (( Sgm X) . d) in X by A52, FINSEQ_1:def 13;

 then

 A70: ex ll be Element of NAT st ll = (( Sgm X) . d) & ll in ( rng f1) & ll > (p / 2);

 then

 consider e be Nat such that

 A71: e in ( dom f1) and

 A72: (f1 . e) = ((f2 /^ n) . d) by A67, FINSEQ_2: 10;

 ((f2 /^ n) . d) = ((f . e) mod p) by A44, A71, A72, EULER_2:def 1;

 then

 A73: ((f2 /^ n) . d) < p by NAT_D: 1;



 A74: (f3 . d) = (p - ((f2 /^ n) . d)) by A64, A69;

 then w < (p - (p / 2)) by A67, A70, XREAL_1: 10;

 hence thesis by A17, A74, A73, INT_1: 54, XREAL_1: 50;

 end;



 A75: ( rng f3) c= INT by RELAT_1:def 19;

 for d be Nat st d in ( dom f3) holds (f3 . d) in NAT

 proof

 let d be Nat;

 assume

 A76: d in ( dom f3);

 (f3 . d) > 0 by A68, A76;

 hence thesis by A75, INT_1: 3;

 end;

 then

 reconsider f3 as FinSequence of NAT by FINSEQ_2: 12;

 |.(( - 1) |^ m).| = 1 by SERIES_2: 1;

 then

 A77: (( - 1) |^ m) = 1 or ( - (( - 1) |^ m)) = 1 by ABSVALUE: 1;

 f3 is FinSequence of NAT ;

 then

 reconsider f4 as FinSequence of NAT by FINSEQ_1: 75;



 A78: (f2 | n) = ( Sgm Y) by A63, A66, FINSEQ_3: 113, FINSEQ_6: 10;



 A79: for d st d in ( dom f4) holds (f4 . d) > 0 & (f4 . d) <= p9

 proof

 let d;

 assume

 A80: d in ( dom f4);

 per cases by A80, FINSEQ_1: 25;

 suppose

 A81: d in ( dom (f2 | n));

 reconsider d as Element of NAT by ORDINAL1:def 12;

 ((f2 | n) . d) in ( rng ( Sgm Y)) by A78, A81, FUNCT_1: 3;

 then

 A82: ((f2 | n) . d) in Y by A53, FINSEQ_1:def 13;

 then

 A83: ((f2 | n) . d) in ( rng f1) by XBOOLE_0:def 5;

 not ((f2 | n) . d) in X by A82, XBOOLE_0:def 5;

 then ((f2 | n) . d) <= (p / 2) by A83;

 then

 A84: ((f2 | n) . d) <= p9 by A17, INT_1: 54;

 not ((f2 | n) . d) in { 0 } by A49, A83, XBOOLE_0: 3;

 then ((f2 | n) . d) <> 0 by TARSKI:def 1;

 hence thesis by A81, A84, FINSEQ_1:def 7;

 end;

 suppose ex l be Nat st l in ( dom f3) & d = (( len (f2 | n)) + l);

 then

 consider l be Element of NAT such that

 A85: l in ( dom f3) and

 A86: d = (( len (f2 | n)) + l);

 (f4 . d) = (f3 . l) by A85, A86, FINSEQ_1:def 7;

 hence thesis by A68, A85;

 end;

 end;



 A87: f2 = ((f2 | n) ^ (f2 /^ n)) by RFINSEQ: 8;

 then

 A88: (f2 /^ n) is one-to-one by A50, FINSEQ_3: 91;

 for d,e be Nat st 1 <= d & d < e & e <= ( len f3) holds (f3 . d) <> (f3 . e)

 proof

 let d,e be Nat;

 assume that

 A89: 1 <= d and

 A90: d < e and

 A91: e <= ( len f3);

 1 <= e by A89, A90, XXREAL_0: 2;

 then

 A92: e in ( dom f3) by A91, FINSEQ_3: 25;

 then

 A93: (f3 . e) = (p - ((f2 /^ n) . e)) by A64;

 d < ( len f3) by A90, A91, XXREAL_0: 2;

 then

 A94: d in ( dom f3) by A89, FINSEQ_3: 25;

 then (f3 . d) = (p - ((f2 /^ n) . d)) by A64;

 hence thesis by A88, A57, A90, A94, A92, A93;

 end;

 then ( len f3) = ( card ( rng f3)) by GRAPH_5: 7;

 then

 A95: f3 is one-to-one by FINSEQ_4: 62;



 A96: ( len f2) = p9 by A13, A5, A14, A49, A42, FINSEQ_3: 39, XBOOLE_1: 73;

 then

 A97: n <= ( len f2) by XREAL_1: 43;



 A98: ( rng (f2 | n)) misses ( rng f3)

 proof

 assume ( rng (f2 | n)) meets ( rng f3);

 then

 consider x be object such that

 A99: x in ( rng (f2 | n)) and

 A100: x in ( rng f3) by XBOOLE_0: 3;

 consider e be Nat such that

 A101: e in ( dom f3) and

 A102: (f3 . e) = x by A100, FINSEQ_2: 10;

 x = (p - ((f2 /^ n) . e)) by A64, A101, A102;

 then

 A103: x = (p - (f2 . (e + n))) by A97, A57, A101, RFINSEQ:def 1;

 (e + n) in ( dom f2) by A57, A101, FINSEQ_5: 26;

 then

 consider e1 be Nat such that

 A104: e1 in ( dom f1) and

 A105: (f1 . e1) = (f2 . (e + n)) by A54, FINSEQ_2: 10, FUNCT_1: 3;



 A106: e1 in ( dom f) by A5, A104, FINSEQ_3: 29;



 A107: e1 <= p9 by A13, A5, A104, FINSEQ_3: 25;

 ( rng (f2 | n)) c= ( rng f2) by FINSEQ_5: 19;

 then

 consider d1 be Nat such that

 A108: d1 in ( dom f1) and

 A109: (f1 . d1) = x by A54, A99, FINSEQ_2: 10;

 d1 <= p9 by A13, A5, A108, FINSEQ_3: 25;

 then (d1 + e1) <= (p9 + p9) by A107, XREAL_1: 7;

 then

 A110: (d1 + e1) < p by A11, A18, XREAL_1: 146, XXREAL_0: 2;

 x = ((f . d1) mod p) by A44, A108, A109, EULER_2:def 1;

 then (((f . d1) mod p) + (f2 . (e + n))) = p by A103;

 then (((f . d1) mod p) + ((f . e1) mod p)) = p by A105, A106, EULER_2:def 1;

 then ((((f . d1) mod p) + ((f . e1) mod p)) mod p) = 0 by NAT_D: 25;

 then (((f . d1) + (f . e1)) mod p) = 0 by EULER_2: 6;

 then p divides ((f . d1) + (f . e1)) by PEPIN: 6;

 then p divides ((d1 * a) + (f . e1)) by A25, A44, A108;

 then p divides ((d1 * a) + (e1 * a)) by A25, A106;

 then

 A111: p divides ((d1 + e1) * a);

 d1 >= 1 by A108, FINSEQ_3: 25;

 hence contradiction by A2, A111, A110, NAT_D: 7, WSIERP_1: 30;

 end;

 (f2 | n) is one-to-one by A50, A87, FINSEQ_3: 91;

 then

 A112: f4 is one-to-one by A95, A98, FINSEQ_3: 91;



 A113: for d st d in ( dom f3) holds ((f3 . d),( - ((f2 /^ n) . d))) are_congruent_mod p

 proof

 let d;

 assume d in ( dom f3);



 then ((f3 . d) mod p) = ((p - ((f2 /^ n) . d)) mod p) by A64

 .= (((1 * p) + ( - ((f2 /^ n) . d))) mod p)

 .= (( - ((f2 /^ n) . d)) mod p) by EULER_1: 12;

 hence thesis by NAT_D: 64;

 end;



 A114: ( len (f2 /^ n)) = (( len f2) -' n) by RFINSEQ: 29

 .= (( len f2) - n) by A96, XREAL_1: 43, XREAL_1: 233

 .= m by A96;

 ( len (f2 | n)) = n by A96, FINSEQ_1: 59, XREAL_1: 43;



 then ( len f4) = (n + m) by A58, A114, FINSEQ_1: 22

 .= ( len f) by A13;

 then ( rng f4) = ( rng I) by A13, A112, A79, Th40;

 then ( Product f4) = ( Product I) by A112, EULER_2: 10, RFINSEQ: 26;

 then

 A115: (( Product (f2 | n)) * ( Product f3)) = ( Product I) by RVSUM_1: 97;

 f3 is FinSequence of INT by FINSEQ_2: 24, NUMBERS: 17;

 then ((( Product f3) * ( Product (f2 | n))),(((( - 1) |^ m) * ( Product (f2 /^ n))) * ( Product (f2 | n)))) are_congruent_mod p by A58, A114, A56, A113, Th33, INT_4: 11;

 then ((( Product f3) * ( Product (f2 | n))),((( - 1) |^ m) * (( Product (f2 | n)) * ( Product (f2 /^ n))))) are_congruent_mod p;

 then (( Product I),((( - 1) |^ m) * ( Product ((f2 | n) ^ (f2 /^ n))))) are_congruent_mod p by A115, RVSUM_1: 97;

 then

 A116: (( Product I),((( - 1) |^ m) * ( Product f1))) are_congruent_mod p by A55, RFINSEQ: 8;

 (((( - 1) |^ m) * ( Product f1)),((( - 1) |^ m) * ( Product f))) are_congruent_mod p by A9, INT_4: 11;

 then (( Product I),(((( - 1) |^ m) * (a |^ p9)) * ( Product I))) are_congruent_mod p by A15, A116, INT_1: 15;

 then p divides ((1 - ((( - 1) |^ m) * (a |^ p9))) * ( Product I));

 then p divides (1 - ((( - 1) |^ m) * (a |^ p9))) by A24, WSIERP_1: 29;

 then p divides ((( - 1) |^ m) * (1 - ((( - 1) |^ m) * (a |^ p9)))) by INT_2: 2;

 then

 A117: p divides ((( - 1) |^ m) - (((( - 1) |^ m) * (( - 1) |^ m)) * (a |^ p9)));

 ((( - 1) |^ m) * (( - 1) |^ m)) = (( - 1) |^ (m + m)) by NEWTON: 8

 .= (( - 1) |^ (2 * m))

 .= ((( - 1) |^ 2) |^ m) by NEWTON: 9

 .= ((1 |^ 2) |^ m) by WSIERP_1: 1

 .= 1;

 then ((( - 1) |^ m),(a |^ p9)) are_congruent_mod p by A117;

 then

 A118: ((( - 1) |^ m),( Lege (a,p))) are_congruent_mod p by A8, INT_1: 15;

 per cases by A77;

 suppose

 A119: (( - 1) |^ m) = 1;

 then

 A120: ( Lege (a,p)) <> ( - 1) by A118, A1, NAT_D: 7;

 now

 assume ( Lege (a,p)) = 0 ;

 then p divides (1 - 0 ) by A118, A119;

 then p = 1 by WSIERP_1: 15;

 hence contradiction by A1;

 end;

 hence thesis by A119, Th25, A120;

 end;

 suppose

 A121: (( - 1) |^ m) = ( - 1);

 A122:

 now

 assume ( Lege (a,p)) = 1;

 then p divides ( - 2) by A118, A121;

 then p divides 2 by INT_2: 10;

 hence contradiction by A1, NAT_D: 7;

 end;

 now

 assume ( Lege (a,p)) = 0 ;

 then p divides (( - 1) - 0 ) by A118, A121;

 then p = 1 by WSIERP_1: 15, INT_2: 10;

 hence contradiction by A1;

 end;

 hence thesis by A121, Th25, A122;

 end;

 end;

 theorem :: INT_5:42



 Th42: p > 2 implies ( Lege (2,p)) = (( - 1) |^ (((p ^2 ) -' 1) div 8))

 proof

 set p9 = ((p -' 1) div 2);

 set I = ( idseq p9);

 set fp = (2 * I);

 set nn = (p div 8);



 A1: p > 1 by INT_2:def 4;

 then

 A2: (p - 1) = (p -' 1) by XREAL_1: 233;



 A3: for d st d in ( dom fp) holds (fp . d) = (2 * d)

 proof

 let d;

 assume

 A4: d in ( dom fp);

 then d in ( dom I) by VALUED_1:def 5;

 then d in ( Seg ( len I)) by FINSEQ_1:def 3;

 then

 A5: d is Element of ( Seg p9) by CARD_1:def 7;



 thus (fp . d) = (2 * (I . d)) by A4, VALUED_1:def 5

 .= (2 * d) by A5;

 end;

 for d be Nat st d in ( dom fp) holds (fp . d) in NAT ;

 then

 reconsider fp as FinSequence of NAT by FINSEQ_2: 12;

 set f = (fp mod p);

 set X = { k where k be Element of NAT : k in ( rng f) & k > (p / 2) };

 set m = ( card X);

 ( dom fp) = ( dom I) by VALUED_1:def 5;



 then

 A6: ( len fp) = ( len I) by FINSEQ_3: 29

 .= p9 by CARD_1:def 7;

 set Y = { d where d be Element of NAT : d in ( dom f) & (f . d) > (p / 2) };

 for x be object st x in Y holds x in ( dom f)

 proof

 let x be object;

 assume x in Y;

 then ex k be Element of NAT st x = k & k in ( dom f) & (f . k) > (p / 2);

 hence thesis;

 end;

 then Y c= ( dom f);

 then

 reconsider Y as finite Subset of NAT by XBOOLE_1: 1;

 set Z = ( seq ((p div 4),(p9 -' (p div 4))));



 A7: (p mod 8) <= (8 - 1) by INT_1: 52, NAT_D: 1;

 8 = (2 * 4);

 then

 A8: 2 divides 8;

 A9:

 now

 assume (p mod 8) = 0 ;

 then 8 divides p by PEPIN: 6;

 then p = 8 by INT_2:def 4;

 hence contradiction by A8, NAT_4: 12;

 end;

 for x be object st x in X holds x in ( rng f)

 proof

 let x be object;

 assume x in X;

 then ex k be Element of NAT st x = k & k in ( rng f) & k > (p / 2);

 hence thesis;

 end;

 then

 A10: X c= ( rng f);

 then

 reconsider X as finite set;

 ( card X) is Element of NAT ;

 then

 reconsider m as Element of NAT ;



 A11: ( len f) = ( len fp) by EULER_2:def 1;

 then

 A12: ( dom f) = ( dom fp) by FINSEQ_3: 29;

 assume

 A13: p > 2;

 then (2,p) are_coprime by EULER_1: 2;

 then

 A14: (2 gcd p) = 1 by INT_2:def 3;

 then

 A15: ( Lege (2,p)) = (( - 1) |^ m) by A13, Th41;

 p is odd by A13, PEPIN: 17;

 then

 A16: (p - 1) is even by HILBERT3: 2;



 then

 A17: p9 = (((p -' 1) + 1) div 2) by A2, NAT_2: 26

 .= (p div 2) by A1, XREAL_1: 235;

 then

 A18: f <> {} by A13, A6, A11, NAT_2: 13;

 then

 reconsider U = ( dom f) as non empty finite Subset of NAT ;

 2 divides (p -' 1) by A16, A2, PEPIN: 22;

 then

 A19: (p -' 1) = (2 * p9) by NAT_D: 3;



 A20: for d st d in ( dom f) holds (f . d) = (2 * d)

 proof

 let d;

 assume

 A21: d in ( dom f);

 then d <= p9 by A6, A11, FINSEQ_3: 25;

 then (2 * d) <= (p -' 1) by A19, XREAL_1: 64;

 then (2 * d) < p by NAT_2: 9, XXREAL_0: 2;



 hence (2 * d) = ((2 * d) mod p) by NAT_D: 24

 .= ((fp . d) mod p) by A3, A12, A21

 .= (f . d) by A12, A21, EULER_2:def 1;

 end;



 A22: for d1,d2,k1,k2 be Nat st 1 <= d1 & d1 < d2 & d2 <= ( len f) & k1 = (f . d1) & k2 = (f . d2) holds k1 < k2

 proof

 let d1,d2,k1,k2 be Nat;

 assume that

 A23: 1 <= d1 and

 A24: d1 < d2 and

 A25: d2 <= ( len f) and

 A26: k1 = (f . d1) and

 A27: k2 = (f . d2);

 1 <= d2 by A23, A24, XXREAL_0: 2;

 then d2 in ( dom f) by A25, FINSEQ_3: 25;

 then

 A28: k2 = (2 * d2) by A20, A27;

 d1 <= ( len f) by A24, A25, XXREAL_0: 2;

 then d1 in ( dom f) by A23, FINSEQ_3: 25;

 then k1 = (2 * d1) by A20, A26;

 hence thesis by A24, A28, XREAL_1: 68;

 end;

 ( rng f) is non empty Subset of NAT by A18;

 then

 consider n1 be Element of NAT such that

 A29: ( rng f) c= (( Seg n1) \/ { 0 }) by HEYTING3: 1;

 reconsider X as finite Subset of NAT by A10, XBOOLE_1: 1;

 (Z,(((p -' 1) div 2) -' (p div 4))) are_equipotent by CALCUL_2: 6;

 then

 A30: ( card Z) = (((p -' 1) div 2) -' (p div 4)) by CARD_1:def 2;

 not 0 in ( rng f)

 proof

 assume 0 in ( rng f);

 then

 consider n be Nat such that

 A31: n in ( dom f) and

 A32: (f . n) = 0 by FINSEQ_2: 10;

 (2 * n) = 0 by A20, A31, A32;

 hence contradiction by A31, FINSEQ_3: 25;

 end;

 then

 A33: { 0 } misses ( rng f) by ZFMISC_1: 50;

 then ( rng f) c= ( Seg n1) by A29, XBOOLE_1: 73;

 then

 A34: ( Sgm ( rng f)) = f by A22, FINSEQ_1:def 13;



 A35: (X,Y) are_equipotent

 proof

 deffunc F( Element of U) = (f . $1);

 set YY = { d where d be Element of U : F(d) in X };

 A36:

 now

 let x be set;

 assume x in X;

 then

 consider y be Element of NAT such that

 A37: y = x and

 A38: y in ( rng f) and y > (p / 2);

 consider d be Nat such that

 A39: d in U and

 A40: (f . d) = y by A38, FINSEQ_2: 10;

 reconsider d as Element of U by A39;

 take d;

 thus x = F(d) by A37, A40;

 end;



 A41: Y c= YY

 proof

 let x be object;

 assume x in Y;

 then

 A42: ex d be Element of NAT st d = x & d in ( dom f) & (f . d) > (p / 2);

 then

 reconsider x as Element of U;

 reconsider f as FinSequence of NAT qua set;

 (f . x) in ( rng f) by FUNCT_1: 3;

 then F(x) in X by A42;

 hence thesis;

 end;

 now

 let x be object;

 assume x in YY;

 then

 consider d be Element of U such that

 A43: d = x and

 A44: (f . d) in X;

 ex k be Element of NAT st k = (f . d) & k in ( rng f) & k > (p / 2) by A44;

 hence x in Y by A43;

 end;

 then

 A45: YY c= Y;



 A46: for d1,d2 be Element of U st F(d1) = F(d2) holds d1 = d2

 proof

 let d1,d2 be Element of U;

 assume

 A47: F(d1) = F(d2);

 f is one-to-one by A29, A33, A34, FINSEQ_3: 92, XBOOLE_1: 73;

 hence thesis by A47;

 end;

 (X,YY) are_equipotent from FUNCT_7:sch 3( A36, A46);

 hence thesis by A41, A45, XBOOLE_0:def 10;

 end;

 (p div 2) < p by INT_1: 56;

 then ((p div 2) div 2) <= (p div 2) by NAT_2: 24;

 then

 A48: (p div (2 * 2)) <= (p div 2) by NAT_2: 27;



 A49: Z c= Y

 proof

 let x be object;

 assume

 A50: x in Z;

 then

 reconsider x as Element of NAT ;



 A51: x >= ((p div 4) + 1) by A50, CALCUL_2: 1;

 then ((p div 4) + x) >= ((p div 4) + 1) by NAT_1: 12;

 then

 A52: x >= 1 by XREAL_1: 6;

 x <= ((((p -' 1) div 2) -' (p div 4)) + (p div 4)) by A50, CALCUL_2: 1;

 then x <= ((p -' 1) div 2) by A17, A48, XREAL_1: 235;

 then

 A53: x in ( dom f) by A6, A11, A52, FINSEQ_3: 25;

 x > (p / 4) by A51, INT_1: 29, XXREAL_0: 2;

 then (2 * x) > (2 * (p / 4)) by XREAL_1: 68;

 then (f . x) > (p / 2) by A20, A53;

 hence thesis by A53;

 end;

 now

 let x be object;



 A54: (p / 4) >= [\(p / 4)/] by INT_1:def 6;

 assume x in Y;

 then

 consider x1 be Element of NAT such that

 A55: x1 = x and

 A56: x1 in ( dom f) and

 A57: (f . x1) > (p / 2);

 (2 * x1) > (p / 2) by A20, A56, A57;

 then x1 > ((p / 2) / 2) by XREAL_1: 83;

 then x1 > [\(p / 4)/] by A54, XXREAL_0: 2;

 then

 A58: x1 >= ((p div 4) + 1) by NAT_1: 13;

 x1 <= p9 by A6, A11, A56, FINSEQ_3: 25;

 then x1 <= ((p9 -' (p div 4)) + (p div 4)) by A17, A48, XREAL_1: 235;

 hence x in Z by A55, A58;

 end;

 then Y c= Z;

 then Y = Z by A49, XBOOLE_0:def 10;

 then

 A59: m = (((p -' 1) div 2) -' (p div 4)) by A30, A35, CARD_1: 5;

 A60:

 now

 assume (p mod 8) = 2;

 then 8 divides (p - 2) by PEPIN: 8;

 then 2 divides (p - 2) by A8, INT_2: 9;

 then 2 divides ( - (p - 2)) by INT_2: 10;

 then 2 divides (2 - p);

 then 2 divides p by Th2;

 hence contradiction by A13, NAT_4: 12;

 end;

 A61:

 now

 assume (p mod 8) = 4;

 then 8 divides (p - 4) by PEPIN: 8;

 then 2 divides (p - 4) by A8, INT_2: 9;

 then 2 divides ( - (p - 4)) by INT_2: 10;

 then

 A62: 2 divides (4 - p);

 4 = (2 * 2);

 then 2 divides 4;

 then 2 divides p by A62, Th2;

 hence contradiction by A13, NAT_4: 12;

 end;

 A63:

 now

 assume (p mod 8) = 6;

 then 8 divides (p - 6) by PEPIN: 8;

 then 2 divides (p - 6) by A8, INT_2: 9;

 then 2 divides ( - (p - 6)) by INT_2: 10;

 then

 A64: 2 divides (6 - p);

 6 = (2 * 3);

 then 2 divides 6;

 then 2 divides p by A64, Th2;

 hence contradiction by A13, NAT_4: 12;

 end;

 (p mod 8) = 0 or ... or (p mod 8) = 7 by A7;

 per cases by A9, A60, A61, A63;

 suppose (p mod 8) = 1;

 then

 A65: p = ((8 * nn) + 1) by NAT_D: 2;

 then (p -' 1) = (2 * (4 * nn)) by A2;

 then

 A66: ((p -' 1) div 2) = (4 * nn) by NAT_D: 18;

 (p div 4) = (((4 * (2 * nn)) + 1) div 4) by A65

 .= ((2 * nn) + (1 div 4)) by NAT_D: 61

 .= ((2 * nn) + 0 ) by NAT_D: 27;



 then m = ((4 * nn) - (2 * nn)) by A59, A66, XREAL_1: 64, XREAL_1: 233

 .= (2 * nn);



 then

 A67: ( Lege (2,p)) = ((( - 1) |^ 2) |^ nn) by A15, NEWTON: 9

 .= ((1 |^ 2) |^ nn) by WSIERP_1: 1

 .= 1;

 (((p ^2 ) -' 1) div 8) = ((((((8 * nn) ^2 ) + (2 * (8 * nn))) + 1) -' 1) div 8) by A65

 .= ((8 * ((8 * (nn ^2 )) + (2 * nn))) div 8) by NAT_D: 34

 .= ((8 * (nn ^2 )) + (2 * nn)) by NAT_D: 18;



 hence (( - 1) |^ (((p ^2 ) -' 1) div 8)) = (( - 1) |^ (2 * ((4 * (nn ^2 )) + nn)))

 .= ((( - 1) |^ 2) |^ ((4 * (nn ^2 )) + nn)) by NEWTON: 9

 .= ((1 |^ 2) |^ ((4 * (nn ^2 )) + nn)) by WSIERP_1: 1

 .= ( Lege (2,p)) by A67;

 end;

 suppose (p mod 8) = 3;

 then

 A68: p = ((8 * nn) + 3) by NAT_D: 2;

 then (p -' 1) = (2 * ((4 * nn) + 1)) by A2;

 then

 A69: ((p -' 1) div 2) = ((4 * nn) + 1) by NAT_D: 18;



 A70: (4 * nn) >= (2 * nn) by XREAL_1: 64;

 (p div 4) = (((4 * (2 * nn)) + 3) div 4) by A68

 .= ((2 * nn) + (3 div 4)) by NAT_D: 61

 .= ((2 * nn) + 0 ) by NAT_D: 27;



 then m = (((4 * nn) + 1) - (2 * nn)) by A59, A69, A70, NAT_1: 12, XREAL_1: 233

 .= ((2 * nn) + 1);



 then

 A71: ( Lege (2,p)) = ((( - 1) |^ (2 * nn)) * ( - 1)) by A15, NEWTON: 6

 .= (((( - 1) |^ 2) |^ nn) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ nn) * ( - 1)) by WSIERP_1: 1

 .= ( - 1);

 (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (6 * nn))) + (3 * 3)) - 1) div 8) by A68, NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (6 * nn)) + 1)) div 8)

 .= (((8 * (nn ^2 )) + (6 * nn)) + 1) by NAT_D: 18;



 hence (( - 1) |^ (((p ^2 ) -' 1) div 8)) = ((( - 1) |^ (2 * ((4 * (nn ^2 )) + (3 * nn)))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ ((4 * (nn ^2 )) + (3 * nn))) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ ((4 * (nn ^2 )) + (3 * nn))) * ( - 1)) by WSIERP_1: 1

 .= ( Lege (2,p)) by A71;

 end;

 suppose (p mod 8) = 5;

 then

 A72: p = ((8 * nn) + 5) by NAT_D: 2;

 then (p -' 1) = (2 * ((4 * nn) + 2)) by A2;

 then

 A73: ((p -' 1) div 2) = ((4 * nn) + 2) by NAT_D: 18;



 A74: (4 * nn) >= (2 * nn) by XREAL_1: 64;

 (p div 4) = (((4 * ((2 * nn) + 1)) + 1) div 4) by A72

 .= (((2 * nn) + 1) + (1 div 4)) by NAT_D: 61

 .= (((2 * nn) + 1) + 0 ) by NAT_D: 27;



 then m = (((4 * nn) + 2) - ((2 * nn) + 1)) by A59, A73, A74, XREAL_1: 7, XREAL_1: 233

 .= ((2 * nn) + 1);



 then

 A75: ( Lege (2,p)) = ((( - 1) |^ (2 * nn)) * ( - 1)) by A15, NEWTON: 6

 .= (((( - 1) |^ 2) |^ nn) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ nn) * ( - 1)) by WSIERP_1: 1

 .= ( - 1);

 (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (10 * nn))) + 25) - 1) div 8) by A72, NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (10 * nn)) + 3)) div 8)

 .= (((8 * (nn ^2 )) + (10 * nn)) + 3) by NAT_D: 18;



 hence (( - 1) |^ (((p ^2 ) -' 1) div 8)) = (( - 1) |^ ((((2 * (4 * (nn ^2 ))) + (2 * (5 * nn))) + (2 * 1)) + 1))

 .= ((( - 1) |^ (2 * (((4 * (nn ^2 )) + (5 * nn)) + 1))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ (((4 * (nn ^2 )) + (5 * nn)) + 1)) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ (((4 * (nn ^2 )) + (5 * nn)) + 1)) * ( - 1)) by WSIERP_1: 1

 .= ( Lege (2,p)) by A75;

 end;

 suppose (p mod 8) = 7;

 then

 A76: p = ((8 * nn) + 7) by NAT_D: 2;

 then (p -' 1) = (2 * ((4 * nn) + 3)) by A2;

 then

 A77: ((p -' 1) div 2) = ((4 * nn) + 3) by NAT_D: 18;



 A78: (4 * nn) >= (2 * nn) by XREAL_1: 64;

 (p div 4) = (((4 * ((2 * nn) + 1)) + 3) div 4) by A76

 .= (((2 * nn) + 1) + (3 div 4)) by NAT_D: 61

 .= (((2 * nn) + 1) + 0 ) by NAT_D: 27;



 then m = (((4 * nn) + 3) - ((2 * nn) + 1)) by A59, A77, A78, XREAL_1: 7, XREAL_1: 233

 .= ((2 * nn) + 2);



 then

 A79: ( Lege (2,p)) = (( - 1) |^ (2 * (nn + 1))) by A13, A14, Th41

 .= ((( - 1) |^ 2) |^ (nn + 1)) by NEWTON: 9

 .= ((1 |^ 2) |^ (nn + 1)) by WSIERP_1: 1

 .= 1;

 (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (14 * nn))) + 49) - 1) div 8) by A76, NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (14 * nn)) + 6)) div 8)

 .= (((8 * (nn ^2 )) + (14 * nn)) + 6) by NAT_D: 18;



 hence (( - 1) |^ (((p ^2 ) -' 1) div 8)) = (( - 1) |^ (2 * (((4 * (nn ^2 )) + (7 * nn)) + 3)))

 .= ((( - 1) |^ 2) |^ (((4 * (nn ^2 )) + (7 * nn)) + 3)) by NEWTON: 9

 .= ((1 |^ 2) |^ (((4 * (nn ^2 )) + (7 * nn)) + 3)) by WSIERP_1: 1

 .= ( Lege (2,p)) by A79;

 end;

 end;

 theorem :: INT_5:43

 p > 2 & ((p mod 8) = 1 or (p mod 8) = 7) implies 2 is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (p mod 8) = 1 or (p mod 8) = 7;

 set nn = (p div 8);

 per cases by A2;

 suppose (p mod 8) = 1;

 then p = ((8 * nn) + 1) by NAT_D: 2;



 then (((p ^2 ) -' 1) div 8) = ((((((8 * nn) ^2 ) + (2 * (8 * nn))) + 1) -' 1) div 8)

 .= ((8 * ((8 * (nn ^2 )) + (2 * nn))) div 8) by NAT_D: 34

 .= (2 * ((4 * (nn ^2 )) + nn)) by NAT_D: 18;



 then ( Lege (2,p)) = (( - 1) |^ (2 * ((4 * (nn ^2 )) + nn))) by A1, Th42

 .= ((( - 1) |^ 2) |^ ((4 * (nn ^2 )) + nn)) by NEWTON: 9

 .= ((1 |^ 2) |^ ((4 * (nn ^2 )) + nn)) by WSIERP_1: 1

 .= 1;

 hence thesis by Def3;

 end;

 suppose (p mod 8) = 7;

 then p = ((8 * nn) + 7) by NAT_D: 2;



 then (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (14 * nn))) + 49) - 1) div 8) by NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (14 * nn)) + 6)) div 8)

 .= (2 * (((4 * (nn ^2 )) + (7 * nn)) + 3)) by NAT_D: 18;



 then ( Lege (2,p)) = (( - 1) |^ (2 * (((4 * (nn ^2 )) + (7 * nn)) + 3))) by A1, Th42

 .= ((( - 1) |^ 2) |^ (((4 * (nn ^2 )) + (7 * nn)) + 3)) by NEWTON: 9

 .= ((1 |^ 2) |^ (((4 * (nn ^2 )) + (7 * nn)) + 3)) by WSIERP_1: 1

 .= 1;

 hence thesis by Def3;

 end;

 end;

 theorem :: INT_5:44

 p > 2 & ((p mod 8) = 3 or (p mod 8) = 5) implies not 2 is_quadratic_residue_mod p

 proof

 assume that

 A1: p > 2 and

 A2: (p mod 8) = 3 or (p mod 8) = 5;

 set nn = (p div 8);

 per cases by A2;

 suppose (p mod 8) = 3;

 then p = ((8 * nn) + 3) by NAT_D: 2;



 then (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (6 * nn))) + (3 * 3)) - 1) div 8) by NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (6 * nn)) + 1)) div 8)

 .= (((8 * (nn ^2 )) + (6 * nn)) + 1) by NAT_D: 18;



 then ( Lege (2,p)) = (( - 1) |^ (((8 * (nn ^2 )) + (6 * nn)) + 1)) by A1, Th42

 .= ((( - 1) |^ (2 * ((4 * (nn ^2 )) + (3 * nn)))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ ((4 * (nn ^2 )) + (3 * nn))) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ ((4 * (nn ^2 )) + (3 * nn))) * ( - 1)) by WSIERP_1: 1

 .= ( - 1);

 then not (2 is_quadratic_residue_mod p & (2 mod p) <> 0 ) & not (2 is_quadratic_residue_mod p & (2 mod p) = 0 ) by Def3;

 hence thesis;

 end;

 suppose (p mod 8) = 5;

 then p = ((8 * nn) + 5) by NAT_D: 2;



 then (((p ^2 ) -' 1) div 8) = (((((8 * (8 * (nn ^2 ))) + (8 * (10 * nn))) + 25) - 1) div 8) by NAT_1: 12, XREAL_1: 233

 .= ((8 * (((8 * (nn ^2 )) + (10 * nn)) + 3)) div 8)

 .= (((8 * (nn ^2 )) + (10 * nn)) + 3) by NAT_D: 18;



 then ( Lege (2,p)) = (( - 1) |^ ((((2 * (4 * (nn ^2 ))) + (2 * (5 * nn))) + (2 * 1)) + 1)) by A1, Th42

 .= ((( - 1) |^ (2 * (((4 * (nn ^2 )) + (5 * nn)) + 1))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ (((4 * (nn ^2 )) + (5 * nn)) + 1)) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ (((4 * (nn ^2 )) + (5 * nn)) + 1)) * ( - 1)) by WSIERP_1: 1

 .= ( - 1);

 then not (2 is_quadratic_residue_mod p & (2 mod p) <> 0 ) & not (2 is_quadratic_residue_mod p & (2 mod p) = 0 ) by Def3;

 hence thesis;

 end;

 end;

 theorem :: INT_5:45



 Th45: for a,b be Nat st (a mod 2) = (b mod 2) holds (( - 1) |^ a) = (( - 1) |^ b)

 proof

 let a,b be Nat;

 assume (a mod 2) = (b mod 2);

 then (a,b) are_congruent_mod 2 by NAT_D: 64;

 then

 A1: 2 divides (a - b);

 per cases ;

 suppose a >= b;

 then

 reconsider l = (a - b) as Element of NAT by NAT_1: 21;

 consider n be Nat such that

 A2: l = (2 * n) by A1, NAT_D:def 3;

 (( - 1) |^ a) = (( - 1) |^ (b + (2 * n))) by A2

 .= ((( - 1) |^ b) * (( - 1) |^ (2 * n))) by NEWTON: 8

 .= ((( - 1) |^ b) * ((( - 1) |^ 2) |^ n)) by NEWTON: 9

 .= ((( - 1) |^ b) * ((1 |^ 2) |^ n)) by WSIERP_1: 1

 .= ((( - 1) |^ b) * 1);

 hence thesis;

 end;

 suppose a < b;

 then

 reconsider l = (b - a) as Element of NAT by NAT_1: 21;

 2 divides ( - (a - b)) by A1, INT_2: 10;

 then

 consider n be Nat such that

 A3: l = (2 * n) by NAT_D:def 3;

 (( - 1) |^ b) = (( - 1) |^ (a + (2 * n))) by A3

 .= ((( - 1) |^ a) * (( - 1) |^ (2 * n))) by NEWTON: 8

 .= ((( - 1) |^ a) * ((( - 1) |^ 2) |^ n)) by NEWTON: 9

 .= ((( - 1) |^ a) * ((1 |^ 2) |^ n)) by WSIERP_1: 1

 .= ((( - 1) |^ a) * 1);

 hence thesis;

 end;

 end;

 reserve f,g,h,k for FinSequence of REAL ;

 theorem :: INT_5:46



 Th46: ( len f) = ( len h) & ( len g) = ( len k) implies ((f ^ g) - (h ^ k)) = ((f - h) ^ (g - k))

 proof

 assume that

 A1: ( len f) = ( len h) and

 A2: ( len g) = ( len k);



 A3: ( len (f - h)) = ( len f) by A1, TOPREAL7: 7;

 ( len (f ^ g)) = (( len h) + ( len k)) by A1, A2, FINSEQ_1: 22;

 then ( len (f ^ g)) = ( len (h ^ k)) by FINSEQ_1: 22;

 then

 A4: ( len ((f ^ g) - (h ^ k))) = ( len (f ^ g)) by TOPREAL7: 7;



 A5: ( len (g - k)) = ( len g) by A2, TOPREAL7: 7;

 then ( len ((f - h) ^ (g - k))) = (( len f) + ( len g)) by A3, FINSEQ_1: 22;

 then ( len ((f ^ g) - (h ^ k))) = ( len ((f - h) ^ (g - k))) by A4, FINSEQ_1: 22;

 then

 A6: ( dom ((f ^ g) - (h ^ k))) = ( dom ((f - h) ^ (g - k))) by FINSEQ_3: 29;

 for d be Nat st d in ( dom ((f - h) ^ (g - k))) holds (((f - h) ^ (g - k)) . d) = (((f ^ g) - (h ^ k)) . d)

 proof

 let d be Nat;

 assume

 A7: d in ( dom ((f - h) ^ (g - k)));

 per cases by A7, FINSEQ_1: 25;

 suppose

 A8: d in ( dom (f - h));



 then

 A9: (((f - h) ^ (g - k)) . d) = ((f - h) . d) by FINSEQ_1:def 7

 .= ((f . d) - (h . d)) by A8, VALUED_1: 13;



 A10: ( dom f) = ( dom (f - h)) by A1, TOPREAL7: 7;



 A11: ( dom h) = ( dom (f - h)) by A1, A3, FINSEQ_3: 29;

 (((f ^ g) - (h ^ k)) . d) = (((f ^ g) . d) - ((h ^ k) . d)) by A6, A8, FINSEQ_2: 15, VALUED_1: 13

 .= ((f . d) - ((h ^ k) . d)) by A8, A10, FINSEQ_1:def 7

 .= ((f . d) - (h . d)) by A8, A11, FINSEQ_1:def 7;

 hence thesis by A9;

 end;

 suppose ex e be Nat st e in ( dom (g - k)) & d = (( len (f - h)) + e);

 then

 consider e such that

 A12: e in ( dom (g - k)) and

 A13: d = (( len (f - h)) + e);

 e in ( dom g) by A2, A12, TOPREAL7: 7;

 then

 A14: ((f ^ g) . d) = (g . e) by A3, A13, FINSEQ_1:def 7;

 e in ( dom k) by A2, A5, A12, FINSEQ_3: 29;

 then

 A15: ((h ^ k) . d) = (k . e) by A1, A3, A13, FINSEQ_1:def 7;

 (((f - h) ^ (g - k)) . d) = ((g - k) . e) by A12, A13, FINSEQ_1:def 7

 .= ((g . e) - (k . e)) by A12, VALUED_1: 13;

 hence thesis by A6, A12, A13, A14, A15, FINSEQ_1: 28, VALUED_1: 13;

 end;

 end;

 hence thesis by A6;

 end;

 theorem :: INT_5:47



 Th47: for f be FinSequence of REAL , m be Real holds ( Sum ((( len f) |-> m) - f)) = ((( len f) * m) - ( Sum f))

 proof

 defpred P[ Nat] means for f be FinSequence of REAL , m be Real st ( len f) = $1 holds ( Sum (($1 |-> m) - f)) = (($1 * m) - ( Sum f));



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 P[(n + 1)]

 proof

 let f be FinSequence of REAL , m be Real;



 A3: ( len <*m*>) = 1 by FINSEQ_1: 39;

 assume

 A4: ( len f) = (n + 1);

 then f <> {} ;

 then

 consider f1 be FinSequence of REAL , x be Element of REAL such that

 A5: f = (f1 ^ <*x*>) by HILBERT2: 4;

 reconsider mm = m as Element of REAL by XREAL_0:def 1;



 A6: (n + 1) = (( len f1) + 1) by A4, A5, FINSEQ_2: 16;

 then

 A7: ( len (n |-> m)) = ( len f1) by CARD_1:def 7;



 A8: ( len <*x*>) = 1 by FINSEQ_1: 39;

 (((n + 1) |-> m) - f) = (((n |-> m) ^ <*m*>) - (f1 ^ <*x*>)) by A5, FINSEQ_2: 60

 .= (((n |-> mm) - f1) ^ ( <*mm*> - <*x*>)) by A7, A8, A3, Th46

 .= (((n |-> m) - f1) ^ <*(m - x)*>) by RVSUM_1: 29;



 hence ( Sum (((n + 1) |-> m) - f)) = (( Sum ((n |-> m) - f1)) + (m - x)) by RVSUM_1: 74

 .= (((n * m) - ( Sum f1)) + (m - x)) by A2, A6

 .= (((n + 1) * m) - (( Sum f1) + x))

 .= (((n + 1) * m) - ( Sum f)) by A5, RVSUM_1: 74;

 end;

 hence thesis;

 end;



 A9: P[ 0 ]

 proof

 let f be FinSequence of REAL , m be Real;

 assume ( len f) = 0 ;

 then ( Sum f) = 0 by PROB_3: 62;

 hence thesis by RVSUM_1: 28, RVSUM_1: 72;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A9, A1);

 hence thesis;

 end;

 reserve X for finite set,

F for FinSequence of ( bool X);

 definition

 let X, F;

 :: original: Card

 redefine

 func Card F -> Cardinal-yielding FinSequence of NAT ;

 coherence

 proof

 ( rng ( Card F)) c= NAT

 proof

 let y be object;

 assume y in ( rng ( Card F));

 then

 consider x be object such that

 A1: x in ( dom ( Card F)) and

 A2: y = (( Card F) . x) by FUNCT_1:def 3;



 A3: x in ( dom F) by A1, CARD_3:def 2;

 then (F . x) in ( rng F) by FUNCT_1: 3;

 then

 reconsider Fx = (F . x) as finite set;

 y = ( card Fx) by A2, A3, CARD_3:def 2;

 hence thesis;

 end;

 hence thesis by FINSEQ_1:def 4;

 end;

 end

 theorem :: INT_5:48



 Th48: for f be FinSequence of ( bool X) st (for d, e st d in ( dom f) & e in ( dom f) & d <> e holds (f . d) misses (f . e)) holds ( card ( union ( rng f))) = ( Sum ( Card f))

 proof

 defpred P[ Nat] means for f be FinSequence of ( bool X) st ( len f) = $1 & (for d, e st d in ( dom f) & e in ( dom f) & d <> e holds (f . d) misses (f . e)) holds ( card ( union ( rng f))) = ( Sum ( Card f));



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 P[(n + 1)]

 proof

 let f be FinSequence of ( bool X);

 assume that

 A3: ( len f) = (n + 1) and

 A4: for d, e st d in ( dom f) & e in ( dom f) & d <> e holds (f . d) misses (f . e);



 A5: f <> {} by A3;

 then

 consider f1 be FinSequence of ( bool X), Y be Element of ( bool X) such that

 A6: f = (f1 ^ <*Y*>) by HILBERT2: 4;

 reconsider F1 = ( union ( rng f1)) as finite set;



 A7: ( union ( rng f)) = ( union (( rng f1) \/ ( rng <*Y*>))) by A6, FINSEQ_1: 31

 .= ( union (( rng f1) \/ {Y})) by FINSEQ_1: 38

 .= (F1 \/ ( union {Y})) by ZFMISC_1: 78

 .= (F1 \/ Y) by ZFMISC_1: 25;



 A8: (n + 1) = (( len f1) + 1) by A3, A6, FINSEQ_2: 16;

 F1 misses Y

 proof



 A9: (n + 1) in ( dom f) by A3, A5, FINSEQ_5: 6;

 assume F1 meets Y;

 then

 consider x be object such that

 A10: x in (F1 /\ Y) by XBOOLE_0: 4;

 x in F1 by A10, XBOOLE_0:def 4;

 then

 consider Z be set such that

 A11: x in Z and

 A12: Z in ( rng f1) by TARSKI:def 4;

 consider k be Nat such that

 A13: k in ( dom f1) and

 A14: (f1 . k) = Z by A12, FINSEQ_2: 10;

 k <= n by A8, A13, FINSEQ_3: 25;

 then

 A15: k < (n + 1) by NAT_1: 13;

 k in ( dom f) by A6, A13, FINSEQ_2: 15;

 then (f . (n + 1)) misses (f . k) by A4, A15, A9;

 then Y misses (f . k) by A6, A8, FINSEQ_1: 42;

 then

 A16: Y misses Z by A6, A13, A14, FINSEQ_1:def 7;

 x in (Y \/ Z) by A11, XBOOLE_0:def 3;

 then not x in Y by A11, A16, XBOOLE_0: 5;

 hence contradiction by A10, XBOOLE_0:def 4;

 end;

 then

 A17: (( card F1) + ( card Y)) = ( card (F1 \/ Y)) by CARD_2: 40;

 reconsider gg = <*( card Y)*> as FinSequence of NAT ;



 A18: ( Card f) = (( Card f1) ^ ( Card <*Y*>)) by A6, PRE_POLY: 25

 .= (( Card f1) ^ gg) by PRE_POLY: 24;

 for d, e st d in ( dom f1) & e in ( dom f1) & d <> e holds (f1 . d) misses (f1 . e)

 proof

 let d, e;

 assume that

 A19: d in ( dom f1) and

 A20: e in ( dom f1) and

 A21: d <> e;



 A22: (f . e) = (f1 . e) by A6, A20, FINSEQ_1:def 7;



 A23: e in ( dom f) by A6, A20, FINSEQ_2: 15;



 A24: d in ( dom f) by A6, A19, FINSEQ_2: 15;

 (f . d) = (f1 . d) by A6, A19, FINSEQ_1:def 7;

 hence thesis by A4, A21, A22, A24, A23;

 end;

 then ( card ( union ( rng f1))) = ( Sum ( Card f1)) by A2, A8;

 hence thesis by A17, A18, A7, RVSUM_1: 74;

 end;

 hence thesis;

 end;



 A25: P[ 0 ]

 proof

 let f be FinSequence of ( bool X);

 assume that

 A26: ( len f) = 0 and for d, e st d in ( dom f) & e in ( dom f) & d <> e holds (f . d) misses (f . e);



 A27: ( Card {} ) = {} ;

 f = {} by A26;

 hence thesis by A27, CARD_1: 27, RVSUM_1: 72, ZFMISC_1: 2;

 end;

 let f be FinSequence of ( bool X);

 for n be Nat holds P[n] from NAT_1:sch 2( A25, A1);

 then P[( len f)];

 hence thesis;

 end;



 Lm4: ( Sum fp) is Element of NAT ;

 reserve q for Prime;

 ::$Notion-Name

 theorem :: INT_5:49



 Th49: p > 2 & q > 2 & p <> q implies (( Lege (p,q)) * ( Lege (q,p))) = (( - 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)))

 proof

 assume that

 A1: p > 2 and

 A2: q > 2 and

 A3: p <> q;



 A4: (q,p) are_coprime by A3, INT_2: 30;

 then

 A5: (q gcd p) = 1 by INT_2:def 3;

 reconsider p, q as prime Element of NAT by ORDINAL1:def 12;

 set p9 = ((p -' 1) div 2);



 A6: p > 1 by INT_2:def 4;

 then

 A7: (p -' 1) = (p - 1) by XREAL_1: 233;

 then

 A8: (p -' 1) > 0 by A6, XREAL_1: 50;

 p is odd by A1, PEPIN: 17;

 then

 A9: (p -' 1) is even by A7, HILBERT3: 2;

 then

 A10: 2 divides (p -' 1) by PEPIN: 22;

 then

 A11: (p -' 1) = (2 * p9) by NAT_D: 3;

 then p9 divides (p -' 1);

 then p9 <= (p -' 1) by A8, NAT_D: 7;

 then

 A12: p9 < p by A7, XREAL_1: 146, XXREAL_0: 2;

 set f1 = (q * ( idseq p9));



 A13: for d st d in ( dom f1) holds (f1 . d) = (q * d)

 proof

 let d;

 assume

 A14: d in ( dom f1);

 then d in ( dom ( idseq p9)) by VALUED_1:def 5;

 then d in ( Seg ( len ( idseq p9))) by FINSEQ_1:def 3;

 then

 A15: d is Element of ( Seg p9) by CARD_1:def 7;

 (f1 . d) = (q * (( idseq p9) . d)) by A14, VALUED_1:def 5;

 hence thesis by A15;

 end;



 A16: for d be Nat st d in ( dom f1) holds (f1 . d) in NAT ;

 ( dom f1) = ( dom ( idseq p9)) by VALUED_1:def 5;

 then

 A17: ( len f1) = ( len ( idseq p9)) by FINSEQ_3: 29;

 then

 A18: ( len f1) = p9 by CARD_1:def 7;

 set q9 = ((q -' 1) div 2);

 set g1 = (p * ( idseq q9));



 A19: for d st d in ( dom g1) holds (g1 . d) = (p * d)

 proof

 let d;

 assume

 A20: d in ( dom g1);

 then d in ( dom ( idseq q9)) by VALUED_1:def 5;

 then d in ( Seg ( len ( idseq q9))) by FINSEQ_1:def 3;

 then

 A21: d is Element of ( Seg q9) by CARD_1:def 7;

 (g1 . d) = (p * (( idseq q9) . d)) by A20, VALUED_1:def 5;

 hence thesis by A21;

 end;



 A22: for d be Nat st d in ( dom g1) holds (g1 . d) in NAT ;

 ( dom g1) = ( dom ( idseq q9)) by VALUED_1:def 5;

 then ( len g1) = ( len ( idseq q9)) by FINSEQ_3: 29;

 then

 A23: ( len g1) = q9 by CARD_1:def 7;

 reconsider g1 as FinSequence of NAT by A22, FINSEQ_2: 12;

 set g3 = (g1 mod q);

 set g4 = ( Sgm ( rng g3));



 A24: ( len g3) = ( len g1) by EULER_2:def 1;

 then

 A25: ( dom g1) = ( dom g3) by FINSEQ_3: 29;

 set XX = { k where k be Element of NAT : k in ( rng g4) & k > (q / 2) };

 for x be object st x in XX holds x in ( rng g4)

 proof

 let x be object;

 assume x in XX;

 then ex k be Element of NAT st x = k & k in ( rng g4) & k > (q / 2);

 hence thesis;

 end;

 then

 A26: XX c= ( rng g4);

 reconsider f1 as FinSequence of NAT by A16, FINSEQ_2: 12;

 deffunc F( Nat) = ((f1 . $1) div p);

 consider f2 be FinSequence such that

 A27: ( len f2) = p9 & for d be Nat st d in ( dom f2) holds (f2 . d) = F(d) from FINSEQ_1:sch 2;



 A28: q > 1 by INT_2:def 4;

 then

 A29: (q -' 1) = (q - 1) by XREAL_1: 233;

 then

 A30: (q -' 1) > 0 by A28, XREAL_1: 50;

 q >= (2 + 1) by A2, NAT_1: 13;

 then (q - 1) >= (3 - 1) by XREAL_1: 9;

 then

 A31: q9 >= 1 by A29, NAT_2: 13;

 then ( len g3) >= 1 by A23, EULER_2:def 1;

 then g3 <> {} ;

 then ( rng g3) is finite non empty Subset of NAT ;

 then

 consider n2 be Element of NAT such that

 A32: ( rng g3) c= (( Seg n2) \/ { 0 }) by HEYTING3: 1;

 deffunc F( Nat) = ((g1 . $1) div q);

 consider g2 be FinSequence such that

 A33: ( len g2) = q9 & for d be Nat st d in ( dom g2) holds (g2 . d) = F(d) from FINSEQ_1:sch 2;

 for d be Nat st d in ( dom g2) holds (g2 . d) in NAT

 proof

 let d be Nat;

 assume d in ( dom g2);

 then (g2 . d) = ((g1 . d) div q) by A33;

 hence thesis;

 end;

 then

 reconsider g2 as FinSequence of NAT by FINSEQ_2: 12;



 A34: ( dom g1) = ( dom g2) by A23, A33, FINSEQ_3: 29;



 A35: for d st d in ( dom g1) holds (g1 . d) = (((g2 . d) * q) + (g3 . d))

 proof

 let d;

 assume

 A36: d in ( dom g1);

 then

 A37: (g3 . d) = ((g1 . d) mod q) by EULER_2:def 1;

 (g2 . d) = ((g1 . d) div q) by A33, A34, A36;

 hence thesis by A37, NAT_D: 2;

 end;

 q is odd by A2, PEPIN: 17;

 then

 A38: (q -' 1) is even by A29, HILBERT3: 2;

 then

 A39: 2 divides (q -' 1) by PEPIN: 22;

 then

 A40: (q -' 1) = (2 * q9) by NAT_D: 3;

 then q9 divides (q -' 1);

 then q9 <= (q -' 1) by A30, NAT_D: 7;

 then

 A41: q9 < q by A29, XREAL_1: 146, XXREAL_0: 2;

 not 0 in ( rng g3)

 proof

 assume 0 in ( rng g3);

 then

 consider a be Nat such that

 A42: a in ( dom g3) and

 A43: (g3 . a) = 0 by FINSEQ_2: 10;

 a in ( dom g1) by A24, A42, FINSEQ_3: 29;

 then

 A44: (g1 . a) = (((g2 . a) * q) + 0 ) by A35, A43;

 a in ( dom g1) by A24, A42, FINSEQ_3: 29;

 then (p * a) = ((g2 . a) * q) by A19, A44;

 then

 A45: q divides (p * a);

 a >= 1 by A42, FINSEQ_3: 25;

 then

 A46: q <= a by A4, A45, NAT_D: 7, PEPIN: 3;

 a <= q9 by A23, A24, A42, FINSEQ_3: 25;

 hence contradiction by A41, A46, XXREAL_0: 2;

 end;

 then

 A47: { 0 } misses ( rng g3) by ZFMISC_1: 50;

 then

 A48: g4 is one-to-one by A32, FINSEQ_3: 92, XBOOLE_1: 73;



 A49: for d, e st d in ( dom g1) & e in ( dom g1) & q divides ((g1 . d) - (g1 . e)) holds d = e

 proof



 A50: (q,p qua Integer) are_coprime by A3, INT_2: 30;

 let d, e;

 assume that

 A51: d in ( dom g1) and

 A52: e in ( dom g1) and

 A53: q divides ((g1 . d) - (g1 . e));



 A54: (g1 . e) = (p * e) by A19, A52;

 (g1 . d) = (p * d) by A19, A51;

 then

 A55: q divides ((d - e) * p) by A53, A54;

 now

 assume d <> e;

 then (d - e) <> 0 ;

 then |.q.| <= |.(d - e).| by A55, A50, INT_2: 25, INT_4: 6;

 then

 A56: q <= |.(d - e).| by ABSVALUE:def 1;



 A57: e >= 1 by A52, FINSEQ_3: 25;



 A58: d >= 1 by A51, FINSEQ_3: 25;

 e <= q9 by A23, A52, FINSEQ_3: 25;

 then

 A59: (d - e) >= (1 - q9) by A58, XREAL_1: 13;



 A60: (q9 - 1) < q by A41, XREAL_1: 147;

 d <= q9 by A23, A51, FINSEQ_3: 25;

 then (d - e) <= (q9 - 1) by A57, XREAL_1: 13;

 then

 A61: (d - e) < q by A60, XXREAL_0: 2;

 ( - (q9 - 1)) > ( - q) by A60, XREAL_1: 24;

 then (d - e) > ( - q) by A59, XXREAL_0: 2;

 hence contradiction by A56, A61, SEQ_2: 1;

 end;

 hence thesis;

 end;

 for x,y be object st x in ( dom g3) & y in ( dom g3) & (g3 . x) = (g3 . y) holds x = y

 proof

 let x,y be object;

 assume that

 A62: x in ( dom g3) and

 A63: y in ( dom g3) and

 A64: (g3 . x) = (g3 . y);

 reconsider x, y as Element of NAT by A62, A63;



 A65: (g1 . y) = (((g2 . y) * q) + (g3 . y)) by A25, A35, A63;

 (g1 . x) = (((g2 . x) * q) + (g3 . x)) by A25, A35, A62;

 then ((g1 . x) - (g1 . y)) = (((g2 . x) - (g2 . y)) * q) by A64, A65;

 then q divides ((g1 . x) - (g1 . y));

 hence thesis by A49, A25, A62, A63;

 end;

 then

 A66: g3 is one-to-one;

 then ( len g3) = ( card ( rng g3)) by FINSEQ_4: 62;

 then

 A67: ( len g4) = q9 by A23, A24, A32, A47, FINSEQ_3: 39, XBOOLE_1: 73;

 reconsider XX as finite Subset of NAT by A26, XBOOLE_1: 1;

 set mm = ( card XX);

 reconsider YY = (( rng g4) \ XX) as finite Subset of NAT ;



 A68: g3 is Element of ( NAT * ) by FINSEQ_1:def 11;

 ( len g3) = q9 by A23, EULER_2:def 1;

 then g3 in (q9 -tuples_on NAT ) by A68;

 then

 A69: g3 is Element of (q9 -tuples_on REAL ) by FINSEQ_2: 109, NUMBERS: 19;

 for d be Nat st d in ( dom ( idseq q9)) holds (( idseq q9) . d) in NAT ;

 then ( idseq q9) is FinSequence of NAT by FINSEQ_2: 12;

 then

 reconsider N = ( Sum ( idseq q9)) as Element of NAT by Lm4;



 A70: (2,q) are_coprime by A2, EULER_1: 2;

 ( dom (q * g2)) = ( dom g2) by VALUED_1:def 5;

 then

 A71: ( len (q * g2)) = q9 by A33, FINSEQ_3: 29;

 (q * g2) is Element of ( NAT * ) by FINSEQ_1:def 11;

 then (q * g2) in (q9 -tuples_on NAT ) by A71;

 then

 A72: (q * g2) is Element of (q9 -tuples_on REAL ) by FINSEQ_2: 109, NUMBERS: 19;



 A73: ( dom ((q * g2) + g3)) = (( dom (q * g2)) /\ ( dom g3)) by VALUED_1:def 1

 .= (( dom g2) /\ ( dom g3)) by VALUED_1:def 5

 .= ( dom g1) by A25, A34;

 for d be Nat st d in ( dom g1) holds (g1 . d) = (((q * g2) + g3) . d)

 proof

 let d be Nat;

 assume

 A74: d in ( dom g1);

 then

 A75: d in ( dom (q * g2)) by A34, VALUED_1:def 5;

 (((q * g2) + g3) . d) = (((q * g2) . d) + (g3 . d)) by A73, A74, VALUED_1:def 1;



 hence (((q * g2) + g3) . d) = ((q * (g2 . d)) + (g3 . d)) by A75, VALUED_1:def 5

 .= (g1 . d) by A35, A74;

 end;

 then g1 = ((q * g2) + g3) by A73;



 then

 A76: ( Sum g1) = (( Sum (q * g2)) + ( Sum g3)) by A72, A69, RVSUM_1: 89

 .= ((q * ( Sum g2)) + ( Sum g3)) by RVSUM_1: 87;



 A77: ( rng g3) c= ( Seg n2) by A32, A47, XBOOLE_1: 73;

 then

 A78: ( rng g4) = ( rng g3) by FINSEQ_1:def 13;

 then

 A79: XX c= ( Seg n2) by A77, A26;



 A80: ( len g3) = ( card ( rng g4)) by A66, A78, FINSEQ_4: 62;

 mm <= ( card ( rng g4)) by A26, NAT_1: 43;

 then mm <= q9 by A23, A80, EULER_2:def 1;

 then

 reconsider nn = (q9 - mm) as Element of NAT by NAT_1: 21;



 A81: g4 = ((g4 | nn) ^ (g4 /^ nn)) by RFINSEQ: 8;

 then

 A82: (g4 /^ nn) is one-to-one by A48, FINSEQ_3: 91;



 A83: q9 = (((q -' 1) + 1) div 2) by A38, NAT_2: 26

 .= (q div 2) by A28, XREAL_1: 235;



 A84: g3 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 g4 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 then

 A85: ( Sum g4) = ( Sum g3) by A66, A78, A48, RFINSEQ: 9, RFINSEQ: 26, A84;



 A86: (( rng g4) \ XX) c= ( rng g4) by XBOOLE_1: 36;

 then

 A87: YY c= ( Seg n2) by A77, A78;

 for k,l be Nat st k in YY & l in XX holds k < l

 proof

 let k,l be Nat;

 assume that

 A88: k in YY and

 A89: l in XX;



 A90: not k in XX by A88, XBOOLE_0:def 5;



 A91: ex l1 be Element of NAT st l1 = l & l1 in ( rng g4) & l1 > (q / 2) by A89;

 k in ( rng g4) by A88, XBOOLE_0:def 5;

 then k <= (q / 2) by A90;

 hence thesis by A91, XXREAL_0: 2;

 end;

 then ( Sgm (YY \/ XX)) = (( Sgm YY) ^ ( Sgm XX)) by A87, A79, FINSEQ_3: 42;

 then ( Sgm (( rng g4) \/ XX)) = (( Sgm YY) ^ ( Sgm XX)) by XBOOLE_1: 39;

 then

 A92: g4 = (( Sgm YY) ^ ( Sgm XX)) by A78, A26, XBOOLE_1: 12;

 then ( Sum g4) = (( Sum ( Sgm YY)) + ( Sum ( Sgm XX))) by RVSUM_1: 75;

 then

 A93: (p * ( Sum ( idseq q9))) = (((q * ( Sum g2)) + ( Sum ( Sgm YY))) + ( Sum ( Sgm XX))) by A76, A85, RVSUM_1: 87;



 A94: ( len ( Sgm YY)) = ( card YY) by A77, A78, A86, FINSEQ_3: 39, XBOOLE_1: 1

 .= (q9 - mm) by A23, A24, A26, A80, CARD_2: 44;

 then

 A95: (g4 /^ nn) = ( Sgm XX) by A92, FINSEQ_5: 37;

 for d be Nat st d in ( dom f2) holds (f2 . d) in NAT

 proof

 let d be Nat;

 assume d in ( dom f2);

 then (f2 . d) = ((f1 . d) div p) by A27;

 hence thesis;

 end;

 then

 reconsider f2 as FinSequence of NAT by FINSEQ_2: 12;

 set f3 = (f1 mod p);



 A96: ( len f3) = ( len f1) by EULER_2:def 1;

 then

 A97: ( dom f1) = ( dom f3) by FINSEQ_3: 29;

 set f4 = ( Sgm ( rng f3));

 p >= (2 + 1) by A1, NAT_1: 13;

 then

 A98: (p - 1) >= (3 - 1) by XREAL_1: 9;

 then f3 <> {} by A18, A7, A96, NAT_2: 13;

 then ( rng f3) is finite non empty Subset of NAT ;

 then

 consider n1 be Element of NAT such that

 A99: ( rng f3) c= (( Seg n1) \/ { 0 }) by HEYTING3: 1;



 A100: ( dom f1) = ( dom f2) by A18, A27, FINSEQ_3: 29;



 A101: for d st d in ( dom f1) holds (f1 . d) = (((f2 . d) * p) + (f3 . d))

 proof

 let d;

 assume

 A102: d in ( dom f1);

 then

 A103: (f3 . d) = ((f1 . d) mod p) by EULER_2:def 1;

 (f2 . d) = ((f1 . d) div p) by A27, A100, A102;

 hence thesis by A103, NAT_D: 2;

 end;

 not 0 in ( rng f3)

 proof

 assume 0 in ( rng f3);

 then

 consider a be Nat such that

 A104: a in ( dom f3) and

 A105: (f3 . a) = 0 by FINSEQ_2: 10;

 (f1 . a) = (((f2 . a) * p) + 0 ) by A97, A101, A104, A105;

 then (q * a) = ((f2 . a) * p) by A13, A97, A104;

 then

 A106: p divides (q * a);

 a >= 1 by A104, FINSEQ_3: 25;

 then

 A107: p <= a by A4, A106, NAT_D: 7, PEPIN: 3;

 a <= p9 by A18, A96, A104, FINSEQ_3: 25;

 hence contradiction by A12, A107, XXREAL_0: 2;

 end;

 then

 A108: { 0 } misses ( rng f3) by ZFMISC_1: 50;

 then

 A109: f4 is one-to-one by A99, FINSEQ_3: 92, XBOOLE_1: 73;



 A110: for d, e st d in ( dom f1) & e in ( dom f1) & p divides ((f1 . d) - (f1 . e)) holds d = e

 proof



 A111: (q,p qua Integer) are_coprime by A3, INT_2: 30;

 let d, e;

 assume that

 A112: d in ( dom f1) and

 A113: e in ( dom f1) and

 A114: p divides ((f1 . d) - (f1 . e));



 A115: (f1 . e) = (q * e) by A13, A113;

 (f1 . d) = (q * d) by A13, A112;

 then

 A116: p divides ((d - e) * q) by A114, A115;

 now

 assume d <> e;

 then (d - e) <> 0 ;

 then |.p.| <= |.(d - e).| by A116, A111, INT_2: 25, INT_4: 6;

 then

 A117: p <= |.(d - e).| by ABSVALUE:def 1;



 A118: e >= 1 by A113, FINSEQ_3: 25;



 A119: d >= 1 by A112, FINSEQ_3: 25;

 e <= p9 by A18, A113, FINSEQ_3: 25;

 then

 A120: (d - e) >= (1 - p9) by A119, XREAL_1: 13;



 A121: (p9 - 1) < p by A12, XREAL_1: 147;

 d <= p9 by A18, A112, FINSEQ_3: 25;

 then (d - e) <= (p9 - 1) by A118, XREAL_1: 13;

 then

 A122: (d - e) ( - p) by A121, XREAL_1: 24;

 then (d - e) > ( - p) by A120, XXREAL_0: 2;

 hence contradiction by A117, A122, SEQ_2: 1;

 end;

 hence thesis;

 end;

 for x,y be object st x in ( dom f3) & y in ( dom f3) & (f3 . x) = (f3 . y) holds x = y

 proof

 let x,y be object;

 assume that

 A123: x in ( dom f3) and

 A124: y in ( dom f3) and

 A125: (f3 . x) = (f3 . y);

 reconsider x, y as Element of NAT by A123, A124;



 A126: (f1 . y) = (((f2 . y) * p) + (f3 . y)) by A97, A101, A124;

 (f1 . x) = (((f2 . x) * p) + (f3 . x)) by A97, A101, A123;

 then ((f1 . x) - (f1 . y)) = (((f2 . x) - (f2 . y)) * p) by A125, A126;

 then p divides ((f1 . x) - (f1 . y));

 hence thesis by A110, A97, A123, A124;

 end;

 then

 A127: f3 is one-to-one;

 then ( len f3) = ( card ( rng f3)) by FINSEQ_4: 62;

 then

 A128: ( len f4) = p9 by A18, A96, A99, A108, FINSEQ_3: 39, XBOOLE_1: 73;



 A129: (g4 | nn) = ( Sgm YY) by A92, A94, FINSEQ_3: 113, FINSEQ_6: 10;



 A130: (g4 | nn) is one-to-one by A48, A81, FINSEQ_3: 91;



 A131: ( Lege (p,q)) = (( - 1) |^ ( Sum g2))

 proof

 set g5 = ((mm |-> q) - (g4 /^ nn));

 set g6 = ((g4 | nn) ^ g5);



 A132: (g4 /^ nn) is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A133: ( len (g4 | nn)) = nn by A67, FINSEQ_1: 59, XREAL_1: 43;



 A134: ( len (g4 /^ nn)) = (( len g4) -' nn) by RFINSEQ: 29

 .= (( len g4) - nn) by A67, XREAL_1: 43, XREAL_1: 233

 .= mm by A67;



 A135: ( dom g5) = (( dom (mm |-> q)) /\ ( dom (g4 /^ nn))) by VALUED_1: 12

 .= (( Seg ( len (mm |-> q))) /\ ( dom (g4 /^ nn))) by FINSEQ_1:def 3

 .= (( dom (g4 /^ nn)) /\ ( dom (g4 /^ nn))) by FINSEQ_1:def 3, A134, CARD_1:def 7

 .= ( dom (g4 /^ nn));

 then

 A136: ( len g5) = ( len (g4 /^ nn)) by FINSEQ_3: 29;



 A137: for d st d in ( dom g5) holds (g5 . d) = (q - ((g4 /^ nn) . d))

 proof

 let d;

 assume

 A138: d in ( dom g5);

 then d in ( Seg mm) by A134, A135, FINSEQ_1:def 3;

 then ((mm |-> q) . d) = q by FINSEQ_2: 57;

 hence thesis by A138, VALUED_1: 13;

 end;



 A139: for d st d in ( dom g5) holds (g5 . d) > 0 & (g5 . d) <= q9

 proof

 let d;

 reconsider w = (g5 . d) as Element of INT by INT_1:def 2;

 assume

 A140: d in ( dom g5);

 then (( Sgm XX) . d) in ( rng ( Sgm XX)) by A95, A135, FUNCT_1: 3;

 then (( Sgm XX) . d) in XX by A79, FINSEQ_1:def 13;

 then

 A141: ex ll be Element of NAT st ll = (( Sgm XX) . d) & ll in ( rng g3) & ll > (q / 2) by A78;

 then

 consider e be Nat such that

 A142: e in ( dom g3) and

 A143: (g3 . e) = ((g4 /^ nn) . d) by A95, FINSEQ_2: 10;

 ((g4 /^ nn) . d) = ((g1 . e) mod q) by A25, A142, A143, EULER_2:def 1;

 then

 A144: ((g4 /^ nn) . d) < q by NAT_D: 1;



 A145: (g5 . d) = (q - ((g4 /^ nn) . d)) by A137, A140;

 then w < (q - (q / 2)) by A95, A141, XREAL_1: 10;

 hence thesis by A83, A145, A144, INT_1: 54, XREAL_1: 50;

 end;



 A146: ( rng g5) c= INT by RELAT_1:def 19;

 for d be Nat st d in ( dom g5) holds (g5 . d) in NAT

 proof

 let d be Nat;

 assume

 A147: d in ( dom g5);

 (g5 . d) > 0 by A139, A147;

 hence thesis by A146, INT_1: 3;

 end;

 then

 reconsider g5 as FinSequence of NAT by FINSEQ_2: 12;

 g5 is FinSequence of NAT ;

 then

 reconsider g6 as FinSequence of NAT by FINSEQ_1: 75;



 A148: g6 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A149: nn <= ( len g4) by A67, XREAL_1: 43;



 A150: ( rng (g4 | nn)) misses ( rng g5)

 proof

 assume not ( rng (g4 | nn)) misses ( rng g5);

 then

 consider x be object such that

 A151: x in ( rng (g4 | nn)) and

 A152: x in ( rng g5) by XBOOLE_0: 3;

 consider e be Nat such that

 A153: e in ( dom g5) and

 A154: (g5 . e) = x by A152, FINSEQ_2: 10;

 x = (q - ((g4 /^ nn) . e)) by A137, A153, A154;

 then

 A155: x = (q - (g4 . (e + nn))) by A149, A135, A153, RFINSEQ:def 1;

 (e + nn) in ( dom g4) by A135, A153, FINSEQ_5: 26;

 then

 consider e1 be Nat such that

 A156: e1 in ( dom g3) and

 A157: (g3 . e1) = (g4 . (e + nn)) by A78, FINSEQ_2: 10, FUNCT_1: 3;



 A158: e1 <= q9 by A23, A24, A156, FINSEQ_3: 25;

 ( rng (g4 | nn)) c= ( rng g4) by FINSEQ_5: 19;

 then

 consider d1 be Nat such that

 A159: d1 in ( dom g3) and

 A160: (g3 . d1) = x by A78, A151, FINSEQ_2: 10;

 d1 <= q9 by A23, A24, A159, FINSEQ_3: 25;

 then (d1 + e1) <= (q9 + q9) by A158, XREAL_1: 7;

 then

 A161: (d1 + e1) < q by A29, A40, XREAL_1: 146, XXREAL_0: 2;



 A162: e1 in ( dom g1) by A24, A156, FINSEQ_3: 29;

 then

 A163: (g4 . (e + nn)) = ((g1 . e1) mod q) by A157, EULER_2:def 1;



 A164: d1 in ( dom g1) by A24, A159, FINSEQ_3: 29;

 then x = ((g1 . d1) mod q) by A160, EULER_2:def 1;

 then ((((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q) = 0 by A155, A163, NAT_D: 25;

 then (((g1 . d1) + (g1 . e1)) mod q) = 0 by EULER_2: 6;

 then q divides ((g1 . d1) + (g1 . e1)) by PEPIN: 6;

 then q divides ((d1 * p) + (g1 . e1)) by A19, A164;

 then q divides ((d1 * p) + (e1 * p)) by A19, A162;

 then

 A165: q divides ((d1 + e1) * p);

 d1 >= 1 by A159, FINSEQ_3: 25;

 hence contradiction by A4, A165, A161, NAT_D: 7, PEPIN: 3;

 end;

 for d,e be Nat st 1 <= d & d < e & e <= ( len g5) holds (g5 . d) <> (g5 . e)

 proof

 let d,e be Nat;

 assume that

 A166: 1 <= d and

 A167: d < e and

 A168: e <= ( len g5);

 1 <= e by A166, A167, XXREAL_0: 2;

 then

 A169: e in ( dom g5) by A168, FINSEQ_3: 25;

 then

 A170: (g5 . e) = (q - ((g4 /^ nn) . e)) by A137;

 d < ( len g5) by A167, A168, XXREAL_0: 2;

 then

 A171: d in ( dom g5) by A166, FINSEQ_3: 25;

 then (g5 . d) = (q - ((g4 /^ nn) . d)) by A137;

 hence thesis by A82, A135, A167, A171, A169, A170;

 end;

 then ( len g5) = ( card ( rng g5)) by GRAPH_5: 7;

 then g5 is one-to-one by FINSEQ_4: 62;

 then

 A172: g6 is one-to-one by A130, A150, FINSEQ_3: 91;



 A173: for d st d in ( dom g6) holds (g6 . d) > 0 & (g6 . d) <= q9

 proof

 let d;

 assume

 A174: d in ( dom g6);

 per cases by A174, FINSEQ_1: 25;

 suppose

 A175: d in ( dom (g4 | nn));

 then ((g4 | nn) . d) in ( rng ( Sgm YY)) by A129, FUNCT_1: 3;

 then

 A176: ((g4 | nn) . d) in YY by A87, FINSEQ_1:def 13;

 then

 A177: ((g4 | nn) . d) in ( rng g4) by XBOOLE_0:def 5;

 not ((g4 | nn) . d) in XX by A176, XBOOLE_0:def 5;

 then ((g4 | nn) . d) <= (q / 2) by A177;

 then

 A178: ((g4 | nn) . d) <= q9 by A83, INT_1: 54;

 not ((g4 | nn) . d) in { 0 } by A47, A78, A177, XBOOLE_0: 3;

 then ((g4 | nn) . d) <> 0 by TARSKI:def 1;

 hence thesis by A175, A178, FINSEQ_1:def 7;

 end;

 suppose ex l be Nat st l in ( dom g5) & d = (( len (g4 | nn)) + l);

 then

 consider l be Element of NAT such that

 A179: l in ( dom g5) and

 A180: d = (( len (g4 | nn)) + l);

 (g6 . d) = (g5 . l) by A179, A180, FINSEQ_1:def 7;

 hence thesis by A139, A179;

 end;

 end;



 A181: ( idseq q9) is FinSequence of REAL by RVSUM_1: 145;

 ( len g6) = (( len (g4 | nn)) + ( len g5)) by FINSEQ_1: 22

 .= q9 by A133, A134, A136;

 then ( rng g6) = ( rng ( idseq q9)) by A172, A173, Th40;



 then N = ( Sum g6) by A172, A148, A181, RFINSEQ: 9, RFINSEQ: 26

 .= (( Sum (g4 | nn)) + ( Sum g5)) by RVSUM_1: 75

 .= (( Sum (g4 | nn)) + ((mm * q) - ( Sum (g4 /^ nn)))) by A134, A132, Th47

 .= ((( Sum (g4 | nn)) + (mm * q)) - ( Sum (g4 /^ nn)));

 then ((p - 1) * N) = (((q * ( Sum g2)) + (2 * ( Sum ( Sgm XX)))) - (mm * q)) by A93, A95, A129;



 then

 A182: (((p -' 1) * N) mod 2) = ((((q * ( Sum g2)) - (mm * q)) + (2 * ( Sum ( Sgm XX)))) mod 2) by A6, XREAL_1: 233

 .= (((q * ( Sum g2)) - (mm * q)) mod 2) by EULER_1: 12;

 2 divides ((p -' 1) * N) by A10, NAT_D: 9;

 then ((q * (( Sum g2) - mm)) mod 2) = 0 by A182, PEPIN: 6;

 then 2 divides (q * (( Sum g2) - mm)) by Lm1;

 then 2 divides (( Sum g2) - mm) by A70, INT_2: 25;

 then (( Sum g2),mm) are_congruent_mod 2;

 then (( Sum g2) mod 2) = (mm mod 2) by NAT_D: 64;

 then (( - 1) |^ ( Sum g2)) = (( - 1) |^ mm) by Th45;

 hence thesis by A2, A5, A78, Th41;

 end;

 for d be Nat st d in ( dom ( idseq p9)) holds (( idseq p9) . d) in NAT ;

 then ( idseq p9) is FinSequence of NAT by FINSEQ_2: 12;

 then

 reconsider M = ( Sum ( idseq p9)) as Element of NAT by Lm4;



 A183: (2,p) are_coprime by A1, EULER_1: 2;

 set X = { k where k be Element of NAT : k in ( rng f4) & k > (p / 2) };

 for x be object st x in X holds x in ( rng f4)

 proof

 let x be object;

 assume x in X;

 then ex k be Element of NAT st x = k & k in ( rng f4) & k > (p / 2);

 hence thesis;

 end;

 then

 A184: X c= ( rng f4);



 A185: p9 >= 1 by A7, A98, NAT_2: 13;



 A186: (( Sum f2) + ( Sum g2)) = (p9 * q9)

 proof

 reconsider A = ( Seg p9), B = ( Seg q9) as non empty finite Subset of NAT by A185, A31;

 deffunc F( Element of A, Element of B) = (($1 / p) - ($2 / q));



 A187: for x be Element of A, y be Element of B holds F(x,y) in REAL by XREAL_0:def 1;

 consider z be Function of [:A, B:], REAL such that

 A188: for x be Element of A, y be Element of B holds (z . (x,y)) = F(x,y) from FUNCT_7:sch 1( A187);

 defpred G[ set, set] means ex x be Element of A st $1 = x & $2 = { [x, y] where y be Element of B : (z . (x,y)) > 0 };



 A189: for d be Nat st d in ( Seg p9) holds ex x1 be Element of ( bool ( dom z)) st G[d, x1]

 proof

 let d be Nat;

 assume d in ( Seg p9);

 then

 reconsider d as Element of A;

 take x1 = { [d, y] where y be Element of B : (z . (d,y)) > 0 };

 x1 c= ( dom z)

 proof

 let l be object;

 assume l in x1;

 then ex yy be Element of B st [d, yy] = l & (z . (d,yy)) > 0 ;

 then l in [:A, B:];

 hence thesis by FUNCT_2:def 1;

 end;

 hence thesis;

 end;

 consider Pr be FinSequence of ( bool ( dom z)) such that

 A190: ( dom Pr) = ( Seg p9) & for d be Nat st d in ( Seg p9) holds G[d, (Pr . d)] from FINSEQ_1:sch 5( A189);



 A191: ( dom ( Card Pr)) = ( dom Pr) by CARD_3:def 2

 .= ( dom f2) by A27, A190, FINSEQ_1:def 3;

 for d be Nat st d in ( dom ( Card Pr)) holds (( Card Pr) . d) = (f2 . d)

 proof

 let d be Nat;

 assume

 A192: d in ( dom ( Card Pr));

 then d in ( Seg p9) by A27, A191, FINSEQ_1:def 3;

 then

 consider m be Element of A such that

 A193: m = d and

 A194: (Pr . d) = { [m, y] where y be Element of B : (z . (m,y)) > 0 } by A190;

 (Pr . d) = [: {m}, ( Seg (f2 . m)):]

 proof

 set L = [: {m}, ( Seg (f2 . m)):];



 A195: L c= (Pr . d)

 proof

 now

 assume (q mod p) = 0 ;

 then

 A196: p divides q by PEPIN: 6;

 then p <= q by NAT_D: 7;

 then p < q by A3, XXREAL_0: 1;

 hence contradiction by A6, A196, NAT_4: 12;

 end;

 then

 A197: ( - (q div p)) = ((( - q) div p) + 1) by WSIERP_1: 41;

 2 divides ((p -' 1) * q) by A10, NAT_D: 9;

 then (((p -' 1) * q) mod 2) = 0 by PEPIN: 6;

 then (((p -' 1) * q) div 2) = (((p -' 1) * q) / 2) by REAL_3: 4;



 then

 A198: ((p9 * q) div p) = (((p - 1) * q) div (2 * p)) by A7, A11, NAT_2: 27

 .= ((((p * q) - q) div p) div 2) by PRE_FF: 5

 .= ((q + (( - (q div p)) - 1)) div 2) by A197, NAT_D: 61

 .= (((2 * q9) + ( - (q div p))) div 2) by A29, A40

 .= (q9 + (( - (q div p)) div 2)) by NAT_D: 61;



 A199: ((p9 * q) div p) <= q9

 proof

 per cases ;

 suppose ((q div p) mod 2) = 0 ;



 then (( - (q div p)) div 2) = ( - ((q div p) div 2)) by WSIERP_1: 42

 .= ( - (q div (2 * p))) by NAT_2: 27;

 then ((p9 * q) div p) = (q9 - (q div (2 * p))) by A198;

 hence thesis by XREAL_1: 43;

 end;

 suppose ((q div p) mod 2) <> 0 ;

 then ( - ((q div p) div 2)) = ((( - (q div p)) div 2) + 1) by WSIERP_1: 41;



 then (( - (q div p)) div 2) = (( - ((q div p) div 2)) - 1)

 .= (( - (q div (2 * p))) - 1) by NAT_2: 27;

 then ((p9 * q) div p) = (q9 - ((q div (2 * p)) + 1)) by A198;

 hence thesis by XREAL_1: 43;

 end;

 end;

 m <= p9 by FINSEQ_1: 1;

 then (m * q) <= (p9 * q) by XREAL_1: 64;

 then ((m * q) div p) <= ((p9 * q) div p) by NAT_2: 24;

 then

 A200: ((m * q) div p) <= q9 by A199, XXREAL_0: 2;

 m in ( Seg p9);

 then

 A201: m in ( dom f1) by A18, FINSEQ_1:def 3;



 then

 A202: (f2 . m) = ((f1 . m) div p) by A27, A100

 .= ((m * q) div p) by A13, A201;

 now

 assume ((m * q) / p) is integer;

 then

 A203: p divides (m * q) by WSIERP_1: 17;



 A204: m <= p9 by FINSEQ_1: 1;

 ( 0 + 1) <= m by FINSEQ_1: 1;

 then p <= m by A5, A203, NAT_D: 7, WSIERP_1: 30;

 hence contradiction by A12, A204, XXREAL_0: 2;

 end;

 then

 A205: [\((m * q) / p)/] < ((m * q) / p) by INT_1: 26;

 let l be object;

 assume l in L;

 then

 consider x,y be object such that

 A206: x in {m} and

 A207: y in ( Seg (f2 . m)) and

 A208: l = [x, y] by ZFMISC_1:def 2;

 reconsider y as Element of NAT by A207;



 A209: 1 <= y by A207, FINSEQ_1: 1;

 y <= (f2 . m) by A207, FINSEQ_1: 1;

 then y <= q9 by A200, A202, XXREAL_0: 2;

 then

 reconsider y as Element of B by A209, FINSEQ_1: 1;

 y <= [\((m * q) / p)/] by A207, A202, FINSEQ_1: 1;

 then y < ((m * q) / p) by A205, XXREAL_0: 2;

 then (y * p) < (((m * q) / p) * p) by XREAL_1: 68;

 then (y * p) < (m * q) by XCMPLX_1: 87;

 then (y / q) < (m / p) by XREAL_1: 106;

 then ((m / p) - (y / q)) > 0 by XREAL_1: 50;

 then (z . (m,y)) > 0 by A188;

 then [m, y] in (Pr . d) by A194;

 hence thesis by A206, A208, TARSKI:def 1;

 end;

 (Pr . d) c= L

 proof

 let l be object;



 A210: m in {m} by TARSKI:def 1;

 m in ( Seg p9);

 then

 A211: m in ( dom f1) by A18, FINSEQ_1:def 3;

 assume l in (Pr . d);

 then

 consider y1 be Element of B such that

 A212: l = [m, y1] and

 A213: (z . (m,y1)) > 0 by A194;

 ((m / p) - (y1 / q)) > 0 by A188, A213;

 then (((m / p) - (y1 / q)) + (y1 / q)) > ( 0 + (y1 / q)) by XREAL_1: 6;

 then ((m / p) * q) > ((y1 / q) * q) by XREAL_1: 68;

 then ((m * q) / p) > y1 by XCMPLX_1: 87;

 then ((m * q) div p) >= y1 by INT_1: 54;

 then ((f1 . m) div p) >= y1 by A13, A211;

 then

 A214: y1 <= (f2 . m) by A27, A100, A211;

 y1 >= 1 by FINSEQ_1: 1;

 then y1 in ( Seg (f2 . m)) by A214, FINSEQ_1: 1;

 hence thesis by A212, A210, ZFMISC_1:def 2;

 end;

 hence thesis by A195, XBOOLE_0:def 10;

 end;



 then ( card (Pr . d)) = ( card [:( Seg (f2 . m)), {m}:]) by CARD_2: 4

 .= ( card ( Seg (f2 . m))) by CARD_1: 69;



 then

 A215: ( card (Pr . d)) = ( card (f2 . d)) by A193, FINSEQ_1: 55

 .= (f2 . d);

 d in ( dom Pr) by A192, CARD_3:def 2;

 hence thesis by A215, CARD_3:def 2;

 end;

 then

 A216: ( Card Pr) = f2 by A191;

 defpred K[ set, set] means ex y be Element of B st $1 = y & $2 = { [x, y] where x be Element of A : (z . (x,y)) < 0 };



 A217: for d be Nat st d in ( Seg q9) holds ex x1 be Element of ( bool ( dom z)) st K[d, x1]

 proof

 let d be Nat;

 assume d in ( Seg q9);

 then

 reconsider d as Element of B;

 take x1 = { [x, d] where x be Element of A : (z . (x,d)) < 0 };

 x1 c= ( dom z)

 proof

 let l be object;

 assume l in x1;

 then ex xx be Element of A st [xx, d] = l & (z . (xx,d)) < 0 ;

 then l in [:A, B:];

 hence thesis by FUNCT_2:def 1;

 end;

 hence thesis;

 end;

 consider Pk be FinSequence of ( bool ( dom z)) such that

 A218: ( dom Pk) = ( Seg q9) & for d be Nat st d in ( Seg q9) holds K[d, (Pk . d)] from FINSEQ_1:sch 5( A217);



 A219: ( dom ( Card Pk)) = ( Seg ( len g2)) by A33, A218, CARD_3:def 2

 .= ( dom g2) by FINSEQ_1:def 3;



 A220: for d be Nat st d in ( dom ( Card Pk)) holds (( Card Pk) . d) = (g2 . d)

 proof

 let d be Nat;

 assume

 A221: d in ( dom ( Card Pk));

 then d in ( Seg q9) by A33, A219, FINSEQ_1:def 3;

 then

 consider n be Element of B such that

 A222: n = d and

 A223: (Pk . d) = { [x, n] where x be Element of A : (z . (x,n)) < 0 } by A218;

 (Pk . d) = [:( Seg (g2 . n)), {n}:]

 proof

 set L = [:( Seg (g2 . n)), {n}:];



 A224: L c= (Pk . d)

 proof

 now

 assume (p mod q) = 0 ;

 then

 A225: q divides p by PEPIN: 6;

 then q <= p by NAT_D: 7;

 then q < p by A3, XXREAL_0: 1;

 hence contradiction by A28, A225, NAT_4: 12;

 end;

 then

 A226: ( - (p div q)) = ((( - p) div q) + 1) by WSIERP_1: 41;

 2 divides ((q -' 1) * p) by A39, NAT_D: 9;

 then (((q -' 1) * p) mod 2) = 0 by PEPIN: 6;

 then (((q -' 1) * p) div 2) = (((q -' 1) * p) / 2) by REAL_3: 4;



 then

 A227: ((q9 * p) div q) = (((q - 1) * p) div (2 * q)) by A29, A40, NAT_2: 27

 .= ((((q * p) - p) div q) div 2) by PRE_FF: 5

 .= ((p + (( - (p div q)) - 1)) div 2) by A226, NAT_D: 61

 .= (((2 * p9) - (p div q)) div 2) by A7, A11

 .= (p9 + (( - (p div q)) div 2)) by NAT_D: 61;



 A228: ((q9 * p) div q) <= p9

 proof

 per cases ;

 suppose ((p div q) mod 2) = 0 ;



 then (( - (p div q)) div 2) = ( - ((p div q) div 2)) by WSIERP_1: 42

 .= ( - (p div (2 * q))) by NAT_2: 27;

 then ((q9 * p) div q) = (p9 - (p div (2 * q))) by A227;

 hence thesis by XREAL_1: 43;

 end;

 suppose ((p div q) mod 2) <> 0 ;

 then ( - ((p div q) div 2)) = ((( - (p div q)) div 2) + 1) by WSIERP_1: 41;



 then (( - (p div q)) div 2) = (( - ((p div q) div 2)) - 1)

 .= (( - (p div (2 * q))) - 1) by NAT_2: 27;

 then ((q9 * p) div q) = (p9 - ((p div (2 * q)) + 1)) by A227;

 hence thesis by XREAL_1: 43;

 end;

 end;

 n in ( Seg q9);

 then

 A229: n in ( dom g1) by A23, FINSEQ_1:def 3;



 then

 A230: (g2 . n) = ((g1 . n) div q) by A33, A34

 .= ((n * p) div q) by A19, A229;

 let l be object;

 assume l in L;

 then

 consider x,y be object such that

 A231: x in ( Seg (g2 . n)) and

 A232: y in {n} and

 A233: l = [x, y] by ZFMISC_1:def 2;

 reconsider x as Element of NAT by A231;



 A234: x <= (g2 . n) by A231, FINSEQ_1: 1;

 n <= q9 by FINSEQ_1: 1;

 then (n * p) <= (q9 * p) by XREAL_1: 64;

 then ((n * p) div q) <= ((q9 * p) div q) by NAT_2: 24;

 then ((n * p) div q) <= p9 by A228, XXREAL_0: 2;

 then

 A235: x <= p9 by A230, A234, XXREAL_0: 2;

 1 <= x by A231, FINSEQ_1: 1;

 then

 reconsider x as Element of A by A235, FINSEQ_1: 1;

 now

 assume ((n * p) / q) is integer;

 then

 A236: q divides (n * p) by WSIERP_1: 17;



 A237: n <= q9 by FINSEQ_1: 1;

 ( 0 + 1) <= n by FINSEQ_1: 1;

 then q <= n by A5, A236, NAT_D: 7, WSIERP_1: 30;

 hence contradiction by A41, A237, XXREAL_0: 2;

 end;

 then [\((n * p) / q)/] < ((n * p) / q) by INT_1: 26;

 then x < ((n * p) / q) by A230, A234, XXREAL_0: 2;

 then (x * q) < (((n * p) / q) * q) by XREAL_1: 68;

 then (x * q) < (n * p) by XCMPLX_1: 87;

 then ((x / p) - (n / q)) < 0 by XREAL_1: 49, XREAL_1: 106;

 then (z . (x,n)) < 0 by A188;

 then [x, n] in (Pk . d) by A223;

 hence thesis by A232, A233, TARSKI:def 1;

 end;

 (Pk . d) c= L

 proof

 let l be object;



 A238: n in {n} by TARSKI:def 1;

 n in ( Seg q9);

 then

 A239: n in ( dom g1) by A23, FINSEQ_1:def 3;

 assume l in (Pk . d);

 then

 consider x be Element of A such that

 A240: l = [x, n] and

 A241: (z . (x,n)) < 0 by A223;

 ((x / p) - (n / q)) < 0 by A188, A241;

 then (((x / p) - (n / q)) + (n / q)) < ( 0 + (n / q)) by XREAL_1: 6;

 then ((x / p) * p) < ((n / q) * p) by XREAL_1: 68;

 then x < ((n * p) / q) by XCMPLX_1: 87;

 then x <= ((n * p) div q) by INT_1: 54;

 then ((g1 . n) div q) >= x by A19, A239;

 then

 A242: x <= (g2 . n) by A33, A34, A239;

 x >= 1 by FINSEQ_1: 1;

 then x in ( Seg (g2 . n)) by A242, FINSEQ_1: 1;

 hence thesis by A240, A238, ZFMISC_1:def 2;

 end;

 hence thesis by A224, XBOOLE_0:def 10;

 end;

 then ( card (Pk . d)) = ( card ( Seg (g2 . n))) by CARD_1: 69;



 then

 A243: ( card (Pk . d)) = ( card (g2 . d)) by A222, FINSEQ_1: 55

 .= (g2 . d);

 d in ( dom Pk) by A221, CARD_3:def 2;

 hence thesis by A243, CARD_3:def 2;

 end;

 reconsider U1 = ( union ( rng Pr)), U2 = ( union ( rng Pk)) as finite Subset of ( dom z) by PROB_3: 48;

 ( dom z) c= (U1 \/ U2)

 proof

 let l be object;

 assume l in ( dom z);

 then

 consider x,y be object such that

 A244: x in A and

 A245: y in B and

 A246: l = [x, y] by ZFMISC_1:def 2;

 reconsider y as Element of B by A245;

 reconsider x as Element of A by A244;



 A247: (z . (x,y)) <> 0

 proof

 assume (z . (x,y)) = 0 ;

 then ((x / p) - (y / q)) = 0 by A188;

 then (x * q) = (y * p) by XCMPLX_1: 95;

 then

 A248: p divides (x * q);



 A249: x <= p9 by FINSEQ_1: 1;

 x >= ( 0 + 1) by FINSEQ_1: 1;

 then p <= x by A5, A248, NAT_D: 7, WSIERP_1: 30;

 hence contradiction by A12, A249, XXREAL_0: 2;

 end;

 per cases by A247;

 suppose

 A250: (z . (x,y)) > 0 ;

 G[x, (Pr . x)] by A190;

 then l in (Pr . x) by A246, A250;

 then l in ( Union Pr) by A190, PROB_3: 49;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose

 A251: (z . (x,y)) < 0 ;

 K[y, (Pk . y)] by A218;

 then l in (Pk . y) by A246, A251;

 then l in ( Union Pk) by A218, PROB_3: 49;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 then

 A252: (U1 \/ U2) = ( dom z) by XBOOLE_0:def 10;



 A253: U1 misses U2

 proof

 assume U1 meets U2;

 then

 consider l be object such that

 A254: l in U1 and

 A255: l in U2 by XBOOLE_0: 3;

 l in ( Union Pk) by A255;

 then

 consider k2 be Nat such that

 A256: k2 in ( dom Pk) and

 A257: l in (Pk . k2) by PROB_3: 49;

 l in ( Union Pr) by A254;

 then

 consider k1 be Nat such that

 A258: k1 in ( dom Pr) and

 A259: l in (Pr . k1) by PROB_3: 49;

 reconsider k1, k2 as Element of NAT by ORDINAL1:def 12;

 consider n1 be Element of B such that n1 = k2 and

 A260: (Pk . k2) = { [x, n1] where x be Element of A : (z . (x,n1)) < 0 } by A218, A256;

 consider n2 be Element of A such that

 A261: l = [n2, n1] and

 A262: (z . (n2,n1)) < 0 by A257, A260;

 consider m1 be Element of A such that m1 = k1 and

 A263: (Pr . k1) = { [m1, y] where y be Element of B : (z . (m1,y)) > 0 } by A190, A258;



 A264: ex m2 be Element of B st l = [m1, m2] & (z . (m1,m2)) > 0 by A259, A263;

 then m1 = n2 by A261, XTUPLE_0: 1;

 hence contradiction by A264, A261, A262, XTUPLE_0: 1;

 end;



 A265: for d, e st d in ( dom Pk) & e in ( dom Pk) & d <> e holds (Pk . d) misses (Pk . e)

 proof

 let d, e;

 assume that

 A266: d in ( dom Pk) and

 A267: e in ( dom Pk) and

 A268: d <> e;

 consider y2 be Element of B such that

 A269: y2 = e and

 A270: (Pk . e) = { [x, y2] where x be Element of A : (z . (x,y2)) < 0 } by A218, A267;

 consider y1 be Element of B such that

 A271: y1 = d and

 A272: (Pk . d) = { [x, y1] where x be Element of A : (z . (x,y1)) < 0 } by A218, A266;

 now

 assume not (Pk . d) misses (Pk . e);

 then

 consider l be object such that

 A273: l in (Pk . d) and

 A274: l in (Pk . e) by XBOOLE_0: 3;



 A275: ex x2 be Element of A st l = [x2, y2] & (z . (x2,y2)) < 0 by A270, A274;

 ex x1 be Element of A st l = [x1, y1] & (z . (x1,y1)) < 0 by A272, A273;

 hence contradiction by A268, A271, A269, A275, XTUPLE_0: 1;

 end;

 hence thesis;

 end;



 A276: ( card ( union ( rng Pk))) = ( Sum ( Card Pk)) by A265, Th48;



 A277: for d, e st d in ( dom Pr) & e in ( dom Pr) & d <> e holds (Pr . d) misses (Pr . e)

 proof

 let d, e;

 assume that

 A278: d in ( dom Pr) and

 A279: e in ( dom Pr) and

 A280: d <> e;

 consider x2 be Element of A such that

 A281: x2 = e and

 A282: (Pr . e) = { [x2, y] where y be Element of B : (z . (x2,y)) > 0 } by A190, A279;

 consider x1 be Element of A such that

 A283: x1 = d and

 A284: (Pr . d) = { [x1, y] where y be Element of B : (z . (x1,y)) > 0 } by A190, A278;

 now

 assume not (Pr . d) misses (Pr . e);

 then

 consider l be object such that

 A285: l in (Pr . d) and

 A286: l in (Pr . e) by XBOOLE_0: 3;



 A287: ex y2 be Element of B st l = [x2, y2] & (z . (x2,y2)) > 0 by A282, A286;

 ex y1 be Element of B st l = [x1, y1] & (z . (x1,y1)) > 0 by A284, A285;

 hence contradiction by A280, A283, A281, A287, XTUPLE_0: 1;

 end;

 hence thesis;

 end;

 ( card ( union ( rng Pr))) = ( Sum ( Card Pr)) by A277, Th48;

 then ( card (U1 \/ U2)) = (( Sum ( Card Pr)) + ( Sum ( Card Pk))) by A276, A253, CARD_2: 40;



 then (( Sum ( Card Pr)) + ( Sum ( Card Pk))) = ( card [:A, B:]) by A252, FUNCT_2:def 1

 .= (( card A) * ( card B)) by CARD_2: 46

 .= (p9 * ( card B)) by FINSEQ_1: 57

 .= (p9 * q9) by FINSEQ_1: 57;

 hence thesis by A216, A219, A220, FINSEQ_1: 13;

 end;

 ( dom (p * f2)) = ( dom f2) by VALUED_1:def 5;

 then

 A288: ( len (p * f2)) = p9 by A27, FINSEQ_3: 29;

 (p * f2) is Element of ( NAT * ) by FINSEQ_1:def 11;

 then (p * f2) in (p9 -tuples_on NAT ) by A288;

 then

 A289: (p * f2) is Element of (p9 -tuples_on REAL ) by FINSEQ_2: 109, NUMBERS: 19;



 A290: p9 = (((p -' 1) + 1) div 2) by A9, NAT_2: 26

 .= (p div 2) by A6, XREAL_1: 235;

 reconsider X as finite Subset of NAT by A184, XBOOLE_1: 1;

 set m = ( card X);

 reconsider Y = (( rng f4) \ X) as finite Subset of NAT ;



 A291: f3 is Element of ( NAT * ) by FINSEQ_1:def 11;

 ( len f3) = p9 by A17, A96, CARD_1:def 7;

 then f3 in (p9 -tuples_on NAT ) by A291;

 then

 A292: f3 is Element of (p9 -tuples_on REAL ) by FINSEQ_2: 109, NUMBERS: 19;



 A293: ( rng f3) c= ( Seg n1) by A99, A108, XBOOLE_1: 73;

 then

 A294: ( rng f4) = ( rng f3) by FINSEQ_1:def 13;

 then

 A295: X c= ( Seg n1) by A293, A184;



 A296: ( dom ((p * f2) + f3)) = (( dom (p * f2)) /\ ( dom f3)) by VALUED_1:def 1

 .= (( dom f2) /\ ( dom f3)) by VALUED_1:def 5

 .= ( dom f1) by A97, A100;

 for d be Nat st d in ( dom f1) holds (f1 . d) = (((p * f2) + f3) . d)

 proof

 let d be Nat;

 assume

 A297: d in ( dom f1);

 then

 A298: d in ( dom (p * f2)) by A100, VALUED_1:def 5;

 (((p * f2) + f3) . d) = (((p * f2) . d) + (f3 . d)) by A296, A297, VALUED_1:def 1;



 hence (((p * f2) + f3) . d) = ((p * (f2 . d)) + (f3 . d)) by A298, VALUED_1:def 5

 .= (f1 . d) by A101, A297;

 end;

 then f1 = ((p * f2) + f3) by A296;



 then

 A299: ( Sum f1) = (( Sum (p * f2)) + ( Sum f3)) by A289, A292, RVSUM_1: 89

 .= ((p * ( Sum f2)) + ( Sum f3)) by RVSUM_1: 87;



 A300: (( rng f4) \ X) c= ( rng f4) by XBOOLE_1: 36;

 then

 A301: Y c= ( Seg n1) by A293, A294;



 A302: ( len f3) = ( card ( rng f4)) by A127, A294, FINSEQ_4: 62;

 then

 reconsider n = (p9 - m) as Element of NAT by A18, A96, A184, NAT_1: 21, NAT_1: 43;



 A303: f4 = ((f4 | n) ^ (f4 /^ n)) by RFINSEQ: 8;

 then

 A304: (f4 /^ n) is one-to-one by A109, FINSEQ_3: 91;



 A305: f3 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 f4 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 then

 A306: ( Sum f4) = ( Sum f3) by A127, A294, A109, RFINSEQ: 9, RFINSEQ: 26, A305;

 for k,l be Nat st k in Y & l in X holds k < l

 proof

 let k,l be Nat;

 assume that

 A307: k in Y and

 A308: l in X;



 A309: not k in X by A307, XBOOLE_0:def 5;



 A310: ex l1 be Element of NAT st l1 = l & l1 in ( rng f4) & l1 > (p / 2) by A308;

 k in ( rng f4) by A307, XBOOLE_0:def 5;

 then k <= (p / 2) by A309;

 hence thesis by A310, XXREAL_0: 2;

 end;

 then ( Sgm (Y \/ X)) = (( Sgm Y) ^ ( Sgm X)) by A295, A301, FINSEQ_3: 42;

 then ( Sgm (( rng f4) \/ X)) = (( Sgm Y) ^ ( Sgm X)) by XBOOLE_1: 39;

 then

 A311: f4 = (( Sgm Y) ^ ( Sgm X)) by A294, A184, XBOOLE_1: 12;

 then ( Sum f4) = (( Sum ( Sgm Y)) + ( Sum ( Sgm X))) by RVSUM_1: 75;

 then

 A312: (q * ( Sum ( idseq p9))) = (((p * ( Sum f2)) + ( Sum ( Sgm Y))) + ( Sum ( Sgm X))) by A299, A306, RVSUM_1: 87;



 A313: ( len ( Sgm Y)) = ( card Y) by A293, A294, A300, FINSEQ_3: 39, XBOOLE_1: 1

 .= (p9 - m) by A18, A96, A184, A302, CARD_2: 44;

 then

 A314: (f4 /^ n) = ( Sgm X) by A311, FINSEQ_5: 37;



 A315: (f4 | n) = ( Sgm Y) by A311, A313, FINSEQ_3: 113, FINSEQ_6: 10;



 A316: (f4 | n) is one-to-one by A109, A303, FINSEQ_3: 91;

 ( Lege (q,p)) = (( - 1) |^ ( Sum f2))

 proof

 set f5 = ((m |-> p) - (f4 /^ n));

 set f6 = ((f4 | n) ^ f5);



 A317: (f4 /^ n) is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A318: ( len (f4 | n)) = n by A128, FINSEQ_1: 59, XREAL_1: 43;



 A319: ( len (f4 /^ n)) = (( len f4) -' n) by RFINSEQ: 29

 .= (( len f4) - n) by A128, XREAL_1: 43, XREAL_1: 233

 .= m by A128;



 A320: ( dom f5) = (( dom (m |-> p)) /\ ( dom (f4 /^ n))) by VALUED_1: 12

 .= (( Seg ( len (m |-> p))) /\ ( dom (f4 /^ n))) by FINSEQ_1:def 3

 .= (( dom (f4 /^ n)) /\ ( dom (f4 /^ n))) by FINSEQ_1:def 3, A319, CARD_1:def 7

 .= ( dom (f4 /^ n));

 then

 A321: ( len f5) = ( len (f4 /^ n)) by FINSEQ_3: 29;



 A322: for d st d in ( dom f5) holds (f5 . d) = (p - ((f4 /^ n) . d))

 proof

 let d;

 assume

 A323: d in ( dom f5);

 then d in ( Seg m) by A319, A320, FINSEQ_1:def 3;

 then ((m |-> p) . d) = p by FINSEQ_2: 57;

 hence thesis by A323, VALUED_1: 13;

 end;



 A324: for d st d in ( dom f5) holds (f5 . d) > 0 & (f5 . d) <= p9

 proof

 let d;

 reconsider w = (f5 . d) as Element of INT by INT_1:def 2;

 assume

 A325: d in ( dom f5);

 then (( Sgm X) . d) in ( rng ( Sgm X)) by A314, A320, FUNCT_1: 3;

 then (( Sgm X) . d) in X by A295, FINSEQ_1:def 13;

 then

 A326: ex ll be Element of NAT st ll = (( Sgm X) . d) & ll in ( rng f3) & ll > (p / 2) by A294;

 then

 consider e be Nat such that

 A327: e in ( dom f3) and

 A328: (f3 . e) = ((f4 /^ n) . d) by A314, FINSEQ_2: 10;

 ((f4 /^ n) . d) = ((f1 . e) mod p) by A97, A327, A328, EULER_2:def 1;

 then

 A329: ((f4 /^ n) . d) < p by NAT_D: 1;



 A330: (f5 . d) = (p - ((f4 /^ n) . d)) by A322, A325;

 then w < (p - (p / 2)) by A314, A326, XREAL_1: 10;

 hence thesis by A290, A330, A329, INT_1: 54, XREAL_1: 50;

 end;



 A331: ( rng f5) c= INT by RELAT_1:def 19;

 for d be Nat st d in ( dom f5) holds (f5 . d) in NAT

 proof

 let d be Nat;

 assume

 A332: d in ( dom f5);

 (f5 . d) > 0 by A332, A324;

 hence thesis by A331, INT_1: 3;

 end;

 then

 reconsider f5 as FinSequence of NAT by FINSEQ_2: 12;

 f5 is FinSequence of NAT ;

 then

 reconsider f6 as FinSequence of NAT by FINSEQ_1: 75;



 A333: f6 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A334: n <= ( len f4) by A128, XREAL_1: 43;



 A335: ( rng (f4 | n)) misses ( rng f5)

 proof

 assume not ( rng (f4 | n)) misses ( rng f5);

 then

 consider x be object such that

 A336: x in ( rng (f4 | n)) and

 A337: x in ( rng f5) by XBOOLE_0: 3;

 consider e be Nat such that

 A338: e in ( dom f5) and

 A339: (f5 . e) = x by A337, FINSEQ_2: 10;

 x = (p - ((f4 /^ n) . e)) by A322, A338, A339;

 then

 A340: x = (p - (f4 . (e + n))) by A334, A320, A338, RFINSEQ:def 1;

 (e + n) in ( dom f4) by A320, A338, FINSEQ_5: 26;

 then

 consider e1 be Nat such that

 A341: e1 in ( dom f3) and

 A342: (f3 . e1) = (f4 . (e + n)) by A294, FINSEQ_2: 10, FUNCT_1: 3;



 A343: e1 <= p9 by A18, A96, A341, FINSEQ_3: 25;

 ( rng (f4 | n)) c= ( rng f4) by FINSEQ_5: 19;

 then

 consider d1 be Nat such that

 A344: d1 in ( dom f3) and

 A345: (f3 . d1) = x by A294, A336, FINSEQ_2: 10;

 d1 <= p9 by A18, A96, A344, FINSEQ_3: 25;

 then (d1 + e1) <= (p9 + p9) by A343, XREAL_1: 7;

 then

 A346: (d1 + e1) < p by A7, A11, XREAL_1: 146, XXREAL_0: 2;

 x = ((f1 . d1) mod p) by A97, A344, A345, EULER_2:def 1;

 then (((f1 . d1) mod p) + (f4 . (e + n))) = p by A340;

 then (((f1 . d1) mod p) + ((f1 . e1) mod p)) = p by A97, A341, A342, EULER_2:def 1;

 then ((((f1 . d1) mod p) + ((f1 . e1) mod p)) mod p) = 0 by NAT_D: 25;

 then (((f1 . d1) + (f1 . e1)) mod p) = 0 by EULER_2: 6;

 then p divides ((f1 . d1) + (f1 . e1)) by PEPIN: 6;

 then p divides ((d1 * q) + (f1 . e1)) by A13, A97, A344;

 then p divides ((d1 * q) + (e1 * q)) by A13, A97, A341;

 then

 A347: p divides ((d1 + e1) * q);

 d1 >= 1 by A344, FINSEQ_3: 25;

 hence contradiction by A4, A347, A346, NAT_D: 7, PEPIN: 3;

 end;

 for d,e be Nat st 1 <= d & d < e & e <= ( len f5) holds (f5 . d) <> (f5 . e)

 proof

 let d,e be Nat;

 assume that

 A348: 1 <= d and

 A349: d < e and

 A350: e <= ( len f5);

 1 <= e by A348, A349, XXREAL_0: 2;

 then

 A351: e in ( dom f5) by A350, FINSEQ_3: 25;

 then

 A352: (f5 . e) = (p - ((f4 /^ n) . e)) by A322;

 d < ( len f5) by A349, A350, XXREAL_0: 2;

 then

 A353: d in ( dom f5) by A348, FINSEQ_3: 25;

 then (f5 . d) = (p - ((f4 /^ n) . d)) by A322;

 hence thesis by A304, A320, A349, A353, A351, A352;

 end;

 then ( len f5) = ( card ( rng f5)) by GRAPH_5: 7;

 then f5 is one-to-one by FINSEQ_4: 62;

 then

 A354: f6 is one-to-one by A316, A335, FINSEQ_3: 91;



 A355: for d st d in ( dom f6) holds (f6 . d) > 0 & (f6 . d) <= p9

 proof

 let d;

 assume

 A356: d in ( dom f6);

 per cases by A356, FINSEQ_1: 25;

 suppose

 A357: d in ( dom (f4 | n));

 then ((f4 | n) . d) in ( rng ( Sgm Y)) by A315, FUNCT_1: 3;

 then

 A358: ((f4 | n) . d) in Y by A301, FINSEQ_1:def 13;

 then

 A359: ((f4 | n) . d) in ( rng f4) by XBOOLE_0:def 5;

 not ((f4 | n) . d) in X by A358, XBOOLE_0:def 5;

 then ((f4 | n) . d) <= (p / 2) by A359;

 then

 A360: ((f4 | n) . d) <= p9 by A290, INT_1: 54;

 not ((f4 | n) . d) in { 0 } by A108, A294, A359, XBOOLE_0: 3;

 then ((f4 | n) . d) <> 0 by TARSKI:def 1;

 hence thesis by A357, A360, FINSEQ_1:def 7;

 end;

 suppose ex l be Nat st l in ( dom f5) & d = (( len (f4 | n)) + l);

 then

 consider l be Element of NAT such that

 A361: l in ( dom f5) and

 A362: d = (( len (f4 | n)) + l);

 (f6 . d) = (f5 . l) by A361, A362, FINSEQ_1:def 7;

 hence thesis by A324, A361;

 end;

 end;



 A363: ( idseq p9) is FinSequence of REAL by RVSUM_1: 145;

 ( len f6) = (( len (f4 | n)) + ( len f5)) by FINSEQ_1: 22

 .= p9 by A318, A319, A321;

 then ( rng f6) = ( rng ( idseq p9)) by A354, A355, Th40;



 then M = ( Sum f6) by A363, A354, A333, RFINSEQ: 9, RFINSEQ: 26

 .= (( Sum (f4 | n)) + ( Sum f5)) by RVSUM_1: 75

 .= (( Sum (f4 | n)) + ((m * p) - ( Sum (f4 /^ n)))) by A319, A317, Th47

 .= ((( Sum (f4 | n)) + (m * p)) - ( Sum (f4 /^ n)));

 then ((q - 1) * M) = (((p * ( Sum f2)) + (2 * ( Sum ( Sgm X)))) - (m * p)) by A312, A314, A315;



 then

 A364: (((q -' 1) * M) mod 2) = ((((p * ( Sum f2)) - (m * p)) + (2 * ( Sum ( Sgm X)))) mod 2) by A28, XREAL_1: 233

 .= (((p * ( Sum f2)) - (m * p)) mod 2) by EULER_1: 12;

 2 divides ((q -' 1) * M) by A39, NAT_D: 9;

 then (((q -' 1) * M) mod 2) = 0 by PEPIN: 6;

 then 2 divides (p * (( Sum f2) - m)) by A364, Lm1;

 then (( Sum f2),m) are_congruent_mod 2 by A183, INT_2: 25;

 then (( Sum f2) mod 2) = (m mod 2) by NAT_D: 64;

 then (( - 1) |^ ( Sum f2)) = (( - 1) |^ m) by Th45;

 hence thesis by A1, A5, A294, Th41;

 end;

 hence thesis by A131, A186, NEWTON: 8;

 end;

 theorem :: INT_5:50

 p > 2 & q > 2 & p <> q & (p mod 4) = 3 & (q mod 4) = 3 implies ( Lege (p,q)) = ( - ( Lege (q,p)))

 proof

 assume that

 A1: p > 2 and

 A2: q > 2 and

 A3: p <> q and

 A4: (p mod 4) = 3 and

 A5: (q mod 4) = 3;

 q > 1 by INT_2:def 4;

 then

 A6: (q -' 1) = (q - 1) by XREAL_1: 233;

 q = ((4 * (q div 4)) + 3) by A5, NAT_D: 2;

 then (q -' 1) = (2 * ((2 * (q div 4)) + 1)) by A6;

 then

 A7: ((q -' 1) div 2) = ((2 * (q div 4)) + 1) by NAT_D: 18;

 p > 1 by INT_2:def 4;

 then

 A8: (p -' 1) = (p - 1) by XREAL_1: 233;

 p = ((4 * (p div 4)) + 3) by A4, NAT_D: 2;

 then (p -' 1) = (2 * ((2 * (p div 4)) + 1)) by A8;

 then ((p -' 1) div 2) = ((2 * (p div 4)) + 1) by NAT_D: 18;



 then

 A9: (( Lege (p,q)) * ( Lege (q,p))) = (( - 1) |^ (((2 * (p div 4)) + 1) * ((2 * (q div 4)) + 1))) by A1, A2, A3, A7, Th49

 .= ((( - 1) |^ ((2 * (p div 4)) + 1)) |^ ((2 * (q div 4)) + 1)) by NEWTON: 9

 .= (((( - 1) |^ (2 * (p div 4))) * ( - 1)) |^ ((2 * (q div 4)) + 1)) by NEWTON: 6

 .= ((((( - 1) |^ 2) |^ (p div 4)) * ( - 1)) |^ ((2 * (q div 4)) + 1)) by NEWTON: 9

 .= ((((1 |^ 2) |^ (p div 4)) * ( - 1)) |^ ((2 * (q div 4)) + 1)) by WSIERP_1: 1

 .= ((( - 1) |^ (2 * (q div 4))) * ( - 1)) by NEWTON: 6

 .= (((( - 1) |^ 2) |^ (q div 4)) * ( - 1)) by NEWTON: 9

 .= (((1 |^ 2) |^ (q div 4)) * ( - 1)) by WSIERP_1: 1

 .= (1 * ( - 1));

 per cases by Th25;

 suppose ( Lege (p,q)) = 1;

 hence thesis by A9;

 end;

 suppose ( Lege (p,q)) = 0 ;

 hence thesis by A9;

 end;

 suppose ( Lege (p,q)) = ( - 1);

 hence thesis by A9;

 end;

 end;

 theorem :: INT_5:51

 p > 2 & q > 2 & p <> q & ((p mod 4) = 1 or (q mod 4) = 1) implies ( Lege (p,q)) = ( Lege (q,p))

 proof

 assume that

 A1: p > 2 and

 A2: q > 2 and

 A3: p <> q and

 A4: (p mod 4) = 1 or (q mod 4) = 1;

 p > 1 by INT_2:def 4;

 then

 A5: (p -' 1) = (p - 1) by XREAL_1: 233;

 q > 1 by INT_2:def 4;

 then

 A6: (q -' 1) = (q - 1) by XREAL_1: 233;

 per cases by A4;

 suppose (p mod 4) = 1;

 then p = ((4 * (p div 4)) + 1) by NAT_D: 2;

 then (p -' 1) = (2 * (2 * (p div 4))) by A5;

 then ((p -' 1) div 2) = (2 * (p div 4)) by NAT_D: 18;



 then

 A7: (( Lege (p,q)) * ( Lege (q,p))) = (( - 1) |^ ((2 * (p div 4)) * ((q -' 1) div 2))) by A1, A2, A3, Th49

 .= ((( - 1) |^ (2 * (p div 4))) |^ ((q -' 1) div 2)) by NEWTON: 9

 .= (((( - 1) |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2)) by NEWTON: 9

 .= (((1 |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2)) by WSIERP_1: 1

 .= 1;

 per cases by Th25;

 suppose ( Lege (p,q)) = 1;

 hence thesis by A7;

 end;

 suppose ( Lege (p,q)) = 0 ;

 hence thesis by A7;

 end;

 suppose ( Lege (p,q)) = ( - 1);

 hence thesis by A7;

 end;

 end;

 suppose (q mod 4) = 1;

 then q = ((4 * (q div 4)) + 1) by NAT_D: 2;

 then (q -' 1) = (2 * (2 * (q div 4))) by A6;

 then ((q -' 1) div 2) = (2 * (q div 4)) by NAT_D: 18;



 then

 A8: (( Lege (p,q)) * ( Lege (q,p))) = (( - 1) |^ ((2 * (q div 4)) * ((p -' 1) div 2))) by A1, A2, A3, Th49

 .= ((( - 1) |^ (2 * (q div 4))) |^ ((p -' 1) div 2)) by NEWTON: 9

 .= (((( - 1) |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2)) by NEWTON: 9

 .= (((1 |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2)) by WSIERP_1: 1

 .= 1;

 per cases by Th25;

 suppose ( Lege (p,q)) = 1;

 hence thesis by A8;

 end;

 suppose ( Lege (p,q)) = 0 ;

 hence thesis by A8;

 end;

 suppose ( Lege (p,q)) = ( - 1);

 hence thesis by A8;

 end;

 end;

 end;