environ
vocabularies HIDDEN, ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2, INT_1, SQUARE_1, SEQ_1, NUMPOLY1, REALSET1, SERIES_1, POWER, SEQ_2, ASYMPT_1, FUNCT_7, CARD_1, EUCLID_3, GR_CY_3, ABIAN, TOPGEN_1, FINSET_1, TARSKI, PYTHTRIP, EC_PF_2, NEWTON, XXREAL_0, ORDINAL4, XBOOLE_0, REAL_1, INT_2, NAT_1, XREAL_0, CARD_3, XCMPLX_0, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, VALUED_1, ZFMISC_1, SQUARE_1, INT_1, INT_2, XREAL_0, FUNCT_1, FINSET_1, FINSEQ_1, FUNCOP_1, NEWTON, NAT_D, SEQ_1, SEQ_2, FINSEQ_2, RVSUM_1, SERIES_1, POWER, ABIAN, PYTHTRIP, PEPIN, GR_CY_3, NAT_5, EC_PF_2;
definitions ORDINAL1, TARSKI, XBOOLE_0, FUNCT_2;
theorems FINSEQ_2, RVSUM_1, XCMPLX_1, ORDINAL1, SQUARE_1, NAT_1, POWER, NEWTON, XREAL_1, FINSEQ_1, RELAT_1, XREAL_0, SEQ_2, SERIES_1, SEQ_4, SEQ_1, XXREAL_0, INT_2, PEPIN, NAT_D, POLYEQ_3, VALUED_1, INT_1, INT_4, GR_CY_3, NAT_5, PYTHTRIP, ABIAN, NAT_2, CHORD, EC_PF_2, SUBSET_1, TARSKI, XBOOLE_0;
schemes NAT_1, SEQ_1, FINSEQ_2, NAT_2;
registrations RELSET_1, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, RVSUM_1, XXREAL_0, NAT_2, NEWTON, SEQ_1, XCMPLX_0, NUMBERS, SEQ_2, POWER, ABIAN, PYTHTRIP, SQUARE_1, ORDINAL1, XBOOLE_0, FUNCT_2, VALUED_0, VALUED_1;
constructors HIDDEN, SEQ_1, COMSEQ_2, GR_CY_3, NAT_5, ABIAN, EC_PF_2, MOEBIUS1, RVSUM_1, SERIES_1, SEQ_2, REAL_1, PEPIN, POLYEQ_3, RELSET_1, NAT_D, PYTHTRIP, FINSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM;
equalities POWER, NEWTON, SERIES_1, SQUARE_1, GR_CY_3, XBOOLE_0;
expansions ORDINAL1;
Lm1:
for n being Integer holds n * (n - 1) is even
Lm2:
for n being Integer holds n * (n + 1) is even
theorem Th3:
for
n being
Nat holds
not not
n mod 5
= 0 & ... & not
n mod 5
= 4
theorem Th8:
for
n being
Nat holds
not not
n mod 10
= 0 & ... & not
n mod 10
= 9
Lm3:
0 - 1 < 0
;
Lm4:
for s being non trivial Nat holds PolygonalNumbers s is Subset of NAT
;