let m, n be non zero Nat; :: thesis: pfexp (n lcm m) = max ((pfexp n),(pfexp m))

now :: thesis: for i being object st i in SetPrimes holds
(pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i

set rhs = max ((pfexp n),(pfexp m));
set lhs = pfexp (n lcm m);
let i be object ; :: thesis: ( i in SetPrimes implies (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i )
A1: m divides n lcm m by NAT_D:def 4;
assume i in SetPrimes ; :: thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i
then reconsider j = i as prime Element of NAT by NEWTON:def 6;
set x = j |-count n;
set y = j |-count m;
set z = j |-count (n lcm m);
A2: (pfexp (n lcm m)) . j = j |-count (n lcm m) by Def8;
A3: (pfexp n) . j = j |-count n by Def8;
A4: j > 1 by INT_2:def 4;
then A5: not j |^ ((j |-count n) + 1) divides n by Def7;
A6: n lcm m <> 0 by INT_2:4;
then A7: j |^ (j |-count (n lcm m)) divides n lcm m by A4, Def7;
A8: not j |^ ((j |-count (n lcm m)) + 1) divides n lcm m by A4, A6, Def7;
A9: (pfexp m) . j = j |-count m by Def8;
A10: n divides n lcm m by NAT_D:def 4;
A11: j |^ (j |-count n) divides n by A4, Def7;
then A12: j |^ (j |-count n) divides n lcm m by A10, NAT_D:4;
A13: not j |^ ((j |-count m) + 1) divides m by A4, Def7;
A14: j |^ (j |-count m) divides m by A4, Def7;
then A15: j |^ (j |-count m) divides n lcm m by A1, NAT_D:4;
thus (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i :: thesis: verum

proof

per cases ( (pfexp n) . j <= (pfexp m) . j or (pfexp n) . j > (pfexp m) . j ) ;

suppose A16: (pfexp n) . j <= (pfexp m) . j ; :: thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i

A17: now :: thesis: not j |-count m < j |-count (n lcm m)

consider p being Nat such that
A18: j |-count m = (j |-count n) + p by A3, A9, A16, NAT_1:10;
consider t being Nat such that
A19: n = (j |^ (j |-count n)) * t by A11;

A20: now :: thesis: not j divides t

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A21: t = j * w ;
n = ((j |^ (j |-count n)) * j) * w by A19, A21
.= (j |^ ((j |-count n) + 1)) * w by NEWTON:6 ;
hence contradiction by A5; :: thesis: verum

end;

consider u being Nat such that
A22: n lcm m = n * u by A10;
assume j |-count m < j |-count (n lcm m) ; :: thesis: contradiction
then j |^ ((j |-count m) + 1) divides n lcm m by A7, Th4;
then consider k being Nat such that
A23: n lcm m = (j |^ ((j |-count m) + 1)) * k ;
A24: n lcm m = ((j |^ (j |-count m)) * j) * k by A23, NEWTON:6
.= (j |^ (j |-count m)) * (k * j) ;
(j |^ (j |-count n)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count n)) * (j |^ p)) * (k * j)
.= (j |^ (j |-count n)) * (t * u) by A24, A19, A22, A18, NEWTON:8 ;
then ((j |^ p) * k) * j = t * u by XCMPLX_1:5;
then j divides t * u ;
then j divides u by A20, NEWTON:80;
then consider w being Nat such that
A25: u = j * w ;
((j |^ (j |-count m)) * k) * j = (n * w) * j by A24, A22, A25;
then (j |^ (j |-count m)) * k = n * w by XCMPLX_1:5;
then A26: n divides (j |^ (j |-count m)) * k ;
consider t being Nat such that
A27: m = (j |^ (j |-count m)) * t by A14;

A28: now :: thesis: not j divides t

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A29: t = j * w ;
m = ((j |^ (j |-count m)) * j) * w by A27, A29
.= (j |^ ((j |-count m) + 1)) * w by NEWTON:6 ;
hence contradiction by A13; :: thesis: verum

end;

consider u being Nat such that
A30: n lcm m = m * u by A1;
(j |^ (j |-count m)) * (k * j) = (j |^ (j |-count m)) * (t * u) by A24, A27, A30;
then k * j = t * u by XCMPLX_1:5;
then j divides t * u ;
then j divides u by A28, NEWTON:80;
then consider w being Nat such that
A31: u = j * w ;
((j |^ (j |-count m)) * k) * j = (m * w) * j by A24, A30, A31;
then (j |^ (j |-count m)) * k = m * w by XCMPLX_1:5;
then m divides (j |^ (j |-count m)) * k ;
then A32: n lcm m divides (j |^ (j |-count m)) * k by A26, NAT_D:def 4;
0 <> k by A23, INT_2:4;
then j |^ ((j |-count m) + 1) <= j |^ (j |-count m) by A23, A32, NAT_D:7, XREAL_1:68;
then (j |^ (j |-count m)) * j <= (j |^ (j |-count m)) * 1 by NEWTON:6;
then j <= 1 by XREAL_1:68;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

A33: j |-count m <= j |-count (n lcm m) by A8, A15, Th4;
(max ((pfexp n),(pfexp m))) . j = j |-count m by A9, A16, Def4;
hence (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i by A2, A33, A17, XXREAL_0:1; :: thesis: verum

end;

suppose A34: (pfexp n) . j > (pfexp m) . j ; :: thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i

A35: now :: thesis: not j |-count n < j |-count (n lcm m)

consider p being Nat such that
A36: j |-count n = (j |-count m) + p by A3, A9, A34, NAT_1:10;
consider t being Nat such that
A37: m = (j |^ (j |-count m)) * t by A14;

A38: now :: thesis: not j divides t

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A39: t = j * w ;
m = ((j |^ (j |-count m)) * j) * w by A37, A39
.= (j |^ ((j |-count m) + 1)) * w by NEWTON:6 ;
hence contradiction by A13; :: thesis: verum

end;

consider u being Nat such that
A40: n lcm m = m * u by A1;
assume j |-count n < j |-count (n lcm m) ; :: thesis: contradiction
then j |^ ((j |-count n) + 1) divides n lcm m by A7, Th4;
then consider k being Nat such that
A41: n lcm m = (j |^ ((j |-count n) + 1)) * k ;
A42: n lcm m = ((j |^ (j |-count n)) * j) * k by A41, NEWTON:6
.= (j |^ (j |-count n)) * (k * j) ;
(j |^ (j |-count m)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count m)) * (j |^ p)) * (k * j)
.= (j |^ (j |-count m)) * (t * u) by A42, A37, A40, A36, NEWTON:8 ;
then t * u = ((j |^ p) * k) * j by XCMPLX_1:5;
then j divides t * u ;
then j divides u by A38, NEWTON:80;
then consider w being Nat such that
A43: u = j * w ;
((j |^ (j |-count n)) * k) * j = (m * w) * j by A42, A40, A43;
then (j |^ (j |-count n)) * k = m * w by XCMPLX_1:5;
then A44: m divides (j |^ (j |-count n)) * k ;
consider t being Nat such that
A45: n = (j |^ (j |-count n)) * t by A11;

