let a be non zero Nat; :: thesis: for m, n being Nat holds max ((a |^ n),(a |^ m)) = a |^ (max (n,m))
let m, n be Nat; :: thesis: max ((a |^ n),(a |^ m)) = a |^ (max (n,m))

per cases ( m <= n or m >= n ) ;

suppose A1: m <= n ; :: thesis: max ((a |^ n),(a |^ m)) = a |^ (max (n,m))

then A2: max (m,n) = n by XXREAL_0:def 10;
a |^ m divides a |^ n by A1, NEWTON:89;
then a |^ m <= a |^ n by NAT_D:7;
hence max ((a |^ n),(a |^ m)) = a |^ (max (n,m)) by A2, XXREAL_0:def 10; :: thesis: verum

end;

suppose A1: m >= n ; :: thesis: max ((a |^ n),(a |^ m)) = a |^ (max (n,m))

then A2: max (m,n) = m by XXREAL_0:def 10;
a |^ n divides a |^ m by A1, NEWTON:89;
then a |^ m >= a |^ n by NAT_D:7;
hence max ((a |^ n),(a |^ m)) = a |^ (max (n,m)) by A2, XXREAL_0:def 10; :: thesis: verum

end;

end;