let L be Field; for m, i, j being Element of NAT
for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let m, i, j be Element of NAT ; for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let x be Element of L; ( i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L )
assume that
A1:
i <> j
and
A2:
( 1 <= i & i <= m & 1 <= j & j <= m )
and
A3:
x is_primitive_root_of_degree m
; ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
A4:
x <> 0. L
by A3, Th30;
then A5: pow (x,(m * (i - j))) =
pow ((pow (x,m)),(i - j))
by Th26
.=
pow ((x |^ m),(i - j))
by Def2
.=
pow ((1. L),(i - j))
by A3
.=
1. L
by Th16
;
ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) )
then consider s being FinSequence of L such that
A7:
dom s = Seg m
and
A8:
for k being Nat st k in Seg m holds
s . k = pow (x,((i - j) * (k - 1)))
;
A9:
for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1)))
consider r being Element of L such that
A12:
r = pow (x,(i - j))
;
A13:
len s = m
by A7, FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len s holds
s . k = (pow (x,(i - j))) |^ (k -' 1)
proof
let k be
Nat;
( 1 <= k & k <= len s implies s . k = (pow (x,(i - j))) |^ (k -' 1) )
assume that A14:
1
<= k
and A15:
k <= len s
;
s . k = (pow (x,(i - j))) |^ (k -' 1)
A16:
1
- 1
<= k - 1
by A14, XREAL_1:9;
s . k =
s /. k
by A14, A15, FINSEQ_4:15
.=
pow (
x,
((i - j) * (k - 1)))
by A9, A13, A14, A15
.=
pow (
x,
((i - j) * (k -' 1)))
by A16, XREAL_0:def 2
.=
pow (
(pow (x,(i - j))),
(k -' 1))
by A4, Th26
.=
(pow (x,(i - j))) |^ (k -' 1)
by Def2
;
hence
s . k = (pow (x,(i - j))) |^ (k -' 1)
;
verum
end;
then Sum s =
((1. L) - ((pow (x,(i - j))) |^ (len s))) / ((1. L) - (pow (x,(i - j))))
by A1, A2, A3, Th5, Th32
.=
((1. L) - ((pow (x,(i - j))) |^ m)) / ((1. L) - (pow (x,(i - j))))
by A7, FINSEQ_1:def 3
.=
((1. L) - (pow ((pow (x,(i - j))),m))) / ((1. L) - (pow (x,(i - j))))
by Def2
.=
((1. L) - (pow (x,((i - j) * m)))) / ((1. L) - (pow (x,(i - j))))
by A4, Th26
.=
(0. L) / ((1. L) - r)
by A5, A12, VECTSP_1:19
.=
0. L
;
hence
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
by A2, A3, A9, A13, Th37; verum