let p be prime odd Nat; for m being positive Nat ex u being Element of INT.Ring st ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)
let m be positive Nat; ex u being Element of INT.Ring st ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)
set Gf = 'G' (f_0 (m,p));
set D = Der1 INT.Ring;
A1:
1 < p
by INT_2:def 4;
then
1 + 1 <= p
by INT_1:7;
then A3:
p - 2 = p -' 2
by XREAL_1:233;
len (f_0 (m,p)) =
len (~ (f_0 (m,p)))
.=
(m * p) + p
by Th12
;
then A5:
len ('G' (f_0 (m,p))) = (m * p) + p
by E_TRANS1:def 8;
then A6:
( 1 <= p & p <= len ('G' (f_0 (m,p))) )
by INT_2:def 4, XREAL_1:38;
then A7:
p in dom ('G' (f_0 (m,p)))
by FINSEQ_3:25;
set p1 = p -' 1;
p -' 1 <= len ('G' (f_0 (m,p)))
by NAT_D:35, XREAL_1:38, A5;
then A8:
len (('G' (f_0 (m,p))) | (p -' 1)) = p -' 1
by FINSEQ_1:59;
then A9:
dom (('G' (f_0 (m,p))) | (p -' 1)) = Seg (p -' 1)
by FINSEQ_1:def 3;
A10:
dom (('G' (f_0 (m,p))) | (p -' 1)) = dom ((p -' 1) |-> (0. INT.Ring))
by A8, FINSEQ_1:def 3;
A11:
eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring)) = (p -' 1) |-> (0. INT.Ring)
proof
for
k being
Nat st
k in dom (eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) holds
(eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) . k = ((p -' 1) |-> (0. INT.Ring)) . k
proof
let k be
Nat;
( k in dom (eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) implies (eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) . k = ((p -' 1) |-> (0. INT.Ring)) . k )
assume A12:
k in dom (eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring)))
;
(eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) . k = ((p -' 1) |-> (0. INT.Ring)) . k
then A13:
k in dom (('G' (f_0 (m,p))) | (p -' 1))
by E_TRANS1:def 7;
A14:
k in Seg (p -' 1)
by A12, E_TRANS1:def 7, A9;
then A15:
( 1
<= k &
k <= p -' 1 )
by FINSEQ_1:1;
then A17:
k -' 1
= k - 1
by XREAL_1:233;
p -' 1
<= len ('G' (f_0 (m,p)))
by NAT_D:35, XREAL_1:38, A5;
then
( 1
<= k &
k <= len ('G' (f_0 (m,p))) )
by A15, XXREAL_0:2;
then A16:
k in dom ('G' (f_0 (m,p)))
by FINSEQ_3:25;
A18:
(p -' 1) - 1 =
(p - 1) - 1
by A1, XREAL_1:233
.=
p - 2
;
k in dom (('G' (f_0 (m,p))) | (p -' 1))
by A12, E_TRANS1:def 7;
then (('G' (f_0 (m,p))) | (p -' 1)) /. k =
(('G' (f_0 (m,p))) | (p -' 1)) . k
by PARTFUN1:def 6
.=
('G' (f_0 (m,p))) . k
by FUNCT_1:49, A14
.=
((Der1 INT.Ring) |^ (k -' 1)) . (f_0 (m,p))
by A16, E_TRANS1:def 8
;
then (eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) . k =
eval (
(~ (((Der1 INT.Ring) |^ (k -' 1)) . (f_0 (m,p)))),
(0. INT.Ring))
by A13, E_TRANS1:def 7
.=
0. INT.Ring
by A18, A3, A17, A15, XREAL_1:9, Th22
.=
((p -' 1) |-> (0. INT.Ring)) . k
;
hence
(eval ((('G' (f_0 (m,p))) | (p -' 1)),(0. INT.Ring))) . k = ((p -' 1) |-> (0. INT.Ring)) . k
;
verum
end;
hence
eval (
(('G' (f_0 (m,p))) | (p -' 1)),
(0. INT.Ring))
= (p -' 1) |-> (0. INT.Ring)
by E_TRANS1:def 7, A10;
verum
end;
'G' (f_0 (m,p)) =
((('G' (f_0 (m,p))) | (p -' 1)) ^ <*(('G' (f_0 (m,p))) . p)*>) ^ (('G' (f_0 (m,p))) /^ p)
by A6, FINSEQ_5:84
.=
((('G' (f_0 (m,p))) | (p -' 1)) ^ <*(('G' (f_0 (m,p))) /. p)*>) ^ (('G' (f_0 (m,p))) /^ p)
by A7, PARTFUN1:def 6
.=
(('G' (f_0 (m,p))) | (p -' 1)) ^ (<*(('G' (f_0 (m,p))) /. p)*> ^ (('G' (f_0 (m,p))) /^ p))
by FINSEQ_1:32
;
then A20: Sum ('G' (f_0 (m,p))) =
(Sum (('G' (f_0 (m,p))) | (p -' 1))) + (Sum (<*(('G' (f_0 (m,p))) /. p)*> ^ (('G' (f_0 (m,p))) /^ p)))
by RLVECT_1:41
.=
(Sum (('G' (f_0 (m,p))) | (p -' 1))) + ((Sum <*(('G' (f_0 (m,p))) /. p)*>) + (Sum (('G' (f_0 (m,p))) /^ p)))
by RLVECT_1:41
;
A21: (Eval (~ (^ (Sum (('G' (f_0 (m,p))) | (p -' 1)))))) . 0 =
Sum ((p -' 1) |-> (0. INT.Ring))
by A11, E_TRANS1:30
.=
0. INT.Ring
by MATRIX_3:11
;
A22:
dom <*(('G' (f_0 (m,p))) /. p)*> = Seg 1
by FINSEQ_1:38;
then
1 in dom <*(('G' (f_0 (m,p))) /. p)*>
;
then A23: (eval (<*(('G' (f_0 (m,p))) /. p)*>,(0. INT.Ring))) . 1 =
eval ((~ (<*(('G' (f_0 (m,p))) /. p)*> /. 1)),(0. INT.Ring))
by E_TRANS1:def 7
.=
eval ((~ (('G' (f_0 (m,p))) /. p)),(0. INT.Ring))
by FINSEQ_4:16
;
A25: ('G' (f_0 (m,p))) /. p =
('G' (f_0 (m,p))) . p
by A7, PARTFUN1:def 6
.=
((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p))
by A7, E_TRANS1:def 8
;
dom (eval (<*(('G' (f_0 (m,p))) /. p)*>,(0. INT.Ring))) = {1}
by A22, E_TRANS1:def 7, FINSEQ_1:2;
then
rng (eval (<*(('G' (f_0 (m,p))) /. p)*>,(0. INT.Ring))) = {(eval ((~ (('G' (f_0 (m,p))) /. p)),(0. INT.Ring)))}
by A23, FUNCT_1:4;
then
eval (<*(('G' (f_0 (m,p))) /. p)*>,(0. INT.Ring)) = <*(eval ((~ (('G' (f_0 (m,p))) /. p)),(0. INT.Ring)))*>
by FINSEQ_1:38, A22, E_TRANS1:def 7;
then A26: (Eval (~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>)))) . 0 =
Sum <*(eval ((~ (('G' (f_0 (m,p))) /. p)),(0. INT.Ring)))*>
by E_TRANS1:30
.=
eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring))
by A25, BINOM:3
.=
((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
by Th23
;
A27:
p < len ('G' (f_0 (m,p)))
by XREAL_1:39, A5;
then len (('G' (f_0 (m,p))) /^ p) =
(len ('G' (f_0 (m,p)))) - p
by RFINSEQ:def 1
.=
m * p
by A5
;
then A29:
dom (('G' (f_0 (m,p))) /^ p) = Seg (m * p)
by FINSEQ_1:def 3;
for j being Nat st j in dom (eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) holds
(eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) . j in {(In ((p !),INT.Ring))} -Ideal
proof
let j be
Nat;
( j in dom (eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) implies (eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) . j in {(In ((p !),INT.Ring))} -Ideal )
assume A30:
j in dom (eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring)))
;
(eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) . j in {(In ((p !),INT.Ring))} -Ideal
then A31:
j in dom (('G' (f_0 (m,p))) /^ p)
by E_TRANS1:def 7;
A32:
j in Seg (m * p)
by A29, A30, E_TRANS1:def 7;
then A33:
( 1
<= j &
j <= m * p )
by FINSEQ_1:1;
then A34:
j + p <= (m * p) + p
by XREAL_1:6;
1
<= j + p
by A33, XREAL_1:38;
then
j + p in Seg (len ('G' (f_0 (m,p))))
by A5, A34;
then A35:
j + p in dom ('G' (f_0 (m,p)))
by FINSEQ_1:def 3;
set jp =
j + p;
A36:
(j + p) -' 1
= (j + p) - 1
by A33, XREAL_1:38, XREAL_1:233;
1
<= j
by A32, FINSEQ_1:1;
then A38:
0 + p <= (j - 1) + p
by XREAL_1:6;
then consider w being
Integer such that A39:
((j + p) -' 1) ! = (p !) * w
by INT_1:def 3, A36, NUMBER08:6;
reconsider w0 =
w as
Element of
INT.Ring by INT_1:def 2;
A40:
In (
(((j + p) -' 1) !),
INT.Ring)
= (In ((p !),INT.Ring)) * w0
by A39;
set t9 =
(~ (Product (x. (m,p)))) . (((j + p) -' 1) -' (p -' 1));
(('G' (f_0 (m,p))) /^ p) /. j =
(('G' (f_0 (m,p))) /^ p) . j
by A31, PARTFUN1:def 6
.=
('G' (f_0 (m,p))) . (p + j)
by A27, A31, RFINSEQ:def 1
.=
((Der1 INT.Ring) |^ ((j + p) -' 1)) . (f_0 (m,p))
by A35, E_TRANS1:def 8
;
then
eval (
(~ ((('G' (f_0 (m,p))) /^ p) /. j)),
(0. INT.Ring))
= (((j + p) -' 1) !) * ((~ (Product (x. (m,p)))) . (((j + p) -' 1) -' (p -' 1)))
by A36, A38, Th24;
then
eval (
(~ ((('G' (f_0 (m,p))) /^ p) /. j)),
(0. INT.Ring))
= (In ((((j + p) -' 1) !),INT.Ring)) * ((~ (Product (x. (m,p)))) . (((j + p) -' 1) -' (p -' 1)))
by Lm1;
then A43:
eval (
(~ ((('G' (f_0 (m,p))) /^ p) /. j)),
(0. INT.Ring))
in {(In ((((j + p) -' 1) !),INT.Ring))} -Ideal
by RING_2:18, GCD_1:def 1;
{(In ((((j + p) -' 1) !),INT.Ring))} -Ideal c= {(In ((p !),INT.Ring))} -Ideal
by A40, GCD_1:def 1, RING_2:19;
then
eval (
(~ ((('G' (f_0 (m,p))) /^ p) /. j)),
(0. INT.Ring))
in {(In ((p !),INT.Ring))} -Ideal
by A43;
hence
(eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) . j in {(In ((p !),INT.Ring))} -Ideal
by A31, E_TRANS1:def 7;
verum
end;
then A45:
Sum (eval ((('G' (f_0 (m,p))) /^ p),(0. INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal
by E_TRANS1:3;
(Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) . 0 in {(In ((p !),INT.Ring))} -Ideal
by A45, E_TRANS1:30;
then
(Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) . 0 in { ((In ((p !),INT.Ring)) * r) where r is Element of INT.Ring : verum }
by IDEAL_1:64;
then consider u being Element of INT.Ring such that
A46:
(Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) . 0 = (In ((p !),INT.Ring)) * u
;
A47:
^ ((Sum (('G' (f_0 (m,p))) | (p -' 1))) + ((Sum <*(('G' (f_0 (m,p))) /. p)*>) + (Sum (('G' (f_0 (m,p))) /^ p)))) = (^ (Sum (('G' (f_0 (m,p))) | (p -' 1)))) + (^ ((Sum <*(('G' (f_0 (m,p))) /. p)*>) + (Sum (('G' (f_0 (m,p))) /^ p))))
by E_TRANS1:27;
A48:
^ ((Sum <*(('G' (f_0 (m,p))) /. p)*>) + (Sum (('G' (f_0 (m,p))) /^ p))) = (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>)) + (^ (Sum (('G' (f_0 (m,p))) /^ p)))
by E_TRANS1:27;
~ (^ (Sum ('G' (f_0 (m,p))))) =
(~ (^ (Sum (('G' (f_0 (m,p))) | (p -' 1))))) + (~ (^ ((Sum <*(('G' (f_0 (m,p))) /. p)*>) + (Sum (('G' (f_0 (m,p))) /^ p)))))
by A20, A47, POLYNOM3:def 10
.=
(~ (^ (Sum (('G' (f_0 (m,p))) | (p -' 1))))) + ((~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))))
by A48, POLYNOM3:def 10
;
then
Eval (~ (^ (Sum ('G' (f_0 (m,p)))))) = (Eval (~ (^ (Sum (('G' (f_0 (m,p))) | (p -' 1)))))) + (Eval ((~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))))
by POLYDIFF:55;
then A50: (Eval (~ (^ (Sum ('G' (f_0 (m,p))))))) . 0 =
(0. INT.Ring) + ((Eval ((~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))))) . 0)
by A21, VALUED_1:1
.=
(Eval ((~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))))) . 0
;
(Eval ((~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))))) . 0 =
((Eval (~ (^ (Sum <*(('G' (f_0 (m,p))) /. p)*>)))) + (Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))))) . 0
by POLYDIFF:55
.=
(((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)
by A46, A26, VALUED_1:1
;
hence
ex u being Element of INT.Ring st ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)
by A50; verum