let
i
,
j
be
Integer
;
:: thesis:
(
i
divides
j
implies
i
gcd
j
=
|.
i
.|
)
assume
i
divides
j
;
:: thesis:
i
gcd
j
=
|.
i
.|
then
|.
i
.|
gcd
|.
j
.|
=
|.
i
.|
by
NEWTON:49
,
INT_2:16
;
hence
i
gcd
j
=
|.
i
.|
by
INT_2:34
;
:: thesis:
verum