set K = GF p;
P0:
p > 1
by INT_2:def 4;
now let K1 be
strict Subfield of
GF p;
K1 = GF pset C = the
carrier of
(GF p);
set C1 = the
carrier of
K1;
set n1 =
p - 1;
reconsider n1 =
p - 1 as
Element of
NAT by P0, NAT_1:20;
A1:
for
x being
set st
x in GF p holds
x in K1
proof
A5:
for
n being
Element of
NAT st
n in Segm p holds
n in the
carrier of
K1
proof
defpred S1[
Nat]
means p in the
carrier of
K1;
0 in Segm p
by NAT_1:44;
then
0. (GF p) = 0
by FUNCT_7:def 1;
then
0. K1 = 0
by PFDef2;
then A2:
S1[
0 ]
;
A3:
now let n be
Element of
NAT ;
( 0 <= n & n < n1 & S1[n] implies S1[n + 1] )assume B0:
(
0 <= n &
n < n1 )
;
( S1[n] implies S1[n + 1] )assume B1:
S1[
n]
;
S1[n + 1]B2:
1. K1 =
1. (GF p)
by PFDef2
.=
1
by P0, INT_3:14
;
then B3:
[1,n] in [: the carrier of K1, the carrier of K1:]
by B1, ZFMISC_1:87;
B4:
the
addF of
K1 = the
addF of
(GF p) || the
carrier of
K1
by PFDef2;
B6:
1
+ n < n1 + 1
by B0, XREAL_1:6;
n < n1 + 1
by B0, NAT_1:13;
then B7:
( 1
in Segm p &
n in Segm p )
by P0, NAT_1:44;
the
addF of
K1 . (1,
n) =
(addint p) . (1,
n)
by B3, B4, FUNCT_1:49
.=
(1 + n) mod p
by B7, GR_CY_1:def 4
.=
1
+ n
by B6, NAT_D:63
;
hence
S1[
n + 1]
by B1, B2, BINOP_1:17;
verum end;
A4:
for
n being
Element of
NAT st
0 <= n &
n <= n1 holds
S1[
n]
from INT_1:sch 7(A2, A3);
thus
for
n being
Element of
NAT st
n in Segm p holds
S1[
n]
verum
end;
thus
for
x being
set st
x in GF p holds
x in K1
verum
end;
GF p is
strict Subfield of
GF p
by PF1;
then
GF p is
strict Subfield of
K1
by A1, PF8;
hence
K1 = GF p
by PF5;
verum end;
then
for K1 being Field st K1 is strict Subfield of GF p holds
K1 = GF p
;
hence
GF p is prime
by PFDef3; verum