let
i
be
Integer
;
:: thesis:
(
i
is
even
implies
(
i
^2
)
mod
4
=
0
)
given
i9
being
Integer
such that
A1
:
i
=
2
*
i9
;
:: according to
INT_1:def 3
,
ABIAN:def 1
:: thesis:
(
i
^2
)
mod
4
=
0
i
^2
=
(
4
*
(
i9
^2
)
)
+
0
by
A1
;
hence
(
i
^2
)
mod
4 =
0
mod
4
by
EULER_1:12
.=
0
by
NAT_D:24
;
:: thesis:
verum