let n, k be Element of NAT ; :: thesis: ( k > 0 & n mod (2 * k) >= k implies ( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) ) )
assume that
A1: k > 0 and
A2: n mod (2 * k) >= k ; :: thesis: ( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) )
( ex t being Nat st
( n = ((2 * k) * t) + (n mod (2 * k)) & n mod (2 * k) < 2 * k ) or ( n mod (2 * k) = 0 & 2 * k = 0 ) ) by NAT_D:def 2;
then consider t being Nat such that
A3: n = ((2 * k) * t) + (n mod (2 * k)) by A1;
2 * k > 2 * 0 by A1, XREAL_1:68;
then n mod (2 * k) < 2 * k by NAT_D:1;
then A4: (n mod (2 * k)) - k < (2 * k) - k by XREAL_1:9;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
(n mod (2 * k)) - k >= 0 by A2, XREAL_1:48;
then A5: (n mod (2 * k)) -' k = (n mod (2 * k)) - k by XREAL_0:def 2;
then n = (k * ((2 * t) + 1)) + ((n mod (2 * k)) -' k) by A3;
hence (n mod (2 * k)) - k = n mod k by A5, A4, NAT_D:def 2; :: thesis: (n mod k) + k = n mod (2 * k)
hence (n mod k) + k = n mod (2 * k) ; :: thesis: verum