let a, b be Element of [.0,1.]; :: thesis: ( ( a > 0 or b > 0 ) implies b to_power a in [.0,1.] )
YY: ( b <= 1 & b >= 0 ) by XXREAL_1:1;
XX: a >= 0 by XXREAL_1:1;
assume ( a > 0 or b > 0 ) ; :: thesis: b to_power a in [.0,1.]
per cases then ( ( a > 0 & b <> 0 & b <> 1 ) or ( a > 0 & b <> 0 & b = 1 ) or ( a > 0 & b = 0 ) or ( b > 0 & b <> 1 ) or ( b > 0 & b = 1 ) ) ;
suppose S1: ( a > 0 & b <> 0 & b <> 1 ) ; :: thesis: b to_power a in [.0,1.]
then B1: ( a > 0 & b > 0 ) by XXREAL_1:1;
ZZ: b < 1 by S1, XXREAL_0:1, YY;
b to_power a < b to_power 0 by POWER:40, B1, ZZ;
then A1: b to_power a <= 1 by POWER:24;
b to_power a > 0 by B1, POWER:34;
hence b to_power a in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum
end;
suppose S1: ( a > 0 & b <> 0 & b = 1 ) ; :: thesis: b to_power a in [.0,1.]
then A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by S1, POWER:34;
hence b to_power a in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum
end;
suppose B1: ( a > 0 & b = 0 ) ; :: thesis: b to_power a in [.0,1.]
then A1: b to_power a <= 1 by POWER:def 2;
b to_power a >= 0 by POWER:def 2, B1;
hence b to_power a in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum
end;
suppose B1: ( b > 0 & b <> 1 ) ; :: thesis: b to_power a in [.0,1.]
b <= 1 by XXREAL_1:1;
then b to_power a <= 1 to_power a by XX, B1, HOLDER_1:3;
then A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by B1, POWER:34;
hence b to_power a in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum
end;
suppose B1: ( b > 0 & b = 1 ) ; :: thesis: b to_power a in [.0,1.]
then A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by B1, POWER:34;
hence b to_power a in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum
end;
end;