let k, n, t be Nat; ( 1 <= t & k <= n & 2 * t divides k implies ( n div t is even iff (n -' k) div t is even ) )
assume that
A1:
1 <= t
and
A2:
k <= n
and
A3:
2 * t divides k
; ( n div t is even iff (n -' k) div t is even )
consider r being Nat such that
A4:
k = (2 * t) * r
by A3, NAT_D:def 3;
thus
( n div t is even implies (n -' k) div t is even )
( (n -' k) div t is even implies n div t is even )proof
assume
n div t is
even
;
(n -' k) div t is even
then consider p being
Nat such that A5:
n div t = 2
* p
by ABIAN:def 2;
consider q being
Nat such that A6:
n = (t * (2 * p)) + q
and A7:
q < t
by A1, A5, NAT_D:def 1;
1
* t < 2
* t
by A1, XREAL_1:68;
then
t + q < (2 * t) + t
by A7, XREAL_1:8;
then
q < 2
* t
by XREAL_1:6;
then
q / (2 * t) < 1
by XREAL_1:189;
then A8:
p + (q / (2 * t)) < p + 1
by XREAL_1:6;
consider r being
Nat such that A9:
k = (2 * t) * r
by A3, NAT_D:def 3;
A10:
2
* t <> 0
by A1;
then
(2 * t) * r <= ((2 * t) * p) + ((q / (2 * t)) * (2 * t))
by A2, A6, A9, XCMPLX_1:87;
then
(2 * t) * r <= (2 * t) * (p + (q / (2 * t)))
;
then
r <= p + (q / (2 * t))
by A10, XREAL_1:68;
then
(p + (q / (2 * t))) + r < (p + 1) + (p + (q / (2 * t)))
by A8, XREAL_1:8;
then
r < p + 1
by XREAL_1:6;
then A11:
r <= p
by NAT_1:13;
n -' k =
((t * (2 * p)) + q) - ((2 * t) * r)
by A2, A6, A9, XREAL_1:233
.=
(t * (2 * (p - r))) + q
.=
(t * (2 * (p -' r))) + q
by A11, XREAL_1:233
;
hence
(n -' k) div t is
even
by A7, NAT_D:def 1;
verum
end;
assume
(n -' k) div t is even
; n div t is even
then consider p being Nat such that
A12:
(n -' k) div t = 2 * p
by ABIAN:def 2;
consider q being Nat such that
A13:
n -' k = (t * (2 * p)) + q
and
A14:
q < t
by A1, A12, NAT_D:def 1;
n - k = (t * (2 * p)) + q
by A2, A13, XREAL_1:233;
then
n = (t * (2 * (p + r))) + q
by A4;
hence
n div t is even
by A14, NAT_D:def 1; verum