let a, c, d be Real; :: thesis: ( a > 0 & a <> 1 & c <> d implies a to_power c <> a to_power d )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: c <> d ; :: thesis: a to_power c <> a to_power d

now :: thesis: a to_power c <> a to_power d

per cases ( c < d or c > d ) by A3, XXREAL_0:1;

suppose A4: c < d ; :: thesis: a to_power c <> a to_power d

now :: thesis: a to_power c <> a to_power d

per cases ( a < 1 or a > 1 ) by A2, XXREAL_0:1;

suppose a < 1 ; :: thesis: a to_power c <> a to_power d

hence a to_power c <> a to_power d by A1, A4, Th40; :: thesis: verum

end;

suppose a > 1 ; :: thesis: a to_power c <> a to_power d

hence a to_power c <> a to_power d by A4, Th39; :: thesis: verum

end;

end;

end;

hence a to_power c <> a to_power d ; :: thesis: verum

end;

suppose A5: c > d ; :: thesis: a to_power c <> a to_power d

now :: thesis: a to_power c <> a to_power d

per cases ( a < 1 or a > 1 ) by A2, XXREAL_0:1;

suppose a < 1 ; :: thesis: a to_power c <> a to_power d

hence a to_power c <> a to_power d by A1, A5, Th40; :: thesis: verum

end;

suppose a > 1 ; :: thesis: a to_power c <> a to_power d

hence a to_power c <> a to_power d by A5, Th39; :: thesis: verum

end;

end;

end;

hence a to_power c <> a to_power d ; :: thesis: verum

end;

end;

end;

hence a to_power c <> a to_power d ; :: thesis: verum