let
a
,
b
,
x
be
Real
;
:: thesis:
(
a
>
0
&
a
<>
1 &
x
>
0
&
log
(
a
,
x
)
=
0
implies
x
=
1 )
assume
(
a
>
0
&
a
<>
1 &
x
>
0
&
log
(
a
,
x
)
=
0
) ;
:: thesis:
x
=
1
then
a
to_power
0
=
x
by
POWER:def 3
;
hence
x
=
1
by
POWER:24
;
:: thesis:
verum