let n be Nat; :: thesis: ( n > 0 implies for a being Element of Segm n holds

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) ) )

assume A1: n > 0 ; :: thesis: for a being Element of Segm n holds

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

let a be Element of Segm n; :: thesis: ( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

reconsider n = n as non zero Nat by A1;

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

A2: a < n by NAT_1:44;

then a - a < n - a by XREAL_1:9;

then reconsider b = n - a as Element of NAT by INT_1:3;

consider c being Element of NAT such that

A3: c = b mod n ;

A4: ( (compint n) . a = 0 implies a = 0 )

A10: ( ( b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A3, NAT_D:def 2;

A11: n - a <= n

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) ) )

assume A1: n > 0 ; :: thesis: for a being Element of Segm n holds

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

let a be Element of Segm n; :: thesis: ( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

reconsider n = n as non zero Nat by A1;

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

A2: a < n by NAT_1:44;

then a - a < n - a by XREAL_1:9;

then reconsider b = n - a as Element of NAT by INT_1:3;

consider c being Element of NAT such that

A3: c = b mod n ;

A4: ( (compint n) . a = 0 implies a = 0 )

proof

consider t being Nat such that
a - a < n - a
by A2, XREAL_1:9;

then reconsider a9 = n - a as Element of NAT by INT_1:3;

assume A5: (compint n) . a = 0 ; :: thesis: a = 0

n <= n + a by NAT_1:11;

then A6: n - a <= (n + a) - a by XREAL_1:9;

consider t being Nat such that

A7: a9 = (n * t) + (a9 mod n) and

a9 mod n < n by NAT_D:def 2;

assume a <> 0 ; :: thesis: contradiction

then n - a <> n ;

then A8: n - a < n by A6, XXREAL_0:1;

t = 0

hence contradiction by NAT_1:44; :: thesis: verum

end;then reconsider a9 = n - a as Element of NAT by INT_1:3;

assume A5: (compint n) . a = 0 ; :: thesis: a = 0

n <= n + a by NAT_1:11;

then A6: n - a <= (n + a) - a by XREAL_1:9;

consider t being Nat such that

A7: a9 = (n * t) + (a9 mod n) and

a9 mod n < n by NAT_D:def 2;

assume a <> 0 ; :: thesis: contradiction

then n - a <> n ;

then A8: n - a < n by A6, XXREAL_0:1;

t = 0

proof

then
a9 = 0
by A5, A7, Def11;
assume
t <> 0
; :: thesis: contradiction

then 1 + 0 <= t by INT_1:7;

then A9: 1 * n <= t * n by XREAL_1:64;

t * n <= (t * n) + (a9 mod n) by NAT_1:11;

hence contradiction by A8, A7, A9, XXREAL_0:2; :: thesis: verum

end;then 1 + 0 <= t by INT_1:7;

then A9: 1 * n <= t * n by XREAL_1:64;

t * n <= (t * n) + (a9 mod n) by NAT_1:11;

hence contradiction by A8, A7, A9, XXREAL_0:2; :: thesis: verum

hence contradiction by NAT_1:44; :: thesis: verum

A10: ( ( b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A3, NAT_D:def 2;

A11: n - a <= n

proof

assume
n - a > n
; :: thesis: contradiction

then (n - a) + a > n + a by XREAL_1:6;

hence contradiction by NAT_1:11; :: thesis: verum

end;then (n - a) + a > n + a by XREAL_1:6;

hence contradiction by NAT_1:11; :: thesis: verum

A12: now :: thesis: ( a = 0 implies (compint n) . a = 0 )

assume A13:
a = 0
; :: thesis: (compint n) . a = 0

A14: t = 1

end;A14: t = 1

proof

end;

c = 0
now :: thesis: ( ( t = 0 & t = 1 ) or ( t <> 0 & t = 1 ) )end;

hence
t = 1
; :: thesis: verumper cases
( t = 0 or t <> 0 )
;

end;

case A15:
t <> 0
; :: thesis: t = 1

t < 2

then A18: t <= 1 by NAT_1:13;

1 + 0 <= t by A15, INT_1:7;

hence t = 1 by A18, XXREAL_0:1; :: thesis: verum

end;proof

then
t < 1 + 1
;
assume
t >= 2
; :: thesis: contradiction

then A16: n * t >= n * 2 by XREAL_1:64;

A17: n <= (n * 1) + (n * 1) by NAT_1:11;

(n * t) + c >= n * t by NAT_1:11;

then n - a >= n * 2 by A10, A16, XXREAL_0:2;

then n * 1 = 2 * n by A13, A17, XXREAL_0:1;

hence contradiction by A1; :: thesis: verum

end;then A16: n * t >= n * 2 by XREAL_1:64;

A17: n <= (n * 1) + (n * 1) by NAT_1:11;

(n * t) + c >= n * t by NAT_1:11;

then n - a >= n * 2 by A10, A16, XXREAL_0:2;

then n * 1 = 2 * n by A13, A17, XXREAL_0:1;

hence contradiction by A1; :: thesis: verum

then A18: t <= 1 by NAT_1:13;

1 + 0 <= t by A15, INT_1:7;

hence t = 1 by A18, XXREAL_0:1; :: thesis: verum

proof

hence
(compint n) . a = 0
by A3, Def11; :: thesis: verum
assume
c <> 0
; :: thesis: contradiction

then n + c > n + 0 by XREAL_1:6;

hence contradiction by A10, A11, A14; :: thesis: verum

end;then n + c > n + 0 by XREAL_1:6;

hence contradiction by A10, A11, A14; :: thesis: verum

now :: thesis: ( a <> 0 implies (compint n) . a = n - a )

hence
( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )
by A12, A4; :: thesis: verumassume A19:
a <> 0
; :: thesis: (compint n) . a = n - a

A20: n - a < n

end;A20: n - a < n

proof

t = 0
assume
n - a >= n
; :: thesis: contradiction

then n - a = n by A11, XXREAL_0:1;

hence contradiction by A19; :: thesis: verum

end;then n - a = n by A11, XXREAL_0:1;

hence contradiction by A19; :: thesis: verum

proof

hence
(compint n) . a = n - a
by A3, A10, Def11; :: thesis: verum
assume
t <> 0
; :: thesis: contradiction

then 1 + 0 <= t by INT_1:7;

then A21: 1 * n <= t * n by XREAL_1:64;

n * t <= (n * t) + c by NAT_1:11;

hence contradiction by A10, A20, A21, XXREAL_0:2; :: thesis: verum

end;then 1 + 0 <= t by INT_1:7;

then A21: 1 * n <= t * n by XREAL_1:64;

n * t <= (n * t) + c by NAT_1:11;

hence contradiction by A10, A20, A21, XXREAL_0:2; :: thesis: verum