environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, CARD_1, RELAT_1, ARYTM_3, XXREAL_0, ARYTM_1, NEWTON, FINSEQ_1, RADIX_1, POWER, FINSEQ_2, PARTFUN1, FUNCT_1, CARD_3, ORDINAL4, SUBSET_1, TARSKI, REAL_1, RADIX_2, FUNCT_7;
notations HIDDEN, TARSKI, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, NAT_D, FUNCT_1, POWER, PARTFUN1, FINSEQ_1, FINSEQ_2, NEWTON, RVSUM_1, GR_CY_1, WSIERP_1, RADIX_1, SUBSET_1, RECDEF_1;
definitions TARSKI;
theorems NAT_1, NAT_2, INT_1, FINSEQ_1, PREPOWER, POWER, RVSUM_1, FINSEQ_2, TARSKI, FUNCT_1, PEPIN, RADIX_1, EULER_2, NEWTON, INT_2, XCMPLX_1, XREAL_1, XXREAL_0, XREAL_0, NAT_D, ORDINAL1, PARTFUN1, CARD_1;
schemes NAT_1, FINSEQ_2, RECDEF_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, FINSEQ_2, FINSEQ_1;
constructors HIDDEN, REAL_1, NAT_D, NEWTON, POWER, BINARITH, WSIERP_1, GR_CY_1, RADIX_1, RECDEF_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
definition
let n,
k be
Nat;
let x be
Tuple of
n,
NAT ;
existence
ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 (x,i,k)
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 /. i = SubDigit2 (x,i,k) ) holds
b1 = b2
end;
definition
let k,
n,
x be
Nat;
existence
ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 . i = DigitDC2 (x,i,k)
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 . i = DigitDC2 (x,i,k) ) holds
b1 = b2
end;
definition
let q be
Integer;
let k,
f,
n be
Nat;
let c be
Tuple of
n,
k -SD ;
assume A1:
n >= 1
;
func Mul_mod (
q,
c,
f,
k)
-> Tuple of
n,
INT means :
Def7:
(
it . 1
= Table1 (
q,
c,
f,
n) & ( for
i being
Nat st 1
<= i &
i <= n - 1 holds
ex
I1,
I2 being
Integer st
(
I1 = it . i &
I2 = it . (i + 1) &
I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) );
existence
ex b1 being Tuple of n, INT st
( b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) )
uniqueness
for b1, b2 being Tuple of n, INT st b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & b2 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b2 . i & I2 = b2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) holds
b1 = b2
end;
::
deftheorem Def7 defines
Mul_mod RADIX_2:def 7 :
for q being Integer
for k, f, n being Nat
for c being Tuple of n,k -SD st n >= 1 holds
for b6 being Tuple of n, INT holds
( b6 = Mul_mod (q,c,f,k) iff ( b6 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b6 . i & I2 = b6 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) );
definition
let k,
f,
m,
n be
Nat;
let e be
Tuple of
n,
NAT ;
assume A1:
n >= 1
;
func Pow_mod (
m,
e,
f,
k)
-> Tuple of
n,
NAT means :
Def9:
(
it . 1
= Table2 (
m,
e,
f,
n) & ( for
i being
Nat st 1
<= i &
i <= n - 1 holds
ex
i1,
i2 being
Nat st
(
i1 = it . i &
i2 = it . (i + 1) &
i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) );
existence
ex b1 being Tuple of n, NAT st
( b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) )
uniqueness
for b1, b2 being Tuple of n, NAT st b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & b2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b2 . i & i2 = b2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) holds
b1 = b2
end;
::
deftheorem Def9 defines
Pow_mod RADIX_2:def 9 :
for k, f, m, n being Nat
for e being Tuple of n, NAT st n >= 1 holds
for b6 being Tuple of n, NAT holds
( b6 = Pow_mod (m,e,f,k) iff ( b6 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b6 . i & i2 = b6 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) );
theorem
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