environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_1, RAT_1, RELAT_1, ARYTM_1, NEWTON, ARYTM_3, CARD_1, PREPOWER, FUNCT_1, XXREAL_0, NAT_1, REAL_1, SEQ_1, SEQ_2, ORDINAL2, SQUARE_1, XXREAL_2, SEQ_4, COMPLEX1, VALUED_0, POWER, ABIAN, ORDINAL1;
notations HIDDEN, SUBSET_1, NEWTON, ORDINAL1, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, INT_1, RAT_1, REAL_1, NUMBERS, NAT_1, SEQ_1, SEQ_2, COMSEQ_2, SEQM_3, SQUARE_1, SEQ_4, PREPOWER, ABIAN, XXREAL_2;
definitions INT_1, ABIAN, XXREAL_2;
theorems ABSVALUE, NAT_1, SEQ_2, SEQM_3, INT_1, SEQ_4, NEWTON, PREPOWER, TARSKI, FUNCT_2, XREAL_0, XCMPLX_1, XREAL_1, XXREAL_0, ABIAN, ORDINAL1;
schemes SEQ_1;
registrations XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, PREPOWER, SEQ_4, ABIAN, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, SEQ_2, SEQM_3, SEQ_4, NEWTON, PREPOWER, XXREAL_2, RELSET_1, ABIAN, BINOP_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, XCMPLX_0;
expansions ;
theorem
for
a,
b,
c being
Real st
a > 1 &
b > 0 &
c > b holds
log (
a,
c)
> log (
a,
b)