let n be natural number ; :: 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 natural number 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
assume A5: a + b < n ; :: thesis: (addint n) . a,b = a + b
t = 0
proof
assume A6: t <> 0 ; :: thesis: contradiction
1 + 0 <= t by A6, INT_1:20;
then A7: 1 * n <= t * n by XREAL_1:66;
n * t <= (n * t) + c by NAT_1:11;
hence contradiction by A3, A5, A7, XXREAL_0:2; :: thesis: verum
end;
hence (addint n) . a,b = a + b by A2, A3, GR_CY_1:def 5; :: thesis: verum
end;
A8: ( (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 5;
hence a + b < n by NAT_D:1; :: 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 5;
assume A11: a + b < n ; :: thesis: contradiction
consider t being Nat such that
A12: ( a + b = (n * t) + ((a + b) mod n) & (a + b) mod n < n ) by NAT_D:def 2;
t = 0
proof
assume A13: t <> 0 ; :: thesis: contradiction
1 <= t
proof
1 + 0 <= t by A13, INT_1:20;
hence 1 <= t ; :: thesis: verum
end;
then A15: 1 * n <= t * n by XREAL_1:66;
t * n <= (t * n) + ((a + b) mod n) by NAT_1:11;
hence contradiction by A11, A12, A15, XXREAL_0:2; :: thesis: verum
end;
hence contradiction by A10, A12; :: thesis: verum
end;
now
assume A16: a + b >= n ; :: thesis: (addint n) . a,b = (a + b) - n
t = 1
proof
now
per cases ( t = 0 or t <> 0 ) ;
case t = 0 ; :: thesis: t = 1
hence t = 1 by A3, A16; :: thesis: verum
end;
case A17: t <> 0 ; :: thesis: t = 1
t < 2
proof
assume t >= 2 ; :: thesis: contradiction
then A18: n * t >= n * 2 by XREAL_1:66;
A19: (n * t) + c >= n * t by NAT_1:11;
( a < n & b < n ) by NAT_1:45;
then a + b < (n * 1) + (n * 1) by XREAL_1:10;
hence contradiction by A3, A18, A19, XXREAL_0:2; :: thesis: verum
end;
then t < 1 + 1 ;
then A20: t <= 1 by NAT_1:13;
1 + 0 <= t by A17, INT_1:20;
hence t = 1 by A20, 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 5; :: 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 A4, A8, A9; :: thesis: verum