let
a
,
b
be
Nat
;
:: thesis:
for
u
being
Integer
holds
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
let
u
be
Integer
;
:: thesis:
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
b
divides
u
*
b
;
then
A0
:
b
gcd
(
u
*
b
)
=
|.
b
.|
by
Th3
.=
b
;
per
cases
(
a
<>
0
or
a
=
0
)
;
suppose
a
<>
0
;
:: thesis:
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
hence
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
by
EULER_1:16
;
:: thesis:
verum
end;
suppose
a
=
0
;
:: thesis:
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
hence
(
a
+
(
u
*
b
)
)
gcd
b
=
a
gcd
b
by
A0
;
:: thesis:
verum
end;
end;