let
t
,
u
,
z
be
Integer
;
:: thesis:
(
(
u
+
t
)
+
z
is
even
implies
(
u
*
t
)
*
z
is
even
)
assume
A1
:
(
u
+
t
)
+
z
is
even
;
:: thesis:
(
u
*
t
)
*
z
is
even
per
cases
(
u
is
even
or
u
is
odd
)
;
suppose
u
is
even
;
:: thesis:
(
u
*
t
)
*
z
is
even
hence
(
u
*
t
)
*
z
is
even
;
:: thesis:
verum
end;
suppose
B1
:
u
is
odd
;
:: thesis:
(
u
*
t
)
*
z
is
even
per
cases
(
t
is
even
or
t
is
odd
)
;
suppose
t
is
even
;
:: thesis:
(
u
*
t
)
*
z
is
even
hence
(
u
*
t
)
*
z
is
even
;
:: thesis:
verum
end;
suppose
t
is
odd
;
:: thesis:
(
u
*
t
)
*
z
is
even
then
z
is
even
by
A1
,
B1
;
hence
(
u
*
t
)
*
z
is
even
;
:: thesis:
verum
end;
end;
end;
end;