let
p
be
Prime
;
:: thesis:
for
i
being
Element
of
INT
holds
i
mod
p
is
Element
of
(
GF
p
)
let
i
be
Element
of
INT
;
:: thesis:
i
mod
p
is
Element
of
(
GF
p
)
i
mod
p
in
NAT
by
INT_1:3
,
INT_1:57
;
hence
i
mod
p
is
Element
of
(
GF
p
)
by
INT_1:58
,
NAT_1:44
;
:: thesis:
verum