defpred S1[ Nat] means for m, k, f, ie being Nat st ie is_represented_by $1,k & f > 0 holds
for e being Tuple of $1,NAT st e = DecSD2 ie,$1,k holds
(Pow_mod m,e,f,k) . $1 = (m |^ ie) mod f;
A1:
S1[1]
proof
let m,
k,
f,
ie be
Nat;
:: thesis: ( ie is_represented_by 1,k & f > 0 implies for e being Tuple of 1,NAT st e = DecSD2 ie,1,k holds
(Pow_mod m,e,f,k) . 1 = (m |^ ie) mod f )
assume A2:
(
ie is_represented_by 1,
k &
f > 0 )
;
:: thesis: for e being Tuple of 1,NAT st e = DecSD2 ie,1,k holds
(Pow_mod m,e,f,k) . 1 = (m |^ ie) mod f
let e be
Tuple of 1,
NAT ;
:: thesis: ( e = DecSD2 ie,1,k implies (Pow_mod m,e,f,k) . 1 = (m |^ ie) mod f )
assume A3:
e = DecSD2 ie,1,
k
;
:: thesis: (Pow_mod m,e,f,k) . 1 = (m |^ ie) mod f
ie < (Radix k) |^ 1
by A2, RADIX_1:def 12;
then A4:
ie < Radix k
by NEWTON:10;
A5:
1
- 1
= 0
;
A6:
1
in Seg 1
by FINSEQ_1:4, TARSKI:def 1;
len (DecSD2 ie,1,k) = 1
by FINSEQ_1:def 18;
then
1
in dom (DecSD2 ie,1,k)
by A6, FINSEQ_1:def 3;
then e /. 1 =
(DecSD2 ie,1,k) . 1
by A3, PARTFUN1:def 8
.=
DigitDC2 ie,1,
k
by A6, Def5
.=
(ie mod ((Radix k) |^ 1)) div ((Radix k) |^ 0 )
by A5, XREAL_0:def 2
.=
(ie mod ((Radix k) |^ 1)) div 1
by NEWTON:9
.=
ie mod ((Radix k) |^ 1)
by NAT_2:6
.=
ie mod (Radix k)
by NEWTON:10
.=
ie
by A4, NAT_D:24
;
then
(m |^ ie) mod f = Table2 m,
e,
f,1
;
hence
(Pow_mod m,e,f,k) . 1
= (m |^ ie) mod f
by Def9;
:: thesis: verum
end;
A7:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume A8:
(
n >= 1 &
S1[
n] )
;
:: thesis: S1[n + 1]
A9:
n + 1
>= 1
by NAT_1:12;
let m,
k,
f,
ie be
Nat;
:: thesis: ( ie is_represented_by n + 1,k & f > 0 implies for e being Tuple of (n + 1),NAT st e = DecSD2 ie,(n + 1),k holds
(Pow_mod m,e,f,k) . (n + 1) = (m |^ ie) mod f )
assume A10:
(
ie is_represented_by n + 1,
k &
f > 0 )
;
:: thesis: for e being Tuple of (n + 1),NAT st e = DecSD2 ie,(n + 1),k holds
(Pow_mod m,e,f,k) . (n + 1) = (m |^ ie) mod f
let e be
Tuple of
(n + 1),
NAT ;
:: thesis: ( e = DecSD2 ie,(n + 1),k implies (Pow_mod m,e,f,k) . (n + 1) = (m |^ ie) mod f )
assume A11:
e = DecSD2 ie,
(n + 1),
k
;
:: thesis: (Pow_mod m,e,f,k) . (n + 1) = (m |^ ie) mod f
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
deffunc H1(
Nat)
-> Element of
NAT =
e . ($1 + 1);
consider en being
FinSequence of
NAT such that A12:
len en = n
and A13:
for
i being
Nat st
i in dom en holds
en . i = H1(
i)
from FINSEQ_2:sch 1();
A14:
dom en = Seg n
by A12, FINSEQ_1:def 3;
reconsider en =
en as
Tuple of
n,
NAT by A12, FINSEQ_2:110;
A15:
1
in Seg 1
by FINSEQ_1:4, TARSKI:def 1;
then A16:
1
in Seg (1 + n)
by FINSEQ_2:9;
A17:
n in Seg n
by A8, FINSEQ_1:3;
A18:
n + 1
in Seg (n + 1)
by A9, FINSEQ_1:3;
A19:
for
i being
Element of
NAT st
i in Seg n holds
(Pow_mod m,en,f,k) . i = (Pow_mod m,e,f,k) . i
proof
defpred S2[
Element of
NAT ]
means ( $1
in Seg n implies
(Pow_mod m,en,f,k) . $1
= (Pow_mod m,e,f,k) . $1 );
A20:
S2[
0 ]
by FINSEQ_1:3;
A21:
for
i being
Element of
NAT st
S2[
i] holds
S2[
i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S2[i] implies S2[i + 1] )
assume A22:
(
i in Seg n implies
(Pow_mod m,en,f,k) . i = (Pow_mod m,e,f,k) . i )
;
:: thesis: S2[i + 1]
assume A23:
i + 1
in Seg n
;
:: thesis: (Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)
then A24:
( 1
<= i + 1 &
i + 1
<= n )
by FINSEQ_1:3;
then A25:
(i + 1) - 1
<= n - 1
by XREAL_1:11;
A26:
(
i = 0 or
i + 1
> 1
+ 0 )
by XREAL_1:8;
A27:
dom en = Seg n
by A12, FINSEQ_1:def 3;
A28:
dom e = Seg (len e)
by FINSEQ_1:def 3;
then A29:
dom e = Seg (n + 1)
by FINSEQ_1:def 18;
now per cases
( i = 0 or i >= 1 )
by A26, NAT_1:13;
case A30:
i = 0
;
:: thesis: (Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)then (Pow_mod m,en,f,k) . (i + 1) =
Table2 m,
en,
f,
n
by A8, Def9
.=
(m |^ (en . n)) mod f
by A17, A27, PARTFUN1:def 8
.=
(m |^ (e . (n + 1))) mod f
by A13, A17, A14
.=
Table2 m,
e,
f,
(n + 1)
by A18, A29, PARTFUN1:def 8
.=
(Pow_mod m,e,f,k) . 1
by A9, Def9
;
hence
(Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)
by A30;
:: thesis: verum end; case A31:
i >= 1
;
:: thesis: (Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)reconsider nn =
n - 1 as
Element of
NAT by A8, INT_1:18;
A32:
( 1
<= i &
i <= nn + 1 )
by A25, A31, NAT_1:12;
then A33:
( 1
<= i &
i <= (n + 1) - 1 )
;
A34:
ex
I1,
I2 being
Nat st
(
I1 = (Pow_mod m,en,f,k) . i &
I2 = (Pow_mod m,en,f,k) . (i + 1) &
I2 = (((I1 |^ (Radix k)) mod f) * (Table2 m,en,f,(n -' i))) mod f )
by A8, A25, A31, Def9;
A35:
ex
I1,
I2 being
Nat st
(
I1 = (Pow_mod m,e,f,k) . i &
I2 = (Pow_mod m,e,f,k) . (i + 1) &
I2 = (((I1 |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' i))) mod f )
by A9, A33, Def9;
(1 + i) - i <= n - i
by A24, XREAL_1:11;
then A36:
1
<= n -' i
by A32, XREAL_1:235;
n -' i <= n
by NAT_D:35;
then A37:
n -' i in Seg n
by A36, FINSEQ_1:3;
then A38:
n -' i in dom en
by A12, FINSEQ_1:def 3;
A39:
(n + 1) -' i <= n + 1
by NAT_D:35;
i + 1
<= n
by A23, FINSEQ_1:3;
then
(i + 1) - 1
<= n - 1
by XREAL_1:11;
then
(n + 1) -' i >= (n + 1) -' nn
by NAT_D:41;
then
(n + 1) -' i >= (n + 1) - (n - 1)
by XREAL_0:def 2;
then
1
<= (n + 1) -' i
by XXREAL_0:2;
then
(n + 1) -' i in Seg (n + 1)
by A39, FINSEQ_1:3;
then A40:
(n + 1) -' i in dom e
by A28, FINSEQ_1:def 18;
(Pow_mod m,en,f,k) . (i + 1) =
(((((Pow_mod m,e,f,k) . i) |^ (Radix k)) mod f) * ((m |^ (en . (n -' i))) mod f)) mod f
by A22, A32, A34, A38, FINSEQ_1:3, PARTFUN1:def 8
.=
(((((Pow_mod m,e,f,k) . i) |^ (Radix k)) mod f) * ((m |^ (e . ((n -' i) + 1))) mod f)) mod f
by A13, A37, A14
.=
(((((Pow_mod m,e,f,k) . i) |^ (Radix k)) mod f) * ((m |^ (e . ((n + 1) -' i))) mod f)) mod f
by A32, NAT_D:38
.=
(((((Pow_mod m,e,f,k) . i) |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' i))) mod f
by A40, PARTFUN1:def 8
;
hence
(Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)
by A35;
:: thesis: verum end;
hence
(Pow_mod m,en,f,k) . (i + 1) = (Pow_mod m,e,f,k) . (i + 1)
;
:: thesis: verum
end;
for
i being
Element of
NAT holds
S2[
i]
from NAT_1:sch 1(A20, A21);
hence
for
i being
Element of
NAT st
i in Seg n holds
(Pow_mod m,en,f,k) . i = (Pow_mod m,e,f,k) . i
;
:: thesis: verum
end;
A41:
n in Seg n
by A8, FINSEQ_1:5;
set ien =
SDDec2 en,
k;
A42:
ie = ((SDDec2 en,k) * (Radix k)) + (e /. 1)
proof
reconsider r2 =
Radix k as
Element of
REAL by XREAL_0:def 1;
deffunc H2(
Nat)
-> Element of
NAT =
(DigitSD2 en,k) . $1;
consider rD being
FinSequence of
REAL such that A43:
len rD = n
and A44:
for
i being
Nat st
i in dom rD holds
rD . i = H2(
i)
from FINSEQ_2:sch 1();
reconsider rD =
rD as
Tuple of
n,
REAL by A43, FINSEQ_2:110;
A46:
dom (DigitSD2 en,k) =
Seg (len (DigitSD2 en,k))
by FINSEQ_1:def 3
.=
Seg n
by FINSEQ_1:def 18
;
A47:
dom rD = Seg n
by A43, FINSEQ_1:def 3;
A48:
1
- 1
= 0
;
A49:
DigitSD2 e,
k = <*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))
proof
A50:
len (DigitSD2 e,k) = n + 1
by FINSEQ_1:def 18;
A51:
len ((Radix k) * (DigitSD2 en,k)) =
len (r2 * rD)
by A44, A46, A47, FINSEQ_1:17
.=
n
by FINSEQ_1:def 18
;
A52:
len <*(SubDigit2 e,1,k)*> = 1
by FINSEQ_1:56;
A53:
len (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) =
(len <*(SubDigit2 e,1,k)*>) + (len ((Radix k) * (DigitSD2 en,k)))
by FINSEQ_1:35
.=
n + 1
by A51, FINSEQ_1:def 18
;
then A54:
len (DigitSD2 e,k) = len (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k)))
by FINSEQ_1:def 18;
for
i being
Nat st 1
<= i &
i <= len (DigitSD2 e,k) holds
(DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i
proof
let i be
Nat;
:: thesis: ( 1 <= i & i <= len (DigitSD2 e,k) implies (DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i )
assume A55:
( 1
<= i &
i <= len (DigitSD2 e,k) )
;
:: thesis: (DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i
then A56:
i <= n + 1
by FINSEQ_1:def 18;
then A57:
i in Seg (n + 1)
by A55, FINSEQ_1:3;
then A58:
i in dom (DigitSD2 e,k)
by A50, FINSEQ_1:def 3;
per cases
( i = 1 or i <> 1 )
;
suppose A59:
i = 1
;
:: thesis: (DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . ithen (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i =
SubDigit2 e,1,
k
by FINSEQ_1:58
.=
(DigitSD2 e,k) /. 1
by A16, Def2
.=
(DigitSD2 e,k) . 1
by A58, A59, PARTFUN1:def 8
;
hence
(DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i
by A59;
:: thesis: verum end; suppose A60:
i <> 1
;
:: thesis: (DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i
1
- 1
<= i - 1
by A55, XREAL_1:11;
then reconsider i1 =
i - 1 as
Element of
NAT by INT_1:16;
1
< i
by A55, A60, XXREAL_0:1;
then
1
+ 1
<= i
by INT_1:20;
then A61:
(1 + 1) - 1
<= i - 1
by XREAL_1:11;
A62:
i - 1
<= (n + 1) - 1
by A56, XREAL_1:11;
then A63:
i1 in Seg n
by A61, FINSEQ_1:3;
A64:
i1 in dom rD
by A47, A61, A62, FINSEQ_1:3;
reconsider rs =
rD . (i - 1) as
Real ;
reconsider rs2 =
(DigitSD2 en,k) . (i - 1) as
Element of
NAT ;
1
< i
by A55, A60, XXREAL_0:1;
then (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i =
((Radix k) * (DigitSD2 en,k)) . (i - 1)
by A52, A53, A56, FINSEQ_1:37
.=
(r2 * rD) . (i - 1)
by A44, A46, A47, FINSEQ_1:17
.=
r2 * rs
by RVSUM_1:67
.=
(Radix k) * rs2
by A44, A46, A47, FINSEQ_1:17
.=
(Radix k) * ((DigitSD2 en,k) /. i1)
by A46, A47, A64, PARTFUN1:def 8
.=
(Radix k) * (SubDigit2 en,i1,k)
by A63, Def2
.=
((Radix k) * ((Radix k) |^ (i1 -' 1))) * (en . i1)
.=
((Radix k) |^ ((i1 -' 1) + 1)) * (en . i1)
by NEWTON:11
.=
((Radix k) |^ i1) * (en . i1)
by A61, XREAL_1:237
.=
((Radix k) |^ i1) * (e . (i1 + 1))
by A13, A63, A14
.=
SubDigit2 e,
i,
k
by A55, XREAL_1:235
.=
(DigitSD2 e,k) /. i
by A57, Def2
;
hence
(DigitSD2 e,k) . i = (<*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))) . i
by A58, PARTFUN1:def 8;
:: thesis: verum
end;
hence
DigitSD2 e,
k = <*(SubDigit2 e,1,k)*> ^ ((Radix k) * (DigitSD2 en,k))
by A54, FINSEQ_1:18;
:: thesis: verum
end;
dom e = Seg (len e)
by FINSEQ_1:def 3;
then A65:
1
in dom e
by A16, FINSEQ_1:def 18;
ie =
SDDec2 e,
k
by A10, A11, Th15, NAT_1:12
.=
(SubDigit2 e,1,k) + (Sum ((Radix k) * (DigitSD2 en,k)))
by A49, RVSUM_1:106
.=
(SubDigit2 e,1,k) + (Sum (r2 * rD))
by A44, A46, A47, FINSEQ_1:17
.=
(SubDigit2 e,1,k) + (r2 * (Sum rD))
by RVSUM_1:117
.=
(SubDigit2 e,1,k) + ((Radix k) * (SDDec2 en,k))
by A44, A46, A47, FINSEQ_1:17
.=
(((Radix k) |^ 0 ) * (e . 1)) + ((Radix k) * (SDDec2 en,k))
by A48, XREAL_0:def 2
.=
(1 * (e . 1)) + ((Radix k) * (SDDec2 en,k))
by NEWTON:9
;
hence
ie = ((SDDec2 en,k) * (Radix k)) + (e /. 1)
by A65, PARTFUN1:def 8;
:: thesis: verum
end;
then A66:
ie >= (SDDec2 en,k) * (Radix k)
by INT_1:19;
A67:
Radix k > 0
by Th6;
ie < (Radix k) |^ (n + 1)
by A10, RADIX_1:def 12;
then
(SDDec2 en,k) * (Radix k) < (Radix k) |^ (n + 1)
by A66, XXREAL_0:2;
then
(SDDec2 en,k) * (Radix k) < ((Radix k) |^ n) * (Radix k)
by NEWTON:11;
then
SDDec2 en,
k < (Radix k) |^ n
by XREAL_1:66;
then A68:
SDDec2 en,
k is_represented_by n,
k
by RADIX_1:def 12;
A69:
en = DecSD2 (SDDec2 en,k),
n,
k
proof
A70:
len en = len (DecSD2 (SDDec2 en,k),n,k)
by A12, FINSEQ_1:def 18;
for
i being
Nat st 1
<= i &
i <= len en holds
en . i = (DecSD2 (SDDec2 en,k),n,k) . i
proof
let i be
Nat;
:: thesis: ( 1 <= i & i <= len en implies en . i = (DecSD2 (SDDec2 en,k),n,k) . i )
assume A71:
( 1
<= i &
i <= len en )
;
:: thesis: en . i = (DecSD2 (SDDec2 en,k),n,k) . i
then A72:
i in Seg n
by A12, FINSEQ_1:3;
( 1
<= i + 1 &
i + 1
<= n + 1 )
by A12, A71, XREAL_1:8, XREAL_1:31;
then A73:
i + 1
in Seg (n + 1)
by FINSEQ_1:3;
A74:
e . 1 =
DigitDC2 ie,1,
k
by A11, A16, Def5
.=
(ie mod ((Radix k) |^ 1)) div ((Radix k) |^ 0 )
by XREAL_1:234
.=
(ie mod ((Radix k) |^ 1)) div 1
by NEWTON:9
.=
ie mod ((Radix k) |^ 1)
by NAT_2:6
.=
ie mod (Radix k)
by NEWTON:10
;
dom e = Seg (len e)
by FINSEQ_1:def 3;
then A75:
dom e = Seg (n + 1)
by FINSEQ_1:def 18;
A76:
( 1
<= i + 1 &
0 < Radix k )
by A71, Th6, XREAL_1:31;
A77:
(
Radix k <> 0 &
i <> 0 )
by A71, Th6;
A78:
((e . 1) + ((SDDec2 en,k) * (Radix k))) div (Radix k) =
[\(((e . 1) + ((SDDec2 en,k) * (Radix k))) / (Radix k))/]
by INT_1:def 7
.=
[\(((e . 1) / (Radix k)) + (SDDec2 en,k))/]
by A76, XCMPLX_1:114
.=
[\((e . 1) / (Radix k))/] + (SDDec2 en,k)
by INT_1:51
.=
((e . 1) div (Radix k)) + (SDDec2 en,k)
by INT_1:def 7
.=
0 + (SDDec2 en,k)
by A67, A74, NAT_D:1, NAT_D:27
;
en . i =
e . (i + 1)
by A13, A72, A14
.=
DigitDC2 ie,
(i + 1),
k
by A11, A73, Def5
.=
((((SDDec2 en,k) * (Radix k)) + (e /. 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k)
by A42, A76, Th4
.=
((((SDDec2 en,k) * (Radix k)) + (e . 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k)
by A15, A75, FINSEQ_2:9, PARTFUN1:def 8
.=
((((SDDec2 en,k) * (Radix k)) + (e . 1)) div ((Radix k) |^ i)) mod (Radix k)
by NAT_D:34
.=
((((SDDec2 en,k) * (Radix k)) + (e . 1)) div ((Radix k) * ((Radix k) |^ (i -' 1)))) mod (Radix k)
by A77, PEPIN:27
.=
((((e . 1) + ((SDDec2 en,k) * (Radix k))) div (Radix k)) div ((Radix k) |^ (i -' 1))) mod (Radix k)
by NAT_2:29
.=
DigitDC2 (SDDec2 en,k),
i,
k
by A71, A76, A78, Th4
;
hence
en . i = (DecSD2 (SDDec2 en,k),n,k) . i
by A72, Def5;
:: thesis: verum
end;
hence
en = DecSD2 (SDDec2 en,k),
n,
k
by A70, FINSEQ_1:18;
:: thesis: verum
end;
A79:
n <= (n + 1) - 1
;
n + 1
>= 1
by NAT_1:11;
then
ex
I1,
I2 being
Nat st
(
I1 = (Pow_mod m,e,f,k) . n &
I2 = (Pow_mod m,e,f,k) . (n + 1) &
I2 = (((I1 |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' n))) mod f )
by A8, A79, Def9;
then (Pow_mod m,e,f,k) . (n + 1) =
(((((Pow_mod m,en,f,k) . n) |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' n))) mod f
by A19, A41
.=
(((((m |^ (SDDec2 en,k)) mod f) |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' n))) mod f
by A8, A10, A68, A69
.=
((((m |^ (SDDec2 en,k)) |^ (Radix k)) mod f) * (Table2 m,e,f,((n + 1) -' n))) mod f
by PEPIN:12
.=
(((m |^ (SDDec2 en,k)) |^ (Radix k)) * (Table2 m,e,f,((n + 1) -' n))) mod f
by EULER_2:10
.=
((m |^ ((SDDec2 en,k) * (Radix k))) * (Table2 m,e,f,((n + 1) -' n))) mod f
by NEWTON:14
.=
((m |^ ((SDDec2 en,k) * (Radix k))) * ((m |^ (e /. 1)) mod f)) mod f
by NAT_D:34
.=
((m |^ ((SDDec2 en,k) * (Radix k))) * (m |^ (e /. 1))) mod f
by EULER_2:9
.=
(m |^ (((SDDec2 en,k) * (Radix k)) + (e /. 1))) mod f
by NEWTON:13
;
hence
(Pow_mod m,e,f,k) . (n + 1) = (m |^ ie) mod f
by A42;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A1, A7);
hence
for n being Nat st n >= 1 holds
for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds
for e being Tuple of n,NAT st e = DecSD2 ie,n,k holds
(Pow_mod m,e,f,k) . n = (m |^ ie) mod f
; :: thesis: verum