let a be Real; :: thesis: for l being Integer st a > 0 holds

a #Q l = a #Z l

let l be Integer; :: thesis: ( a > 0 implies a #Q l = a #Z l )

assume a > 0 ; :: thesis: a #Q l = a #Z l

then a #Z l > 0 by Th39;

then A1: a #Z l = (1 -Root (a #Z l)) |^ 1 by Def2;

denominator l = 1 by RAT_1:17;

hence a #Q l = 1 -Root (a #Z l) by RAT_1:17

.= a #Z l by A1 ;

:: thesis: verum

a #Q l = a #Z l

let l be Integer; :: thesis: ( a > 0 implies a #Q l = a #Z l )

assume a > 0 ; :: thesis: a #Q l = a #Z l

then a #Z l > 0 by Th39;

then A1: a #Z l = (1 -Root (a #Z l)) |^ 1 by Def2;

denominator l = 1 by RAT_1:17;

hence a #Q l = 1 -Root (a #Z l) by RAT_1:17

.= a #Z l by A1 ;

:: thesis: verum