environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, CARD_1, CARD_3, ARYTM_3, ARYTM_1, NUMBERS, XXREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, INT_2, BINOP_2, ORDINAL4, FINSEQ_1, VALUED_1, FINSOP_1, NEWTON, RFINSEQ, ABIAN, AFINSQ_1, AFINSQ_2, FIB_NUM2, JORDAN3, NUMERAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSET_1, CARD_1, SETWISEO, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, RAT_1, MEMBERED, VALUED_0, INT_2, NAT_D, BINOP_2, FINSEQ_1, RECDEF_1, VALUED_1, FINSOP_1, NEWTON, ABIAN, SERIES_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STIRL2_1, FIB_NUM2, NUMERAL1;
definitions TARSKI, FUNCT_1, STIRL2_1, FIB_NUM2, XBOOLE_0, AFINSQ_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, XXREAL_0, XREAL_0, XREAL_1, NAT_1, INT_1, VALUED_0, INT_2, NAT_D, BINOP_2, CARD_2, VALUED_1, NEWTON, ABIAN, WSIERP_1, EULER_1, AFINSQ_1, PEPIN, AFINSQ_2, STIRL2_1, NAT_4, FIB_NUM2, NUMERAL1, CARD_FIN, XCMPLX_1;
schemes NAT_1, AFINSQ_2, STIRL2_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, ORDINAL3, FINSET_1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, BINOP_2, FINSEQ_1, VALUED_1, NEWTON, RFINSEQ, ABIAN, POWER, AFINSQ_1, AFINSQ_2, ORDINAL6, ALGSTR_4, INT_2;
constructors HIDDEN, XTUPLE_0, FUNCT_1, RELSET_1, PARTFUN1, WELLORD2, FUNCT_2, BINOP_1, FUNCOP_1, CARD_1, SETWISEO, XXREAL_0, REAL_1, SQUARE_1, NAT_1, VALUED_0, ABSVALUE, NAT_D, BINOP_2, ORDINAL4, RECDEF_1, VALUED_1, SEQ_1, FINSOP_1, NEWTON, PREPOWER, ABIAN, SERIES_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STIRL2_1, FIB_NUM2, ORDINAL6, BINOM, CARD_FIN, NUMERAL1, ALGSTR_4;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities ORDINAL1, AFINSQ_2, XCMPLX_0;
expansions ;
Lm1:
for n being Element of NAT st 1 < n & n < 5 & n is prime & not n = 2 holds
n = 3
Lm2:
( not 6 is prime & not 8 is prime & not 9 is prime & not 10 is prime & not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime & not 18 is prime & not 20 is prime & not 21 is prime & not 22 is prime & not 24 is prime & not 25 is prime & not 26 is prime & not 27 is prime & not 28 is prime )
Lm3:
for n being Element of NAT st 1 < n & n < 29 & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds
n = 23
Lm4:
for k being Element of NAT st k < 841 holds
for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds
n = 23