set K = GF p;
A1:
p > 1
by INT_2:def 4;
now for K1 being strict Subfield of GF p holds K1 = GF plet 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 A1, NAT_1:20;
A2:
for
x being
set st
x in GF p holds
x in K1
proof
A3:
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 SUBSET_1:def 8;
then
0. K1 = 0
by Def1;
then A4:
S1[
0 ]
;
A5:
now for n being Element of NAT st 0 <= n & n < n1 & S1[n] holds
S1[n + 1]let n be
Element of
NAT ;
( 0 <= n & n < n1 & S1[n] implies S1[n + 1] )assume A6:
(
0 <= n &
n < n1 )
;
( S1[n] implies S1[n + 1] )assume A7:
S1[
n]
;
S1[n + 1]A8:
1. K1 =
1. (GF p)
by Def1
.=
1
by A1, INT_3:14
;
then A9:
[1,n] in [: the carrier of K1, the carrier of K1:]
by A7, ZFMISC_1:87;
A10:
the
addF of
K1 = the
addF of
(GF p) || the
carrier of
K1
by Def1;
A11:
1
+ n < n1 + 1
by A6, XREAL_1:6;
n < n1 + 1
by A6, NAT_1:13;
then A12:
( 1
in Segm p &
n in Segm p )
by A1, NAT_1:44;
the
addF of
K1 . (1,
n) =
(addint p) . (1,
n)
by A9, A10, FUNCT_1:49
.=
(1 + n) mod p
by A12, GR_CY_1:def 4
.=
1
+ n
by A11, NAT_D:63
;
hence
S1[
n + 1]
by A7, A8, BINOP_1:17;
verum end;
A13:
for
n being
Element of
NAT st
0 <= n &
n <= n1 holds
S1[
n]
from INT_1:sch 7(A4, A5);
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
by A3;
verum
end;
GF p is
strict Subfield of
GF p
by Th1;
then
GF p is
strict Subfield of
K1
by A2, Th7;
hence
K1 = GF p
by Th4;
verum end;
then
for K1 being Field st K1 is strict Subfield of GF p holds
K1 = GF p
;
hence
GF p is prime
; verum