Description: Closed form of aleximi . Note: this proof is shorter, so aleximi could be deduced from it ( exim would have to be proved first, see
bj-eximALT but its proof is shorter (currently almost a subproof of
aleximi )). (Contributed by BJ, 8-Nov-2021)