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

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

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

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

end;

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

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

end;

end;