let a be Real; :: thesis: for p being Rational st a >= 1 & p <= 0 holds

a #Q p <= 1

let p be Rational; :: thesis: ( a >= 1 & p <= 0 implies a #Q p <= 1 )

assume that

A1: a >= 1 and

A2: p <= 0 ; :: thesis: a #Q p <= 1

a #Q (- p) >= 1 by A1, A2, Th60;

then 1 / (a #Q p) >= 1 by A1, Th54;

hence a #Q p <= 1 by XREAL_1:191; :: thesis: verum

a #Q p <= 1

let p be Rational; :: thesis: ( a >= 1 & p <= 0 implies a #Q p <= 1 )

assume that

A1: a >= 1 and

A2: p <= 0 ; :: thesis: a #Q p <= 1

a #Q (- p) >= 1 by A1, A2, Th60;

then 1 / (a #Q p) >= 1 by A1, Th54;

hence a #Q p <= 1 by XREAL_1:191; :: thesis: verum