let n be Nat; :: thesis: ( n > 0 implies for a, b being Element of Segm n holds
( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) ) )
assume A1: n > 0 ; :: thesis: for a, b being Element of Segm n holds
( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )
let a, b be Element of Segm n; :: thesis: ( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )
reconsider n = n as non zero Nat by A1;
consider c being Element of NAT such that
A2: c = (a + b) mod n ;
consider t being Nat such that
A3: ( ( a + b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A2, NAT_D:def 2;
A4: now :: thesis: ( a + b >= n implies (addint n) . (a,b) = (a + b) - n )
assume A5: a + b >= n ; :: thesis: (addint n) . (a,b) = (a + b) - n
t = 1
proof
now :: thesis: ( ( t = 0 & t = 1 ) or ( t <> 0 & t = 1 ) )
per cases ( t = 0 or t <> 0 ) ;
case t = 0 ; :: thesis: t = 1
hence t = 1 by A3, A5; :: thesis: verum
end;
case A6: t <> 0 ; :: thesis: t = 1
t < 2
proof
( a < n & b < n ) by NAT_1:44;
then A7: ( (n * t) + c >= n * t & a + b < (n * 1) + (n * 1) ) by NAT_1:11, XREAL_1:8;
assume t >= 2 ; :: thesis: contradiction
then n * t >= n * 2 by XREAL_1:64;
hence contradiction by A3, A7, XXREAL_0:2; :: thesis: verum
end;
then t < 1 + 1 ;
then A8: t <= 1 by NAT_1:13;
1 + 0 <= t by A6, INT_1:7;
hence t = 1 by A8, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence t = 1 ; :: thesis: verum
end;
hence (addint n) . (a,b) = (a + b) - n by A2, A3, GR_CY_1:def 4; :: thesis: verum
end;
A9: ( (addint n) . (a,b) = (a + b) - n implies a + b >= n )
proof
assume (addint n) . (a,b) = (a + b) - n ; :: thesis: a + b >= n
then A10: (a + b) mod n = (a + b) - n by GR_CY_1:def 4;
consider t being Nat such that
A11: a + b = (n * t) + ((a + b) mod n) and
(a + b) mod n < n by NAT_D:def 2;
assume A12: a + b < n ; :: thesis: contradiction
t = 0
proof
assume t <> 0 ; :: thesis: contradiction
then 1 + 0 <= t by INT_1:7;
then A13: 1 * n <= t * n by XREAL_1:64;
t * n <= (t * n) + ((a + b) mod n) by NAT_1:11;
hence contradiction by A12, A11, A13, XXREAL_0:2; :: thesis: verum
end;
hence contradiction by A10, A11; :: thesis: verum
end;
A14: now :: thesis: ( a + b < n implies (addint n) . (a,b) = a + b )
assume A15: a + b < n ; :: thesis: (addint n) . (a,b) = a + b
t = 0
proof
assume t <> 0 ; :: thesis: contradiction
then 1 + 0 <= t by INT_1:7;
then A16: 1 * n <= t * n by XREAL_1:64;
n * t <= (n * t) + c by NAT_1:11;
hence contradiction by A3, A15, A16, XXREAL_0:2; :: thesis: verum
end;
hence (addint n) . (a,b) = a + b by A2, A3, GR_CY_1:def 4; :: thesis: verum
end;
( (addint n) . (a,b) = a + b implies a + b < n )
proof
assume (addint n) . (a,b) = a + b ; :: thesis: a + b < n
then (a + b) mod n = a + b by GR_CY_1:def 4;
hence a + b < n by NAT_D:1; :: thesis: verum
end;
hence ( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) ) by A14, A9, A4; :: thesis: verum