environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NEWTON, INT_1, SUBSET_1, ARYTM_1, ABIAN, TARSKI, XBOOLE_0, INT_2, NAT_1, EC_PF_2, INT_7, INT_5, INT_3, PEPIN, SQUARE_1, ZFMISC_1, GRAPH_1, GROUP_1, ALGSTR_0, FUNCT_7, FUNCT_1, BINOP_2, XCMPLX_0, NAT_6;
notations HIDDEN, SUBSET_1, TARSKI, XBOOLE_0, ORDINAL1, STRUCT_0, NUMBERS, CARD_1, XCMPLX_0, XREAL_0, ALGSTR_0, GR_CY_1, INT_5, INT_1, ABIAN, SQUARE_1, GROUP_1, PEPIN, NAT_3, BINOP_1, MEMBERED, INT_2, INT_3, EC_PF_2, INT_7, NAT_D, XXREAL_0, NEWTON;
definitions NAT_1, NAT_2, NAT_D, INT_1, NEWTON, EC_PF_2, XREAL_0, XCMPLX_0, ALGSTR_0, INT_3, INT_7;
theorems ABIAN, INT_1, INT_2, NAT_1, NAT_2, NEWTON, XREAL_1, XCMPLX_0, XCMPLX_1, XXREAL_0, NAT_4, ORDINAL1, PEPIN, SQUARE_1, EC_PF_2, INT_3, XBOOLE_0, NAT_D, INT_5, INT_7, GROUP_1, GR_CY_1, EULER_1, ALGSTR_0, TARSKI;
schemes NAT_1;
registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, NAT_2, NAT_3, SQUARE_1, INT_7, ABIAN, STRUCT_0, RELSET_1;
constructors HIDDEN, REAL_1, NAT_D, POWER, DOMAIN_1, ABIAN, PEPIN, NAT_3, NUMBERS, NAT_4, NEWTON, EC_PF_2, SUBSET_1, ALGSTR_0, INT_5, INT_7, XXREAL_0, GROUP_1, GR_CY_1, BINOP_2, RELSET_1, XTUPLE_0, BINOP_1, INT_3;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities NEWTON, NAT_1, NAT_2, INT_1, INT_2, SQUARE_1;
expansions NEWTON, NAT_1, NAT_2, INT_1, INT_2, EC_PF_2, TARSKI, MEMBERED, ABIAN, SQUARE_1, XCMPLX_0;
Lm1:
for n being natural even number holds (- 1) |^ n = 1
Lm2:
for n being natural odd number holds (- 1) |^ n = - 1
Lm3:
for a being natural number
for b being integer number st a divides b holds
a gcd b = a
Lm4:
for a being integer number
for p being natural prime number holds Lege (a,p) = Leg (a,p)
Lm5:
1 is odd
Lm6:
3 is Proth
Lm7:
9 is Proth