let a, n, m be Element of NAT ; :: thesis: ( a <> 0 & 1 < m implies ALGO_BPOW (a,n,m) = (a to_power n) mod m )
assume AS: ( a <> 0 & 1 < m ) ; :: thesis: ALGO_BPOW (a,n,m) = (a to_power n) mod m
consider A, B being sequence of NAT such that
ASC: ( ALGO_BPOW (a,n,m) = B . (LenBSeq n) & A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) ) by Def1;
set NBS = Nat2BL . n;
Nat2BL . n = (LenBSeq n) -BinarySequence n by BINARI_6:def 2;
then reconsider NBS = Nat2BL . n as Tuple of LenBSeq n, BOOLEAN ;
defpred S₁[ Nat] means ( $1 < LenBSeq n implies ex SUBBS being Tuple of $1 + 1, BOOLEAN st
( SUBBS = (Nat2BL . n) | ($1 + 1) & B . ($1 + 1) = (a to_power (Absval SUBBS)) mod m ) );
LC1: S₁[ 0 ]

proof

reconsider NBS0 = NBS | (0 + 1) as Tuple of 1, BOOLEAN ;
PCJJ: B . (0 + 1) = BinBranch ((B . 0),(((B . 0) * (A . 0)) mod m),((Nat2BL . n) . (0 + 1))) by ASC;
then PCC0: B . 1 = BinBranch (1,(a mod m),((Nat2BL . n) . 1)) by NAT_D:73, ASC;

per cases ( NBS0 = <*TRUE*> or NBS0 = <*FALSE*> ) by BINARITH:14;

suppose LCT: NBS0 = <*TRUE*> ; :: thesis: S₁[ 0 ]

then LCT1: Absval NBS0 = 1 by BINARITH:16;
<*(NBS . 1)*> . 1 = <*TRUE*> . 1 by FINSEQ_5:20, LCT;
then B . 1 = (a to_power 1) mod m by defBB, PCC0, XBOOLEAN:def 2;
hence S₁[ 0 ] by LCT1; :: thesis: verum

end;

suppose LCF: NBS0 = <*FALSE*> ; :: thesis: S₁[ 0 ]

then LCF1: Absval NBS0 = 0 by BINARITH:15;
<*(NBS . 1)*> . 1 = <*FALSE*> . 1 by FINSEQ_5:20, LCF;
then B . 1 = 1 by defBB, ASC, PCJJ, XBOOLEAN:def 1
.= 1 mod m by NAT_D:14, AS
.= (a to_power 0) mod m by POWER:24 ;
hence S₁[ 0 ] by LCF1; :: thesis: verum

end;

end;

end;

LC2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume ASPi: S₁[i] ; :: thesis: S₁[i + 1]
assume I1: i + 1 < LenBSeq n ; :: thesis: ex SUBBS being Tuple of (i + 1) + 1, BOOLEAN st
( SUBBS = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS)) mod m )
i < LenBSeq n

proof

assume COV: i >= LenBSeq n ; :: thesis: contradiction
(i + 1) - 1 < (LenBSeq n) - 0 by I1, XREAL_1:14;
hence contradiction by COV; :: thesis: verum

end;

then consider SUBBS being Tuple of i + 1, BOOLEAN such that
CLa: ( SUBBS = (Nat2BL . n) | (i + 1) & B . (i + 1) = (a to_power (Absval SUBBS)) mod m ) by ASPi;
set j = i + 1;
thus ex SUBBS1 being Tuple of (i + 1) + 1, BOOLEAN st
( SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m ) :: thesis: verum

proof

LINT: (i + 1) + 1 <= LenBSeq n by INT_1:7, I1;
1 <= (i + 1) + 1 by NAT_1:11;
then (i + 1) + 1 in Seg (LenBSeq n) by LINT;
then CHO: (i + 1) + 1 in dom NBS by FINSEQ_1:89;
set SUBBS1 = (Nat2BL . n) | ((i + 1) + 1);
Lhyo: (i + 1) + 1 <= len NBS by FINSEQ_3:153, LINT;
Sho: (Nat2BL . n) | ((i + 1) + 1) is Element of BOOLEAN * by FINSEQ_1:def 11;
len ((Nat2BL . n) | ((i + 1) + 1)) = min (((i + 1) + 1),(len NBS)) by FINSEQ_2:21;
then len ((Nat2BL . n) | ((i + 1) + 1)) = (i + 1) + 1 by Lhyo, XXREAL_0:def 9;
then (Nat2BL . n) | ((i + 1) + 1) in ((i + 1) + 1) -tuples_on BOOLEAN by Sho;
then reconsider SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) as Tuple of (i + 1) + 1, BOOLEAN ;
set BC = IFEQ ((NBS . ((i + 1) + 1)),FALSE,0,(2 to_power (i + 1)));
CCL2: SUBBS1 = SUBBS ^ <*(NBS . ((i + 1) + 1))*> by FINSEQ_5:10, CLa, CHO;
PO: NBS . ((i + 1) + 1) is Element of BOOLEAN by FINSEQ_1:84, CHO;
reconsider X = NBS . ((i + 1) + 1) as Nat ;
ZZ: Absval SUBBS1 = (Absval SUBBS) + (IFEQ ((NBS . ((i + 1) + 1)),FALSE,0,(2 to_power (i + 1)))) by BINARITH:20, CCL2, PO;
LMT1: B . ((i + 1) + 1) = BinBranch ((B . (i + 1)),(((B . (i + 1)) * (A . (i + 1))) mod m),X) by ASC;
take SUBBS1 ; :: thesis: ( SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m )
thus SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) ; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m
thus B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m :: thesis: verum

proof

per cases ( X = 0 or X <> 0 ) ;

suppose LPP: X = 0 ; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

then IFEQ ((NBS . ((i + 1) + 1)),FALSE,0,(2 to_power (i + 1))) = 0 by FUNCOP_1:def 8, XBOOLEAN:def 1;
hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by ZZ, CLa, LMT1, defBB, LPP; :: thesis: verum

end;

suppose LPP1: X <> 0 ; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

then B . ((i + 1) + 1) = ((B . (i + 1)) * (A . (i + 1))) mod m by LMT1, defBB
.= (a to_power ((Absval SUBBS) + (2 to_power (i + 1)))) mod m by CBPOW2, ASC, AS, CLa ;
hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by FUNCOP_1:def 8, XBOOLEAN:def 1, LPP1, ZZ; :: thesis: verum

end;

end;

end;

end;

end;

LC3: for i being Nat holds S₁[i] from NAT_1:sch 2(LC1, LC2);
(LenBSeq n) - 1 in NAT by INT_1:5, NAT_1:14;
then reconsider fs = (LenBSeq n) - 1 as Nat ;
consider FSBS being Tuple of fs + 1, BOOLEAN such that
Lcfs: ( FSBS = (Nat2BL . n) | (fs + 1) & B . (fs + 1) = (a to_power (Absval FSBS)) mod m ) by LC3, XREAL_1:44;
reconsider FSBS = FSBS as Tuple of LenBSeq n, BOOLEAN ;
dom NBS = Seg (LenBSeq n) by FINSEQ_1:89;
hence ALGO_BPOW (a,n,m) = (a to_power n) mod m by ASC, BINARI_6:10, Lcfs; :: thesis: verum