let a be positive heavy Real; :: thesis: for b being positive Real holds
( a > b iff log (a,b) < 1 )
let b be positive Real; :: thesis: ( a > b iff log (a,b) < 1 )
A1: a > 1 by TA1;
A2: ( log (a,b) < 1 implies a > b )
proof
assume log (a,b) < 1 ; :: thesis: a > b
then a to_power (log (a,b)) < a to_power 1 by A1, POWER:39;
hence a > b ; :: thesis: verum
end;
( a > b implies log (a,b) < 1 )
proof
assume a > b ; :: thesis: log (a,b) < 1
then a to_power 1 > a to_power (log (a,b)) ;
then ( 1 >= log (a,b) & 1 <> log (a,b) ) by A1, POWER:39;
hence log (a,b) < 1 by XXREAL_0:1; :: thesis: verum
end;
hence ( a > b iff log (a,b) < 1 ) by A2; :: thesis: verum