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

now

let i be set ; :: thesis: ( i in SetPrimes implies (pfexp (n lcm m)) . i = (max (pfexp n),(pfexp m)) . i )
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 lhs = pfexp (n lcm m);
set rhs = max (pfexp n),(pfexp m);
set x = j |-count n;
set y = j |-count m;
set z = j |-count (n lcm m);
A1: j > 1 by INT_2:def 5;
A2: n lcm m <> 0 by INT_2:4;
A3: (pfexp (n lcm m)) . j = j |-count (n lcm m) by Def8;
A4: j |^ (j |-count (n lcm m)) divides n lcm m by A1, A2, Def7;
A5: not j |^ ((j |-count (n lcm m)) + 1) divides n lcm m by A1, A2, Def7;
A6: (pfexp n) . j = j |-count n by Def8;
A7: j |^ (j |-count n) divides n by A1, Def7;
A8: not j |^ ((j |-count n) + 1) divides n by A1, Def7;
A9: (pfexp m) . j = j |-count m by Def8;
A10: j |^ (j |-count m) divides m by A1, Def7;
A11: not j |^ ((j |-count m) + 1) divides m by A1, Def7;
A12: m divides n lcm m by NAT_D:def 4;
A13: n divides n lcm m by NAT_D:def 4;
A14: j |^ (j |-count m) divides n lcm m by A10, A12, NAT_D:4;
A15: j |^ (j |-count n) divides n lcm m by A7, A13, 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

then A17: (max (pfexp n),(pfexp m)) . j = j |-count m by A9, Def4;
A18: j |-count m <= j |-count (n lcm m) by A5, A14, Th4;

now

assume j |-count m < j |-count (n lcm m) ; :: thesis: contradiction
then j |^ ((j |-count m) + 1) divides n lcm m by A4, Th4;
then consider k being Nat such that
A19: n lcm m = (j |^ ((j |-count m) + 1)) * k by NAT_D:def 3;
A20: n lcm m = ((j |^ (j |-count m)) * j) * k by A19, NEWTON:11
.= (j |^ (j |-count m)) * (k * j) ;
0 <> k by A19, INT_2:4;
then A21: 0 < k ;
then A22: 0 * k < (j |^ (j |-count m)) * k ;
consider t being Nat such that
A23: n = (j |^ (j |-count n)) * t by A7, NAT_D:def 3;
consider u being Nat such that
A24: n lcm m = n * u by A13, NAT_D:def 3;
consider p being Nat such that
A25: j |-count m = (j |-count n) + p by A6, A9, A16, NAT_1:10;
(j |^ (j |-count n)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count n)) * (j |^ p)) * (k * j)
.= (j |^ (j |-count n)) * (t * u) by A20, A23, A24, A25, NEWTON:13 ;
then ((j |^ p) * k) * j = t * u by XCMPLX_1:5;
then A26: j divides t * u by NAT_D:def 3;

now

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A27: t = j * w by NAT_D:def 3;
n = ((j |^ (j |-count n)) * j) * w by A23, A27
.= (j |^ ((j |-count n) + 1)) * w by NEWTON:11 ;
hence contradiction by A8, NAT_D:def 3; :: thesis: verum

end;

then j divides u by A26, NEWTON:98;
then consider w being Nat such that
A28: u = j * w by NAT_D:def 3;
((j |^ (j |-count m)) * k) * j = (n * w) * j by A20, A24, A28;
then (j |^ (j |-count m)) * k = n * w by XCMPLX_1:5;
then A29: n divides (j |^ (j |-count m)) * k by NAT_D:def 3;
consider t being Nat such that
A30: m = (j |^ (j |-count m)) * t by A10, NAT_D:def 3;
consider u being Nat such that
A31: n lcm m = m * u by A12, NAT_D:def 3;
(j |^ (j |-count m)) * (k * j) = (j |^ (j |-count m)) * (t * u) by A20, A30, A31;
then k * j = t * u by XCMPLX_1:5;
then A32: j divides t * u by NAT_D:def 3;

now

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A33: t = j * w by NAT_D:def 3;
m = ((j |^ (j |-count m)) * j) * w by A30, A33
.= (j |^ ((j |-count m) + 1)) * w by NEWTON:11 ;
hence contradiction by A11, NAT_D:def 3; :: thesis: verum

end;

