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

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