let s be Nat; for k being non zero Nat st k <= s holds
(Problem58Solution s) . k = ((sequenceQk s) . k) |^ (primenumber (k - 1))
let k be non zero Nat; ( k <= s implies (Problem58Solution s) . k = ((sequenceQk s) . k) |^ (primenumber (k - 1)) )
assume A1:
k <= s
; (Problem58Solution s) . k = ((sequenceQk s) . k) |^ (primenumber (k - 1))
set p = primenumber (k - 1);
set AnPk = sequenceAnPk (s,k);
len (sequenceAnPk (s,k)) = s
by A1, Def10;
then reconsider AnPk = sequenceAnPk (s,k) as s -element natural-valued FinSequence by CARD_1:def 7;
set Ak1Pk = sequenceAk1Pk s;
set I = idseq s;
set A = sequenceA s;
set Qk = sequenceQk s;
set F = (idseq s) to_power AnPk;
A2:
len ((idseq s) to_power AnPk) = s
by CARD_1:def 7;
then A3:
dom ((idseq s) to_power AnPk) = Seg s
by FINSEQ_1:def 3;
1 <= k
by NAT_1:14;
then A4:
k in dom ((idseq s) to_power AnPk)
by A1, A2, FINSEQ_3:25;
(sequenceAk1Pk s) . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1))
by A1, Def9;
then
((sequenceAk1Pk s) . k) * (primenumber (k - 1)) = ((sequenceA s) . k) + 1
by XCMPLX_1:87;
then A5:
(k |^ ((sequenceAk1Pk s) . k)) |^ (primenumber (k - 1)) = k |^ (((sequenceA s) . k) + 1)
by NEWTON:9;
(idseq s) to_power AnPk is FinSequence of REAL
by FINSEQ_1:102;
then A6:
(Product ((idseq s) to_power AnPk)) |^ (primenumber (k - 1)) = Product (((idseq s) to_power AnPk) |^ (primenumber (k - 1)))
by NAT_3:15;
A7:
len (((idseq s) to_power AnPk) |^ (primenumber (k - 1))) = len ((idseq s) to_power AnPk)
by NAT_3:def 1;
A8:
len ((idseq s) to_power (sequenceA s)) = s
by CARD_1:def 7;
A9:
1 <= k
by NAT_1:14;
then A10:
k in dom (((idseq s) to_power AnPk) |^ (primenumber (k - 1)))
by A1, A2, A7, FINSEQ_3:25;
then A11:
(((idseq s) to_power AnPk) |^ (primenumber (k - 1))) . k = (((idseq s) to_power AnPk) . k) |^ (primenumber (k - 1))
by NAT_3:def 1;
A12:
(idseq s) . k = k
by A3, A4, FINSEQ_2:49;
A13:
((idseq s) to_power AnPk) . k = ((idseq s) . k) to_power (AnPk . k)
by A4, Def6;
A14:
AnPk . k = 0
by A1, Def10;
A15:
k |^ 0 = 1
by NEWTON:4;
len (sequenceA s) = s
by Def5;
then A16:
dom (sequenceA s) = Seg s
by FINSEQ_1:def 3;
dom ((idseq s) to_power (sequenceA s)) = (dom (idseq s)) /\ (dom (sequenceA s))
by Def6;
then A17: ((idseq s) to_power (sequenceA s)) . k =
k to_power ((sequenceA s) . k)
by A3, A4, A12, A16, Def6
.=
(k |^ ((sequenceA s) . k)) * ((((idseq s) to_power AnPk) |^ (primenumber (k - 1))) . k)
by A12, A11, A13, A14, A15
;
for j being Nat st j in dom (((idseq s) to_power AnPk) |^ (primenumber (k - 1))) & k <> j holds
((idseq s) to_power (sequenceA s)) . j = (((idseq s) to_power AnPk) |^ (primenumber (k - 1))) . j
then A18:
Product ((idseq s) to_power (sequenceA s)) = (k |^ ((sequenceA s) . k)) * ((Product ((idseq s) to_power AnPk)) |^ (primenumber (k - 1)))
by A6, A7, A8, A10, A17, Th4, CARD_1:def 7;
thus (Problem58Solution s) . k =
k * (numberQ s)
by A1, A9, Th48
.=
(k * (k |^ ((sequenceA s) . k))) * ((Product ((idseq s) to_power AnPk)) |^ (primenumber (k - 1)))
by A18
.=
((k |^ ((sequenceAk1Pk s) . k)) |^ (primenumber (k - 1))) * ((Product ((idseq s) to_power AnPk)) |^ (primenumber (k - 1)))
by A5, NEWTON:6
.=
((k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power AnPk))) |^ (primenumber (k - 1))
by NEWTON:7
.=
((sequenceQk s) . k) |^ (primenumber (k - 1))
by A1, Def11
; verum