let p, q be Prime; :: thesis: ( p > 2 & q > 2 & p <> q & p mod 4 = 3 & q mod 4 = 3 implies Lege (p,q) = - (Lege (q,p)) )

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 ; :: thesis: Lege (p,q) = - (Lege (q,p))

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) ;

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 ; :: thesis: Lege (p,q) = - (Lege (q,p))

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) ;