let t be Real; :: thesis: ( 0 < t & t <> 1 implies (2 * t) / ((t ^2) - 1) <> 0 )
assume that
A1: 0 < t and
A2: t <> 1 ; :: thesis: (2 * t) / ((t ^2) - 1) <> 0
per cases ( 1 < t or t < 1 ) by A2, XXREAL_0:1;
suppose A3: 1 < t ; :: thesis: (2 * t) / ((t ^2) - 1) <> 0
then t < t ^2 by SQUARE_1:14;
then 1 < t ^2 by A3, XXREAL_0:2;
then A4: 1 - 1 < (t ^2) - 1 by XREAL_1:14;
2 * 1 < 2 * t by A3, XREAL_1:68;
then 0 / ((t ^2) - 1) < (2 * t) / ((t ^2) - 1) by A4;
hence (2 * t) / ((t ^2) - 1) <> 0 ; :: thesis: verum
end;
suppose A5: t < 1 ; :: thesis: (2 * t) / ((t ^2) - 1) <> 0
then t ^2 < t by A1, SQUARE_1:13;
then t ^2 < 1 by A5, XXREAL_0:2;
then A6: (t ^2) - 1 < 1 - 1 by XREAL_1:14;
0 * 2 < 2 * t by A1;
then (2 * t) / ((t ^2) - 1) < 0 / ((t ^2) - 1) by A6;
hence (2 * t) / ((t ^2) - 1) <> 0 ; :: thesis: verum
end;
end;