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