defpred S₁[ 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 & S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume that
A2: n >= 1 and
A3: S₁[n] ; :: thesis:
let m, k, f, ie be Nat; :: thesis:
A4: n + 1 >= 1 by NAT_1:12;
assume that
A5: ie is_represented_by n + 1,k and
A6: f > 0 ; :: thesis:
let e be Tuple of n + 1, NAT ; :: thesis:
assume A7: e = DecSD2 (ie,(n + 1),k) ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( 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 = H₁(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)

A16: len <*(SubDigit2 (e,1,k))*> = 1 by FINSEQ_1:39;
deffunc H₂( 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 = H₂(i) from FINSEQ_2:sch 1();
A19: for i being Nat st i in dom rD holds
rD . i = (DigitSD2 (en,k)) . i

proof

let i be Nat; :: thesis:
assume i in dom rD ; :: thesis:
then rD . i = H₂(i) by A18;
hence rD . i = (DigitSD2 (en,k)) . i ; :: thesis:

end;

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; :: thesis:
assume that
A26: 1 <= i and
A27: i <= len (DigitSD2 (e,k)) ; :: thesis:
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 ;

suppose A31: i = 1 ; :: thesis:

then (<*(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; :: thesis:

end;

suppose A32: i <> 1 ; :: thesis:

reconsider 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; :: thesis:

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; :: thesis:

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 S₂[ 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 S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A44: ( i in Seg n implies (Pow_mod (m,en,f,k)) . i = (Pow_mod (m,e,f,k)) . i ) ; :: thesis:
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 ; :: thesis:
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 :: thesis:

per cases by A45, NAT_1:13;

case A52: i = 0 ; :: thesis:

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; :: thesis:

end;

case A53: i >= 1 ; :: thesis:

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; :: thesis:

end;

hence (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1) ; :: thesis:

end;

A60: S₂[ 0 ] by FINSEQ_1:1;
for i being Nat holds S₂[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 ; :: thesis:

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; :: thesis:
assume that
A68: 1 <= i and
A69: i <= len en ; :: thesis:
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; :: thesis:

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; :: thesis:

end;

A74: S₁[1]

proof

let m, k, f, ie be Nat; :: thesis:
assume that
A75: ie is_represented_by 1,k and
f > 0 ; :: thesis:
ie < (Radix k) |^ 1 by A75, RADIX_1:def 12;
then A76: ie < Radix k ;
let e be Tuple of 1, NAT ; :: thesis:
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) ; :: thesis:
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; :: thesis:

end;

for n being Nat st n >= 1 holds
S₁[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 ; :: thesis: