let x, a, b be Real; :: thesis: for n being Element of NAT st a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 holds

x = n -root (- (b / a))

let n be Element of NAT ; :: thesis: ( a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 implies x = n -root (- (b / a)) )

assume that

A1: a <> 0 and

A2: n is odd and

A3: Polynom (a,b,0,(x |^ n)) = 0 ; :: thesis: ( x = 0 or x = n -root (- (b / a)) )

x = n -root (- (b / a))

let n be Element of NAT ; :: thesis: ( a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 implies x = n -root (- (b / a)) )

assume that

A1: a <> 0 and

A2: n is odd and

A3: Polynom (a,b,0,(x |^ n)) = 0 ; :: thesis: ( x = 0 or x = n -root (- (b / a)) )

now :: thesis: ( x = 0 or x = n -root (- (b / a)) )

hence
( x = 0 or x = n -root (- (b / a)) )
; :: thesis: verumend;