For the most part, real logarithm functions are proved and complex logarithm functions are noted in the missing theorems list.
One big part is a proof of https://us.metamath.org/mpeuni/eflt.html via continuity (I don't know if there is an easier proof but this one works). Some consequences of eflt are included as well.
logfac seems provable but a bit involved, so it isn't included here.
For the most part, real logarithm functions are proved and complex logarithm functions are noted in the missing theorems list.
One big part is a proof of https://us.metamath.org/mpeuni/eflt.html via continuity (I don't know if there is an easier proof but this one works). Some consequences of
efltare included as well.logfacseems provable but a bit involved, so it isn't included here.