environ
vocabularies HIDDEN, NUMBERS, INT_1, NAT_1, SUBSET_1, EQREL_1, EULER_1, FINSEQ_1, INT_4, MEMBER_1, TARSKI, REAL_1, ARYTM_3, FUNCT_1, RELAT_1, FINSET_1, CARD_1, XBOOLE_0, ARYTM_1, INT_2, XXREAL_0, COMPLEX1, NEWTON, SQUARE_1, PARTFUN1, INT_8, PEPIN, INT_5, POLYEQ_3, ABIAN, CARD_3, ORDINAL4, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_1, INT_2, NAT_D, FUNCT_1, FINSEQ_1, RELSET_1, EULER_1, TREES_4, EQREL_1, PARTFUN1, FINSET_1, WSIERP_1, NEWTON, MEMBER_1, ABIAN, PEPIN, INT_4, INT_5, POLYEQ_3;
definitions TARSKI, XBOOLE_0;
theorems ORDINAL1, NAT_1, NAT_2, INT_1, INT_2, FINSEQ_1, CARD_2, INT_5, EULER_1, EULER_2, NEWTON, XCMPLX_1, XREAL_1, RELAT_1, ABIAN, STIRL2_1, XXREAL_0, NAT_D, PEPIN, NAT_4, WSIERP_1, FINSEQ_3, INT_4, PYTHTRIP, ABSVALUE, FINSEQ_2, FINSEQ_4, FUNCT_1, MEMBER_1, FINSEQ_5, XBOOLE_1, XREAL_0, SEQ_2, XBOOLE_0, EQREL_1, NUMBERS, RVSUM_1;
schemes NAT_1, FINSEQ_1, FINSEQ_2;
registrations RELAT_1, FINSEQ_1, CARD_1, NAT_1, INT_1, MEMBERED, FINSET_1, NEWTON, NAT_3, XXREAL_0, NUMBERS, XBOOLE_0, XREAL_0, ORDINAL1, VALUED_0, ABIAN, MEMBER_1, XCMPLX_0, WSIERP_1, INT_4;
constructors HIDDEN, EULER_1, WSIERP_1, PEPIN, NAT_3, NAT_D, INTEGRA2, RELSET_1, ABIAN, INT_4, INT_5, POLYEQ_3;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, FINSEQ_1, EULER_1, POLYEQ_3;
expansions TARSKI, XBOOLE_0;
Lm1:
for x being Integer holds 2 divides x * (x + 1)
Lm2:
for m, n, k being Nat st k <= n holds
m |^ k divides m |^ n
by NEWTON:89;
theorem Th17:
for
s,
t,
n being
Nat st
n > 1 &
s,
n are_coprime &
t,
n are_coprime &
order (
s,
n),
order (
t,
n)
are_coprime holds
order (
(s * t),
n)
= (order (s,n)) * (order (t,n))
theorem
for
s,
t,
n being
Nat st
n > 1 &
s,
n are_coprime &
t,
n are_coprime &
order (
(s * t),
n)
= (order (s,n)) * (order (t,n)) holds
order (
s,
n),
order (
t,
n)
are_coprime
Lm3:
for X being finite set st card X = 0 holds
X = {}
;