let a, b be Real; :: thesis: for n being Nat st a >= 0 & b > 0 & n >= 1 holds
n -Root (a / b) = (n -Root a) / (n -Root b)
let n be Nat; :: thesis: ( a >= 0 & b > 0 & n >= 1 implies n -Root (a / b) = (n -Root a) / (n -Root b) )
assume that
A1: a >= 0 and
A2: b > 0 and
A3: n >= 1 ; :: thesis: n -Root (a / b) = (n -Root a) / (n -Root b)
thus n -Root (a / b) = n -Root (a * (b "))
.= (n -Root a) * (n -Root (b ")) by A1, A2, A3, Th22
.= (n -Root a) * (n -Root (1 / b))
.= (n -Root a) * (1 / (n -Root b)) by A2, A3, Th23
.= ((n -Root a) * 1) / (n -Root b)
.= (n -Root a) / (n -Root b) ; :: thesis: verum