environ
vocabularies HIDDEN, FUNCT_1, INT_1, ARYTM_1, ARYTM_3, CARD_1, FUNCT_2, NAT_1, CARD_3, FINSET_1, ORDINAL2, RPR_1, CARDFIN2, ABIAN, POWER, COMPLEX1, AFINSQ_1, RELAT_1, XCMPLX_0, SIN_COS, SERIES_1, TAYLOR_1, SUBSET_1, FDIFF_1, FINSEQ_1, TARSKI, REAL_1, FINSOP_1, NEWTON, ORDINAL1, REALSET1, XXREAL_0, XBOOLE_0, XXREAL_1, VALUED_1, NUMBERS, BINOP_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_1, NAT_1, COMPLEX1, BINOP_2, VALUED_1, NEWTON, RCOMP_1, FCONT_1, POWER, SERIES_1, SEQFUNC, SIN_COS, AFINSQ_1, ABIAN, TAYLOR_1, RPR_1, AFINSQ_2;
definitions XBOOLE_0, TARSKI;
theorems CARD_2, CARD_FIN, FUNCT_2, XBOOLE_0, NEWTON, XREAL_0, XCMPLX_1, RPR_1, XREAL_1, XCMPLX_0, INT_1, ORDINAL1, CARD_1, TAYLOR_1, SIN_COS, TAYLOR_2, XXREAL_1, ABIAN, STIRL2_1, SERIES_1, SEQ_1, SIN_COS2, NAT_1, TARSKI, BINOP_2, IRRAT_1, SEQ_2, FIB_NUM2, SIN_COS7, XXREAL_0, RELAT_1, VALUED_1, FUNCT_1, AFINSQ_2, XBOOLE_1, POWER;
schemes RECDEF_2, FIB_NUM, NAT_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, CARD_1, FINSET_1, NUMBERS, SIN_COS, RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, FCONT_3, FCONT_1, AFINSQ_1, POWER, FUNCT_1, BINOP_2, XCMPLX_0, XBOOLE_0, RELAT_1, FRAENKEL, AFINSQ_2, ORDINAL1, NEWTON;
constructors HIDDEN, REAL_1, SERIES_1, ABIAN, RCOMP_1, SIN_COS, TAYLOR_1, FCONT_1, SEQFUNC, RELSET_1, SETWISEO, YELLOW20, WELLORD2, NAT_D, BINARITH, RPR_1, AFINSQ_2, NEWTON, BINOP_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0, SUBSET_1, SIN_COS, CARD_1, ORDINAL1;
expansions ;
reconsider j = 1, z = 0 as Element of INT by INT_1:def 2;
deffunc H1( Nat, Integer, Integer) -> Element of INT = In ((($1 + 1) * ($2 + $3)),INT);
Lm1:
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
:: we cannot divide and it has to be proved separately.