environ
vocabularies HIDDEN, NUMBERS, NEWTON, NAT_1, ARYTM_3, RELAT_1, INT_2, XXREAL_0, INT_1, ARYTM_1, ABIAN, CARD_1, EULER_1, INT_7, GRAPH_1, FINSET_1, GROUP_1, SUBSET_1, GROUP_4, STRUCT_0, GROUP_2, INT_5, UNIROOTS, INT_3, XBOOLE_0, ALGSTR_0, BINOP_2, REALSET1, FUNCT_7, BINOP_1, VECTSP_2, SUPINF_2, MESFUNC1, POLYNOM1, HURWITZ, POLYNOM2, AFINSQ_1, POLYNOM5, POLYNOM3, TARSKI, FUNCT_1, FINSEQ_1, GR_CY_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, INT_2, NAT_D, XXREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_7, BINOP_1, NAT_1, GROUP_2, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_4, VFUNCT_1, GR_CY_1, VECTSP_1, VECTSP_2, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, NEWTON, EULER_1, INT_3, HURWITZ, REALSET1, INT_5, INT_7, ABIAN, UNIROOTS;
definitions GROUP_1, TARSKI;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, FUNCT_2, VECTSP_1, INT_1, RLVECT_1, GR_CY_1, NAT_1, INT_2, PEPIN, NAT_D, XCMPLX_1, WSIERP_1, CARD_1, GROUP_1, GROUP_2, WELLORD2, XREAL_1, NEWTON, XXREAL_0, GROUP_4, POLYNOM4, POLYNOM5, CARD_2, EULER_1, XBOOLE_1, INT_7, NAT_2, INT_4, INT_6, INT_5, NAT_4, RADIX_2, PREPOWER, UNIROOTS, GR_CY_2, SUBSET_1;
schemes NAT_1, FUNCT_2, RECDEF_1;
registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_2, FINSET_1, GR_CY_1, VECTSP_1, INT_3, XXREAL_0, RELAT_1, CARD_1, ALGSTR_1, POLYNOM3, POLYNOM4, POLYNOM5, WSIERP_1, NEWTON, INT_7, VFUNCT_1, FUNCT_2;
constructors HIDDEN, REAL_1, NAT_D, EUCLID, REALSET1, GROUP_4, GR_CY_1, INT_3, BINARITH, POLYNOM4, POLYNOM5, WELLORD2, ALGSTR_1, HURWITZ, UPROOTS, INT_5, EULER_1, INT_7, ABIAN, UNIROOTS, RELSET_1, VFUNCT_1, ALGSEQ_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, GROUP_1, INT_3, POLYNOM3, HURWITZ, INT_7, CARD_1, ORDINAL1;
expansions STRUCT_0, TARSKI;
theorem Th1:
for
p,
q being
Prime for
k being
Nat holds
( not
k divides p * q or
k = 1 or
k = p or
k = q or
k = p * q )
Lm1:
for p being Nat st p > 2 holds
(2 * p) + 1 > 5
Lm2:
2 |^ 2 = 4
Lm3:
2 |^ 3 = 8
Lm4:
2 |^ 4 = 16
Lm5:
2 |^ 8 = 256
Lm6:
for a, p being Nat st p > 1 & (a |^ p) - 1 is Prime holds
a > 1
Lm7:
for n being Nat
for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
Lm8:
for n being Nat
for a being Integer st n <> 0 holds
ex an being Nat st an,a are_congruent_mod n
Lm9:
for a, b, n, x being Nat st a,b are_congruent_mod n & n <> 0 holds
a |^ x,b |^ x are_congruent_mod n
Lm10:
for F being commutative Skew-Field
for G being Subgroup of MultGroup F
for n being Nat st 0 < n holds
ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1. F) ) )
Lm11:
for F being commutative Skew-Field
for G being Subgroup of MultGroup F
for a, b being Element of G
for n being Nat st G is finite & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})