let a be Real; :: thesis: for n being Nat st 0 <= a holds

a #Q n = a |^ n

let n be Nat; :: thesis: ( 0 <= a implies a #Q n = a |^ n )

A1: denominator n = 1 by RAT_1:17;

A2: numerator n = n by RAT_1:17;

assume 0 <= a ; :: thesis: a #Q n = a |^ n

hence a #Q n = a #Z n by A1, A2, Lm5, Th21

.= a |^ n by Th36 ;

:: thesis: verum

a #Q n = a |^ n

let n be Nat; :: thesis: ( 0 <= a implies a #Q n = a |^ n )

A1: denominator n = 1 by RAT_1:17;

A2: numerator n = n by RAT_1:17;

assume 0 <= a ; :: thesis: a #Q n = a |^ n

hence a #Q n = a #Z n by A1, A2, Lm5, Th21

.= a |^ n by Th36 ;

:: thesis: verum