let m, n be non zero Nat; pfexp (n lcm m) = max ((pfexp n),(pfexp m))
now for i being object st i in SetPrimes holds
(pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . iset rhs =
max (
(pfexp n),
(pfexp m));
set lhs =
pfexp (n lcm m);
let i be
object ;
( 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
;
(pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . ithen 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
verumproof
per cases
( (pfexp n) . j <= (pfexp m) . j or (pfexp n) . j > (pfexp m) . j )
;
suppose A16:
(pfexp n) . j <= (pfexp m) . j
;
(pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . iA17:
now 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;
consider u being
Nat such that A22:
n lcm m = n * u
by A10;
assume
j |-count m < j |-count (n lcm m)
;
contradictionthen
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;
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;
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;
verum end; suppose A34:
(pfexp n) . j > (pfexp m) . j
;
(pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . iA35:
now 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;
consider u being
Nat such that A40:
n lcm m = m * u
by A1;
assume
j |-count n < j |-count (n lcm m)
;
contradictionthen
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;
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;
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;
verum end; end;
end; end;
hence
pfexp (n lcm m) = max ((pfexp n),(pfexp m))
; verum