environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, XCMPLX_0, INT_2, NAT_3, XXREAL_0, XBOOLE_0, NEWTON, ARYTM_3, ARYTM_1, NAT_1, RELAT_1, CARD_1, ABIAN, SUBSET_1, FINSET_1, FINSEQ_1, FUNCT_1, FINSEQ_3, TARSKI, CARD_3, ORDINAL4, FUNCT_2, FINSEQ_2, FUNCOP_1, MOEBIUS1, COMPLEX1, INT_1, REALSET1, SQUARE_1, INT_5, ZFMISC_1, POWER, REAL_1, PRE_POLY, UPROOTS, BHSP_5, CLASSES1, PARTFUN1, RFUNCT_3, BINOP_2, PROB_1, WAYBEL29, MSSUBFAM, TOPGEN_1, EULER_1, NAT_5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCOP_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, FINSEQ_1, FINSEQ_3, EXTREAL1, XCMPLX_0, XREAL_0, NAT_1, INT_1, INT_2, NAT_D, RVSUM_1, REAL_1, SQUARE_1, XXREAL_0, NEWTON, FINSEQ_2, ABIAN, PEPIN, INT_5, FINSEQOP, ENUMSET1, FINSET_1, COMPLEX1, NAT_3, DOMAIN_1, POWER, MOEBIUS1, BHSP_5, EULER_1, WSIERP_1, BINOP_1, RECDEF_1, UPROOTS, BINOP_2, FUNCT_3, RFUNCT_3, CLASSES1, PRE_POLY;
definitions TARSKI;
theorems XBOOLE_0, XBOOLE_1, XXREAL_0, XREAL_1, XCMPLX_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, INT_1, INT_2, INT_4, INT_5, NEWTON, EULER_1, EULER_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, RVSUM_1, WSIERP_1, ORDINAL1, IDEA_1, INT_6, FIB_NUM3, POWER, PEPIN, SQUARE_1, CARD_1, CARD_2, ZFMISC_1, FINSEQ_4, JGRAPH_1, TARSKI, COMPLEX1, ABSVALUE, MOEBIUS1, CARD_3, MESFUNC3, FUNCT_2, EXTREAL1, FINSEQOP, FUNCOP_1, BAGORDER, RELSET_1, WELLORD2, PARTFUN1, BHSP_5, UPROOTS, RFINSEQ, BINOP_2, BINOP_1, FUNCT_3, RFUNCT_3, NAT_4, NAT_3, XREAL_0, ABIAN, ENUMSET1, MONOID_1, CLASSES1, PRE_POLY, XTUPLE_0, NUMBERS;
schemes NAT_1, FUNCT_1, FUNCT_2, BINOP_2, FINSEQ_1;
registrations XBOOLE_0, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RVSUM_1, VALUED_0, NEWTON, ABIAN, FUNCT_1, ZFMISC_1, SUBSET_1, MOEBIUS1, FUNCT_2, PRE_CIRC, RELAT_1, SQUARE_1, CARD_1, PREPOWER, NAT_3, PRE_POLY, ORDINAL1;
constructors HIDDEN, WELLORD2, REAL_1, NAT_D, BINOP_2, WSIERP_1, ABIAN, EULER_1, PEPIN, INT_5, RECDEF_1, MOEBIUS1, FINSEQOP, EXTREAL1, UPROOTS, NAT_3, REALSET1, POWER, BHSP_5, CALCUL_2, SUPINF_1, RFUNCT_3, CLASSES1, BINOP_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities NEWTON, FINSEQ_1, FINSEQ_3, EULER_1, MOEBIUS1, CARD_1, ORDINAL1;
expansions TARSKI, FINSEQ_1;
Lm1:
for p being Nat
for n0, m0 being non zero Nat st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0))
theorem Th1:
for
n being
Nat holds 2
|^ (n + 1) < (2 |^ (n + 2)) - 1
Lm2:
for n, m, l being Nat holds {n,m,l} is finite Subset of NAT
Lm3:
for k, n, m, l being Nat holds {n,m,l,k} is finite Subset of NAT
theorem Th20:
for
l,
p,
n1,
n2 being
Nat st
0 <> l &
p > l &
p > n1 &
p > n2 &
(l * n1) mod p = (l * n2) mod p &
p is
prime holds
n1 = n2
Lm4:
for k, m being Nat holds
( k < m iff k <= m - 1 )
Lm5:
for a being Element of NAT
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
Lm6:
for a being Element of NAT
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
Lm7:
for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
Lm8:
for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Product (Del (ft,a))) * (ft . a) = Product ft
Lm9:
for n being Nat st n + 2 is prime holds
for l being Nat st l in Seg n & l <> 1 holds
ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
Lm10:
for n being Nat
for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds
ex k being Nat st
( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds
(Product f) mod (n + 2) = 1
Lm11:
for I being set
for f, g being Function of I,NAT
for J, K being finite Subset of I
for j being object st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))