let a be Real; :: thesis: for p being Rational
for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a
let p be Rational; :: thesis: for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a
let n be Nat; :: thesis: ( n >= 1 & p = n " implies a #Q p = n -Root a )
assume that
A1: n >= 1 and
A2: p = n " ; :: thesis: a #Q p = n -Root a
reconsider q = n as Rational ;
A3: p = 1 / n by A2;
then denominator p = numerator q by A1, RAT_1:44;
then A4: denominator p = n by RAT_1:17;
numerator p = denominator q by A1, A3, RAT_1:44;
then numerator p = 1 by RAT_1:17;
hence a #Q p = n -Root a by A4, Th35; :: thesis: verum