then j divides u by A32, NEWTON:98;
then consider w being Nat such that
A34: u = j * w by NAT_D:def 3;
((j |^ (j |-count m)) * k) * j = (m * w) * j by A20, A31, A34;
then (j |^ (j |-count m)) * k = m * w by XCMPLX_1:5;
then m divides (j |^ (j |-count m)) * k by NAT_D:def 3;
then n lcm m divides (j |^ (j |-count m)) * k by A29, NAT_D:def 4;
then (j |^ ((j |-count m) + 1)) * k <= (j |^ (j |-count m)) * k by A19, A22, NAT_D:7;
then j |^ ((j |-count m) + 1) <= j |^ (j |-count m) by A21, XREAL_1:70;
then (j |^ (j |-count m)) * j <= (j |^ (j |-count m)) * 1 by NEWTON:11;
then j <= 1 by XREAL_1:70;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

hence (pfexp (n lcm m)) . i = (max (pfexp n),(pfexp m)) . i by A3, A17, A18, XXREAL_0:1; :: thesis: verum

end;

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

then A36: (max (pfexp n),(pfexp m)) . j = j |-count n by A6, Def4;
A37: j |-count n <= j |-count (n lcm m) by A5, A15, Th4;

now

assume j |-count n < j |-count (n lcm m) ; :: thesis: contradiction
then j |^ ((j |-count n) + 1) divides n lcm m by A4, Th4;
then consider k being Nat such that
A38: n lcm m = (j |^ ((j |-count n) + 1)) * k by NAT_D:def 3;
A39: n lcm m = ((j |^ (j |-count n)) * j) * k by A38, NEWTON:11
.= (j |^ (j |-count n)) * (k * j) ;
0 <> k by A38, INT_2:4;
then A40: 0 < k ;
then A41: 0 * k < (j |^ (j |-count n)) * k ;
consider t being Nat such that
A42: m = (j |^ (j |-count m)) * t by A10, NAT_D:def 3;
consider u being Nat such that
A43: n lcm m = m * u by A12, NAT_D:def 3;
consider p being Nat such that
A44: j |-count n = (j |-count m) + p by A6, A9, A35, NAT_1:10;
(j |^ (j |-count m)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count m)) * (j |^ p)) * (k * j)
.= (j |^ (j |-count m)) * (t * u) by A39, A42, A43, A44, NEWTON:13 ;
then t * u = ((j |^ p) * k) * j by XCMPLX_1:5;
then A45: j divides t * u by NAT_D:def 3;

now

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A46: t = j * w by NAT_D:def 3;
m = ((j |^ (j |-count m)) * j) * w by A42, A46
.= (j |^ ((j |-count m) + 1)) * w by NEWTON:11 ;
hence contradiction by A11, NAT_D:def 3; :: thesis: verum

end;

then j divides u by A45, NEWTON:98;
then consider w being Nat such that
A47: u = j * w by NAT_D:def 3;
((j |^ (j |-count n)) * k) * j = (m * w) * j by A39, A43, A47;
then (j |^ (j |-count n)) * k = m * w by XCMPLX_1:5;
then A48: m divides (j |^ (j |-count n)) * k by NAT_D:def 3;
consider t being Nat such that
A49: n = (j |^ (j |-count n)) * t by A7, NAT_D:def 3;
consider u being Nat such that
A50: n lcm m = n * u by A13, NAT_D:def 3;
(j |^ (j |-count n)) * (k * j) = (j |^ (j |-count n)) * (t * u) by A39, A49, A50;
then k * j = t * u by XCMPLX_1:5;
then A51: j divides t * u by NAT_D:def 3;

now

assume j divides t ; :: thesis: contradiction
then consider w being Nat such that
A52: t = j * w by NAT_D:def 3;
n = ((j |^ (j |-count n)) * j) * w by A49, A52
.= (j |^ ((j |-count n) + 1)) * w by NEWTON:11 ;
hence contradiction by A8, NAT_D:def 3; :: thesis: verum

end;

then j divides u by A51, NEWTON:98;
then consider w being Nat such that
A53: u = j * w by NAT_D:def 3;
((j |^ (j |-count n)) * k) * j = (n * w) * j by A39, A50, A53;
then (j |^ (j |-count n)) * k = n * w by XCMPLX_1:5;
then n divides (j |^ (j |-count n)) * k by NAT_D:def 3;
then n lcm m divides (j |^ (j |-count n)) * k by A48, NAT_D:def 4;
then (j |^ ((j |-count n) + 1)) * k <= (j |^ (j |-count n)) * k by A38, A41, NAT_D:7;
then j |^ ((j |-count n) + 1) <= j |^ (j |-count n) by A40, XREAL_1:70;
then (j |^ (j |-count n)) * j <= (j |^ (j |-count n)) * 1 by NEWTON:11;
then j <= 1 by XREAL_1:70;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

hence (pfexp (n lcm m)) . i = (max (pfexp n),(pfexp m)) . i by A3, A36, A37, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

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