let r be Real; :: thesis: for i, j being Nat st r <> 0 & j <= i holds
r |^ (i -' j) = (r |^ i) / (r |^ j)
let i, j be Nat; :: thesis: ( r <> 0 & j <= i implies r |^ (i -' j) = (r |^ i) / (r |^ j) )
assume that
A1: r <> 0 and
A2: j <= i ; :: thesis: r |^ (i -' j) = (r |^ i) / (r |^ j)
reconsider rr = r as Real ;
thus (r |^ i) / (r |^ j) = (Product (i |-> rr)) / (rr |^ j) by NEWTON:def 1
.= (Product (i |-> rr)) / (Product (j |-> rr)) by NEWTON:def 1
.= Product ((i -' j) |-> rr) by A1, A2, Th8
.= r |^ (i -' j) by NEWTON:def 1 ; :: thesis: verum