let F1 be Field; :: thesis: ( F1 is finite iff ex n being non zero Nat st card F1 = (Char F1) |^ n )

now :: thesis: ( F1 is finite implies ex n being non zero Nat st card F1 = (Char F1) |^ n )

assume F1 is finite ; :: thesis: ex n being non zero Nat st card F1 = (Char F1) |^ n
then reconsider F = F1 as finite Field ;
set p = Char F;
H: F is Char F -characteristic by RING_3:def 6;
set M = multMagma(# the carrier of F, the addF of F #);
( multMagma(# the carrier of F, the addF of F #) is Group-like & multMagma(# the carrier of F, the addF of F #) is associative )

proof

ex e being Element of multMagma(# the carrier of F, the addF of F #) st
for h being Element of multMagma(# the carrier of F, the addF of F #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = e & g * h = e ) )

proof

reconsider z = 0. F as Element of multMagma(# the carrier of F, the addF of F #) ;
take z ; :: thesis: for h being Element of multMagma(# the carrier of F, the addF of F #) holds
( h * z = h & z * h = h & ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z ) )

now :: thesis: for h being Element of multMagma(# the carrier of F, the addF of F #) holds
( h * z = h & z * h = h & ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z ) )

let h be Element of multMagma(# the carrier of F, the addF of F #); :: thesis: ( h * z = h & z * h = h & ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z ) )
reconsider j = h as Element of F ;
( j + (0. F) = j & (0. F) + j = j ) ;
hence ( h * z = h & z * h = h ) ; :: thesis: ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z )
thus ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z ) :: thesis: verum

proof

reconsider g = - j as Element of multMagma(# the carrier of F, the addF of F #) ;
take g ; :: thesis: ( h * g = z & g * h = z )
thus h * g = j + (- j)
.= z by RLVECT_1:5 ; :: thesis: g * h = z
thus g * h = (- j) + j
.= z by RLVECT_1:5 ; :: thesis: verum

end;

end;

hence for h being Element of multMagma(# the carrier of F, the addF of F #) holds
( h * z = h & z * h = h & ex g being Element of multMagma(# the carrier of F, the addF of F #) st
( h * g = z & g * h = z ) ) ; :: thesis: verum

end;

hence multMagma(# the carrier of F, the addF of F #) is Group-like by GROUP_1:def 2; :: thesis: multMagma(# the carrier of F, the addF of F #) is associative

now :: thesis: for x, y, z being Element of multMagma(# the carrier of F, the addF of F #) holds (x * y) * z = x * (y * z)

let x, y, z be Element of multMagma(# the carrier of F, the addF of F #); :: thesis: (x * y) * z = x * (y * z)
reconsider a = x, b = y, c = z as Element of F ;
thus (x * y) * z = (a + b) + c
.= a + (b + c) by RLVECT_1:def 3
.= x * (y * z) ; :: thesis: verum

end;

hence multMagma(# the carrier of F, the addF of F #) is associative by GROUP_1:def 3; :: thesis: verum

end;

then reconsider M = multMagma(# the carrier of F, the addF of F #) as finite Group ;
H1: 1_ M = 0. F

proof

reconsider z = 0. F as Element of M ;

now :: thesis: for h being Element of M holds
( h * z = h & z * h = h )

let h be Element of M; :: thesis: ( h * z = h & z * h = h )
reconsider j = h as Element of F ;
( j + (0. F) = j & (0. F) + j = j ) ;
hence ( h * z = h & z * h = h ) ; :: thesis: verum

end;

hence 1_ M = 0. F by GROUP_1:def 4; :: thesis: verum

end;

H2: now :: thesis: for a being Element of F
for b being Element of M
for n being non zero Nat st a = b holds
b |^ n = n * a

let a be Element of F; :: thesis: for b being Element of M
for n being non zero Nat st a = b holds
b |^ n = n * a
let b be Element of M; :: thesis: for n being non zero Nat st a = b holds
b |^ n = n * a
let n be non zero Nat; :: thesis: ( a = b implies b |^ n = n * a )
assume AS: a = b ; :: thesis: b |^ n = n * a
defpred S₁[ Nat] means for a being Element of F
for b being Element of M st a = b holds
b |^ $1 = $1 * a;
IA: S₁[1]

proof

now :: thesis: for a being Element of F
for b being Element of M st a = b holds
b |^ 1 = 1 * a

let a be Element of F; :: thesis: for b being Element of M st a = b holds
b |^ 1 = 1 * a
let b be Element of M; :: thesis: ( a = b implies b |^ 1 = 1 * a )
assume a = b ; :: thesis: b |^ 1 = 1 * a
hence b |^ 1 = a by GROUP_1:26
.= 1 * a by BINOM:13 ;
:: thesis: verum

end;

hence S₁[1] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for a being Element of F
for b being Element of M st a = b holds
b |^ (k + 1) = (k + 1) * a

let a be Element of F; :: thesis: for b being Element of M st a = b holds
b |^ (k + 1) = (k + 1) * a
let b be Element of M; :: thesis: ( a = b implies b |^ (k + 1) = (k + 1) * a )
assume C: a = b ; :: thesis: b |^ (k + 1) = (k + 1) * a
then D: b |^ k = k * a by B;
thus b |^ (k + 1) = (b |^ k) * b by GROUP_1:34
.= (k * a) + (1 * a) by D, C, BINOM:13
.= (k + 1) * a by BINOM:15 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
n >= 0 + 1 by INT_1:7;
hence b |^ n = n * a by I, AS; :: thesis: verum

end;

reconsider e = 1. F as Element of M ;
ord e = Char F

proof

B0: Char F is Element of NAT by ORDINAL1:def 12;
B1: e |^ (Char F) = (Char F) * (1. F) by H2
.= (Char F) '*' (1. F) by RING_3:def 2
.= 1_ M by H1, RING_3:def 5 ;
then B2: not e is being_of_order_0 by GROUP_1:def 10;

now :: thesis: for m being Nat st e |^ m = 1_ M & m <> 0 holds
Char F <= m

let m be Nat; :: thesis: ( e |^ m = 1_ M & m <> 0 implies Char F <= m )
assume B4: ( e |^ m = 1_ M & m <> 0 ) ; :: thesis: Char F <= m
m '*' (1. F) = m * (1. F) by RING_3:def 2
.= 0. F by B4, H2, H1 ;
hence Char F <= m by B4, RING_3:def 5; :: thesis: verum

end;

hence ord e = Char F by B0, B1, B2, GROUP_1:def 11; :: thesis: verum

end;

then A: Char F divides card M by GR_CY_1:8;

B: now :: thesis: for q being Prime st Char F <> q holds
not q divides card M

let q be Prime; :: thesis: ( Char F <> q implies not q divides card M )
assume E: ( Char F <> q & q divides card M ) ; :: thesis: contradiction
then consider b being Element of M such that
C: ord b = q by GROUP_10:11;
reconsider a = b as Element of F ;
q > 1 by INT_2:def 4;
then D: not a is zero by H1, C, GROUP_1:42;
q * a = b |^ q by H2
.= 0. F by C, GROUP_1:41, H1 ;
then ( Char F divides q & Char F > 1 ) by H, D, Lm2a, INT_2:def 4;
hence contradiction by E, INT_2:def 4; :: thesis: verum

end;

ex n being Nat st card F = (Char F) |^ n

proof

consider k, m being Nat such that
C: ( card F = m * ((Char F) |^ k) & not Char F divides m ) by CF1;
( m <= 1 implies not not m = 0 & ... & not m = 1 ) ;

per cases then ( m = 0 or m = 1 or m > 1 ) ;

suppose ( m = 0 or m = 1 ) ; :: thesis: ex n being Nat st card F = (Char F) |^ n

hence ex n being Nat st card F = (Char F) |^ n by C; :: thesis: verum

end;

suppose m > 1 ; :: thesis: ex n being Nat st card F = (Char F) |^ n

then m >= 1 + 1 by INT_1:7;
then ex q being Element of NAT st
( q is prime & q divides m ) by INT_2:31;
hence ex n being Nat st card F = (Char F) |^ n by B, C, INT_2:2; :: thesis: verum

end;

end;

end;

then consider n being Nat such that
F: card F = (Char F) |^ n ;

now :: thesis: not n is zero

assume n is zero ; :: thesis: contradiction
then ( card F = 1 & Char F > 1 ) by F, NEWTON:4, INT_2:def 4;
hence contradiction by A, NAT_D:7; :: thesis: verum

end;

hence ex n being non zero Nat st card F1 = (Char F1) |^ n by F; :: thesis: verum

end;

hence ( F1 is finite iff ex n being non zero Nat st card F1 = (Char F1) |^ n ) ; :: thesis: verum