let n be natural number ; :: 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 natural number by A1;
reconsider a = a as Element of NAT by ORDINAL1:def 13;
A2: a < n by NAT_1:45;
then a - a < n - a by XREAL_1:11;
then reconsider b = n - a as Element of NAT by INT_1:16;
consider c being Element of NAT such that
A3: c = b mod n ;
consider t being Nat such that
A4: ( ( b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A3, NAT_D:def 2;
A5: n - a <= n
proof
assume n - a > n ; :: thesis: contradiction
then (n - a) + a > n + a by XREAL_1:8;
hence contradiction by NAT_1:11; :: thesis: verum
end;
A6: now
assume A7: a = 0 ; :: thesis: (compint n) . a = 0
A8: t = 1
proof
now
per cases ( t = 0 or t <> 0 ) ;
case t = 0 ; :: thesis: t = 1
hence t = 1 by A4, A7; :: thesis: verum
end;
case A9: t <> 0 ; :: thesis: t = 1
t < 2
proof
assume t >= 2 ; :: thesis: contradiction
then A10: n * t >= n * 2 by XREAL_1:66;
(n * t) + c >= n * t by NAT_1:11;
then A11: n - a >= n * 2 by A4, A10, XXREAL_0:2;
n <= (n * 1) + (n * 1) by NAT_1:11;
then n * 1 = 2 * n by A7, A11, XXREAL_0:1;
hence contradiction by A1; :: thesis: verum
end;
then t < 1 + 1 ;
then A12: t <= 1 by NAT_1:13;
1 + 0 <= t by A9, INT_1:20;
hence t = 1 by A12, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence t = 1 ; :: thesis: verum
end;
c = 0
proof
assume A13: c <> 0 ; :: thesis: contradiction
n + c > n + 0 by A13, XREAL_1:8;
hence contradiction by A4, A5, A8; :: thesis: verum
end;
hence (compint n) . a = 0 by A3, Def12; :: thesis: verum
end;
A14: ( (compint n) . a = 0 implies a = 0 )
proof
assume A15: (compint n) . a = 0 ; :: thesis: a = 0
assume A16: a <> 0 ; :: thesis: contradiction
A17: n - a < n
proof
n <= n + a by NAT_1:11;
then A18: n - a <= (n + a) - a by XREAL_1:11;
n - a <> n by A16;
hence n - a < n by A18, XXREAL_0:1; :: thesis: verum
end;
a - a < n - a by A2, XREAL_1:11;
then reconsider a' = n - a as Element of NAT by INT_1:16;
consider t being Nat such that
A19: ( a' = (n * t) + (a' mod n) & a' mod n < n ) by NAT_D:def 2;
t = 0
proof
assume A20: t <> 0 ; :: thesis: contradiction
1 <= t
proof
1 + 0 <= t by A20, INT_1:20;
hence 1 <= t ; :: thesis: verum
end;
then A22: 1 * n <= t * n by XREAL_1:66;
t * n <= (t * n) + (a' mod n) by NAT_1:11;
hence contradiction by A17, A19, A22, XXREAL_0:2; :: thesis: verum
end;
then a' = 0 by A15, A19, Def12;
hence contradiction by NAT_1:45; :: thesis: verum
end;
now
assume A23: a <> 0 ; :: thesis: (compint n) . a = n - a
A24: n - a < n
proof
assume n - a >= n ; :: thesis: contradiction
then n - a = n by A5, XXREAL_0:1;
hence contradiction by A23; :: thesis: verum
end;
t = 0
proof
assume A25: t <> 0 ; :: thesis: contradiction
1 + 0 <= t by A25, INT_1:20;
then A26: 1 * n <= t * n by XREAL_1:66;
n * t <= (n * t) + c by NAT_1:11;
hence contradiction by A4, A24, A26, XXREAL_0:2; :: thesis: verum
end;
hence (compint n) . a = n - a by A3, A4, Def12; :: thesis: verum
end;
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 A6, A14; :: thesis: verum