let a, c, d be real number ; :: thesis: ( a > 0 & a <> 1 & c <> d implies a to_power c <> a to_power d )
assume A1: ( a > 0 & a <> 1 & c <> d ) ; :: thesis: a to_power c <> a to_power d

now

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

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

now

per cases ( a < 1 or a > 1 ) by A1, 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, A2, Th45; :: 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 A2, Th44; :: thesis: verum

end;

end;

end;

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

end;

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

now

per cases ( a < 1 or a > 1 ) by A1, 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, A3, Th45; :: 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 A3, Th44; :: 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