A46: now :: thesis: not j divides t

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A47: t = j * w ;
n = ((j |^ (j |-count n)) * j) * w by A45, A47
.= (j |^ ((j |-count n) + 1)) * w by NEWTON:6 ;
hence contradiction by A5; :: thesis: verum

end;

consider u being Nat such that
A48: n lcm m = n * u by A10;
(j |^ (j |-count n)) * (k * j) = (j |^ (j |-count n)) * (t * u) by A42, A45, A48;
then k * j = t * u by XCMPLX_1:5;
then j divides t * u ;
then j divides u by A46, NEWTON:80;
then consider w being Nat such that
A49: u = j * w ;
((j |^ (j |-count n)) * k) * j = (n * w) * j by A42, A48, A49;
then (j |^ (j |-count n)) * k = n * w by XCMPLX_1:5;
then n divides (j |^ (j |-count n)) * k ;
then A50: n lcm m divides (j |^ (j |-count n)) * k by A44, NAT_D:def 4;
0 <> k by A41, INT_2:4;
then j |^ ((j |-count n) + 1) <= j |^ (j |-count n) by A41, A50, NAT_D:7, XREAL_1:68;
then (j |^ (j |-count n)) * j <= (j |^ (j |-count n)) * 1 by NEWTON:6;
then j <= 1 by XREAL_1:68;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

A51: j |-count n <= j |-count (n lcm m) by A8, A12, Th4;
(max ((pfexp n),(pfexp m))) . j = j |-count n by A3, A34, Def4;
hence (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i by A2, A51, A35, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

hence pfexp (n lcm m) = max ((pfexp n),(pfexp m)) ; :: thesis: verum