let a be Real; for p being Rational st a > 0 holds
1 / (a #Q p) = a #Q (- p)
let p be Rational; ( a > 0 implies 1 / (a #Q p) = a #Q (- p) )
assume
a > 0
; 1 / (a #Q p) = a #Q (- p)
then A1:
a #Z (numerator p) > 0
by Th39;
thus a #Q (- p) =
(denominator (- p)) -Root (a #Z (- (numerator p)))
by RAT_1:43
.=
(denominator p) -Root (a #Z (- (numerator p)))
by RAT_1:43
.=
(denominator p) -Root (1 / (a #Z (numerator p)))
by Th41
.=
1 / (a #Q p)
by A1, Th23, RAT_1:11
; verum