let
a
,
x
be
Real
;
:: thesis:
(
a
>
0
&
a
<>
1 &
a
to_power
x
=
1 implies
x
=
0
)
assume
that
A1
: (
a
>
0
&
a
<>
1 )
and
A2
:
a
to_power
x
=
1 ;
:: thesis:
x
=
0
x
=
log
(
a
,1)
by
A1
,
A2
,
POWER:def 3
;
hence
x
=
0
by
A1
,
POWER:51
;
:: thesis:
verum