let n be non zero Nat; for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime & len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & k1 . 1 is_expressible_by n & k1 . 2 is_expressible_by n & k1 . 3 is_expressible_by n & k1 . 4 is_expressible_by n & k2 . 1 = INV_MOD ((k1 . 1),n) & k2 . 2 = NEG_MOD ((k1 . 2),n) & k2 . 3 = NEG_MOD ((k1 . 3),n) & k2 . 4 = INV_MOD ((k1 . 4),n) holds
IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m
let m, k1, k2 be FinSequence of NAT ; ( (2 to_power n) + 1 is prime & len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & k1 . 1 is_expressible_by n & k1 . 2 is_expressible_by n & k1 . 3 is_expressible_by n & k1 . 4 is_expressible_by n & k2 . 1 = INV_MOD ((k1 . 1),n) & k2 . 2 = NEG_MOD ((k1 . 2),n) & k2 . 3 = NEG_MOD ((k1 . 3),n) & k2 . 4 = INV_MOD ((k1 . 4),n) implies IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m )
assume that
A1:
(2 to_power n) + 1 is prime
and
A2:
len m >= 4
and
A3:
m . 1 is_expressible_by n
and
A4:
m . 2 is_expressible_by n
and
A5:
m . 3 is_expressible_by n
and
A6:
m . 4 is_expressible_by n
and
A7:
k1 . 1 is_expressible_by n
and
A8:
k1 . 2 is_expressible_by n
and
A9:
k1 . 3 is_expressible_by n
and
A10:
k1 . 4 is_expressible_by n
and
A11:
k2 . 1 = INV_MOD ((k1 . 1),n)
and
A12:
k2 . 2 = NEG_MOD ((k1 . 2),n)
and
A13:
k2 . 3 = NEG_MOD ((k1 . 3),n)
and
A14:
k2 . 4 = INV_MOD ((k1 . 4),n)
; IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m
A15:
k2 . 4 is_expressible_by n
by A1, A10, A14, Def10;
2 <= len m
by A2, XXREAL_0:2;
then
2 in Seg (len m)
by FINSEQ_1:1;
then A16:
2 in dom m
by FINSEQ_1:def 3;
Seg (len m) = dom m
by FINSEQ_1:def 3;
then A17:
4 in dom m
by A2, FINSEQ_1:1;
1 <= len m
by A2, XXREAL_0:2;
then
1 in Seg (len m)
by FINSEQ_1:1;
then A18:
1 in dom m
by FINSEQ_1:def 3;
3 <= len m
by A2, XXREAL_0:2;
then
3 in Seg (len m)
by FINSEQ_1:1;
then A19:
3 in dom m
by FINSEQ_1:def 3;
consider I1 being FinSequence of NAT such that
A20:
I1 = IDEAoperationA (m,k1,n)
;
consider I2 being FinSequence of NAT such that
A21:
I2 = IDEAoperationA (I1,k2,n)
;
A22:
k2 . 1 is_expressible_by n
by A1, A7, A11, Def10;
A23:
now for j being Nat st j in Seg (len m) holds
I2 . j = m . jlet j be
Nat;
( j in Seg (len m) implies I2 . j = m . j )assume A24:
j in Seg (len m)
;
I2 . j = m . jthen
j in Seg (len I1)
by A20, Def11;
then A25:
j in dom I1
by FINSEQ_1:def 3;
A26:
j in dom m
by A24, FINSEQ_1:def 3;
now I2 . j = m . jper cases
( j = 1 or j = 2 or j = 3 or j = 4 or ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) )
;
suppose A27:
j = 1
;
I2 . j = m . jhence I2 . j =
MUL_MOD (
(I1 . 1),
(k2 . 1),
n)
by A21, A25, Def11
.=
MUL_MOD (
(MUL_MOD ((m . 1),(k1 . 1),n)),
(k2 . 1),
n)
by A20, A18, Def11
.=
MUL_MOD (
(m . 1),
(MUL_MOD ((k1 . 1),(k2 . 1),n)),
n)
by A1, A3, A7, A22, Th23
.=
MUL_MOD (1,
(m . 1),
n)
by A1, A7, A11, Def10
.=
m . j
by A3, A27, Th22
;
verum end; suppose A28:
j = 2
;
I2 . j = m . jhence I2 . j =
ADD_MOD (
(I1 . 2),
(k2 . 2),
n)
by A21, A25, Def11
.=
ADD_MOD (
(ADD_MOD ((m . 2),(k1 . 2),n)),
(k2 . 2),
n)
by A20, A16, Def11
.=
ADD_MOD (
(m . 2),
(ADD_MOD ((k1 . 2),(k2 . 2),n)),
n)
by Th14
.=
ADD_MOD (
0,
(m . 2),
n)
by A8, A12, Th11
.=
m . j
by A4, A28, Th13
;
verum end; suppose A29:
j = 3
;
I2 . j = m . jhence I2 . j =
ADD_MOD (
(I1 . 3),
(k2 . 3),
n)
by A21, A25, Def11
.=
ADD_MOD (
(ADD_MOD ((m . 3),(k1 . 3),n)),
(k2 . 3),
n)
by A20, A19, Def11
.=
ADD_MOD (
(m . 3),
(ADD_MOD ((k1 . 3),(k2 . 3),n)),
n)
by Th14
.=
ADD_MOD (
0,
(m . 3),
n)
by A9, A13, Th11
.=
m . j
by A5, A29, Th13
;
verum end; suppose A30:
j = 4
;
I2 . j = m . jhence I2 . j =
MUL_MOD (
(I1 . 4),
(k2 . 4),
n)
by A21, A25, Def11
.=
MUL_MOD (
(MUL_MOD ((m . 4),(k1 . 4),n)),
(k2 . 4),
n)
by A20, A17, Def11
.=
MUL_MOD (
(m . 4),
(MUL_MOD ((k1 . 4),(k2 . 4),n)),
n)
by A1, A6, A10, A15, Th23
.=
MUL_MOD (1,
(m . 4),
n)
by A1, A10, A14, Def10
.=
m . j
by A6, A30, Th22
;
verum end; end; end; hence
I2 . j = m . j
;
verum end;
A32:
Seg (len m) = dom m
by FINSEQ_1:def 3;
Seg (len m) =
Seg (len I1)
by A20, Def11
.=
Seg (len I2)
by A21, Def11
.=
dom I2
by FINSEQ_1:def 3
;
hence
IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m
by A20, A21, A32, A23, FINSEQ_1:13; verum