let a be Element of NAT ; :: thesis: for q being Real st 1 < q & q |^ a = 1 holds

a = 0

let q be Real; :: thesis: ( 1 < q & q |^ a = 1 implies a = 0 )

assume that

A1: 1 < q and

A2: q |^ a = 1 and

A3: a <> 0 ; :: thesis: contradiction

a < 1 + 1 by A1, A2, PREPOWER:13;

then a <= 0 + 1 by NAT_1:13;

then a = 1 by A3, NAT_1:8;

then q #Z a = q by PREPOWER:35;

hence contradiction by A1, A2, PREPOWER:36; :: thesis: verum

a = 0

let q be Real; :: thesis: ( 1 < q & q |^ a = 1 implies a = 0 )

assume that

A1: 1 < q and

A2: q |^ a = 1 and

A3: a <> 0 ; :: thesis: contradiction

a < 1 + 1 by A1, A2, PREPOWER:13;

then a <= 0 + 1 by NAT_1:13;

then a = 1 by A3, NAT_1:8;

then q #Z a = q by PREPOWER:35;

hence contradiction by A1, A2, PREPOWER:36; :: thesis: verum