let m, n be positive Real; :: thesis: ( (1 / m) + (1 / n) = 1 implies m > 1 )
assume (1 / m) + (1 / n) = 1 ; :: thesis: m > 1
then A1: 1 / n = 1 - (1 / m) ;
assume m <= 1 ; :: thesis: contradiction
then 1 <= 1 / m by XREAL_1:181;
hence contradiction by A1, XREAL_1:47; :: thesis: verum