let
m
,
n
be
Nat
;
:: thesis:
( 1
<=
m
implies 1
<=
m
to_power
n
)
per
cases
(
n
=
0
or
n
<>
0
)
;
suppose
n
=
0
;
:: thesis:
( 1
<=
m
implies 1
<=
m
to_power
n
)
hence
( 1
<=
m
implies 1
<=
m
to_power
n
)
by
POWER:24
;
:: thesis:
verum
end;
suppose
A1
:
n
<>
0
;
:: thesis:
( 1
<=
m
implies 1
<=
m
to_power
n
)
assume
1
<=
m
;
:: thesis:
1
<=
m
to_power
n
then
( 1
<
m
or 1
=
m
)
by
XXREAL_0:1
;
hence
1
<=
m
to_power
n
by
A1
,
POWER:26
,
POWER:35
;
:: thesis:
verum
end;
end;