let p be Prime; :: thesis: for n being non zero Nat
for F being p -characteristic Field holds (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F)
let n be non zero Nat; :: thesis: for F being p -characteristic Field holds (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F)
let F be p -characteristic Field; :: thesis: (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F)
set q = X^ ((p |^ n),F);
set Dq = (Deriv F) . (X^ ((p |^ n),F));

now :: thesis: for m being Nat holds ((Deriv F) . (X^ ((p |^ n),F))) . m = (- (1_. F)) . m

let m be Nat; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

per cases ( m = 0 or m = 1 or ( m <> 0 & m <> 1 & m = (p |^ n) - 1 ) or ( m <> 0 & m <> 1 & m <> (p |^ n) - 1 ) ) ;

suppose A: m = 0 ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

hence ((Deriv F) . (X^ ((p |^ n),F))) . m = (0 + 1) * ((X^ ((p |^ n),F)) . (0 + 1)) by RINGDER1:def 8
.= 1 * (- (1. F)) by Lm10
.= - (1. F) by BINOM:13
.= - ((1_. F) . m) by A, POLYNOM3:30
.= (- (1_. F)) . m by BHSP_1:44 ;
:: thesis: verum

end;

suppose A: m = 1 ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

per cases ( ( p = 2 & n = 1 ) or p <> 2 or n <> 1 ) ;

suppose B: ( p = 2 & n = 1 ) ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

then C: Char F = 2 by RING_3:def 6;
thus ((Deriv F) . (X^ ((p |^ n),F))) . m = (1 + 1) * ((X^ ((p |^ n),F)) . (1 + 1)) by A, RINGDER1:def 8
.= 2 * (1. F) by B, Lm10
.= 2 '*' (1. F) by RING_3:def 2
.= - (0. F) by C, REALALG2:24
.= - ((1_. F) . m) by A, POLYNOM3:30
.= (- (1_. F)) . m by BHSP_1:44 ; :: thesis: verum

end;

suppose B: ( p <> 2 or n <> 1 ) ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

C: 2 <> p |^ n

proof

p > 1 by INT_2:def 4;
then E: p >= 1 + 1 by INT_1:7;
F: n >= 0 + 1 by INT_1:7;

per cases ( p <> 2 or n <> 1 ) by B;

suppose p <> 2 ; :: thesis: 2 <> p |^ n

then p > 2 by E, XXREAL_0:1;
then p >= 2 + 1 by INT_1:7;
then H: p |^ n >= 3 |^ n by thX3a;
3 |^ n >= 3 |^ 1 by F, NAT_6:1;
hence 2 <> p |^ n by H, XXREAL_0:2; :: thesis: verum

end;

suppose n <> 1 ; :: thesis: 2 <> p |^ n

then H: not n is trivial by NAT_2:def 1;
I: p |^ n >= 2 |^ n by E, thX3a;
2 |^ n >= 2 |^ 2 by H, NAT_2:29, NAT_6:1;
then p |^ n >= 2 |^ (1 + 1) by I, XXREAL_0:2;
then p |^ n >= (2 |^ 1) * 2 by NEWTON:6;
hence 2 <> p |^ n ; :: thesis: verum

end;

end;

end;

thus ((Deriv F) . (X^ ((p |^ n),F))) . m = (1 + 1) * ((X^ ((p |^ n),F)) . (1 + 1)) by A, RINGDER1:def 8
.= 2 * (0. F) by C, Lm11
.= - (0. F)
.= - ((1_. F) . m) by A, POLYNOM3:30
.= (- (1_. F)) . m by BHSP_1:44 ; :: thesis: verum

end;

end;

end;

suppose A: ( m <> 0 & m <> 1 & m = (p |^ n) - 1 ) ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

reconsider n1 = n - 1 as Nat ;
B: p |^ (n1 + 1) = (p |^ n1) * p by NEWTON:6;
thus ((Deriv F) . (X^ ((p |^ n),F))) . m = (p |^ n) * ((X^ ((p |^ n),F)) . (((p |^ n) - 1) + 1)) by A, RINGDER1:def 8
.= - (0. F) by B, FIELD_15:37
.= - ((1_. F) . m) by A, POLYNOM3:30
.= (- (1_. F)) . m by BHSP_1:44 ; :: thesis: verum

end;

suppose A: ( m <> 0 & m <> 1 & m <> (p |^ n) - 1 ) ; :: thesis: ((Deriv F) . (X^ ((p |^ n),F))) . b₁ = (- (1_. F)) . b₁

then B: ( m + 1 <> 1 & m + 1 <> p |^ n ) ;
thus ((Deriv F) . (X^ ((p |^ n),F))) . m = (m + 1) * ((X^ ((p |^ n),F)) . (m + 1)) by RINGDER1:def 8
.= (m + 1) * (0. F) by B, Lm11
.= - (0. F)
.= - ((1_. F) . m) by A, POLYNOM3:30
.= (- (1_. F)) . m by BHSP_1:44 ; :: thesis: verum

end;

end;

end;

hence (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F) ; :: thesis: verum