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