let m, n be positive real number ; :: thesis: ( (1 / m) + (1 / n) = 1 implies m > 1 )
assume (1 / m) + (1 / n) = 1 ; :: thesis: m > 1
then A2: 1 / n = 1 - (1 / m) ;
assume m <= 1 ; :: thesis: contradiction
then 1 <= 1 / m by XREAL_1:183;
hence contradiction by A2, XREAL_1:49; :: thesis: verum