let i, j be integer number ; for n being natural number st n < j & i,n are_congruent_mod j holds
i mod j = n
let n be natural number ; ( n < j & i,n are_congruent_mod j implies i mod j = n )
assume A1:
( n < j & i,n are_congruent_mod j )
; i mod j = n
then consider x being Integer such that
A2:
j * x = i - n
;
A3:
i = ((i div j) * j) + (i mod j)
by A1, INT_1:59;
per cases
( n = 0 or n <> 0 )
;
suppose A5:
n <> 0
;
i mod j = nA6:
i / j =
((j * x) + n) * (j ")
by A2, XCMPLX_0:def 9
.=
(x * (j * (j "))) + (n * (j "))
.=
(x * 1) + (n * (j "))
by A1, XCMPLX_0:def 7
;
then A7:
x <= i / j
by A5, A1, XREAL_1:29;
A8:
(i / j) - 1
= x + ((n * (j ")) - 1)
by A6;
A9:
n / j < j / j
by A1, XREAL_1:74;
j / j =
j * (j ")
by XCMPLX_0:def 9
.=
1
by A1, XCMPLX_0:def 7
;
then
n * (j ") < 1
by A9, XCMPLX_0:def 9;
then
(n * (j ")) - 1
< 1
- 1
by XREAL_1:9;
then
(i / j) - 1
< x
by A8, XREAL_1:30;
then
i div j = x
by A7, INT_1:def 6;
hence
i mod j = n
by A2, A3;
verum end; end;