let m, n be non zero Nat; :: thesis: pfexp (n gcd m) = min ((pfexp n),(pfexp m))
now :: thesis: for i being object st i in SetPrimes holds
(pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i
set rhs = min ((pfexp n),(pfexp m));
set lhs = pfexp (n gcd m);
let i be object ; :: thesis: ( i in SetPrimes implies (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i )
assume i in SetPrimes ; :: thesis: (pfexp (n gcd m)) . i = (min ((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 gcd m);
A1: (pfexp (n gcd m)) . j = j |-count (n gcd m) by Def8;
A2: j <> 1 by INT_2:def 4;
then A3: j |^ (j |-count n) divides n by Def7;
A4: n gcd m <> 0 by INT_2:5;
then A5: j |^ (j |-count (n gcd m)) divides n gcd m by A2, Def7;
A6: not j |^ ((j |-count (n gcd m)) + 1) divides n gcd m by A2, A4, Def7;
A7: not j |^ ((j |-count m) + 1) divides m by A2, Def7;
A8: j |^ (j |-count m) divides m by A2, Def7;
n gcd m divides m by NAT_D:def 5;
then A9: j |^ (j |-count (n gcd m)) divides m by A5, NAT_D:4;
A10: (pfexp n) . j = j |-count n by Def8;
n gcd m divides n by NAT_D:def 5;
then A11: j |^ (j |-count (n gcd m)) divides n by A5, NAT_D:4;
A12: (pfexp m) . j = j |-count m by Def8;
A13: not j |^ ((j |-count n) + 1) divides n by A2, Def7;
thus (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i :: thesis: verum
proof
per cases ( (pfexp n) . j <= (pfexp m) . j or (pfexp n) . j > (pfexp m) . j ) ;
suppose A14: (pfexp n) . j <= (pfexp m) . j ; :: thesis: (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i
A15: now :: thesis: not j |-count (n gcd m) < j |-count n
assume A16: j |-count (n gcd m) < j |-count n ; :: thesis: contradiction
then j |-count (n gcd m) < j |-count m by A10, A12, A14, XXREAL_0:2;
then A17: j |^ ((j |-count (n gcd m)) + 1) divides m by A8, Th4;
j |^ ((j |-count (n gcd m)) + 1) divides n by A3, A16, Th4;
hence contradiction by A6, A17, NAT_D:def 5; :: thesis: verum
end;
A18: j |-count (n gcd m) <= j |-count n by A13, A11, Th4;
(min ((pfexp n),(pfexp m))) . j = j |-count n by A10, A14, Def3;
hence (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i by A1, A18, A15, XXREAL_0:1; :: thesis: verum
end;
suppose A19: (pfexp n) . j > (pfexp m) . j ; :: thesis: (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i
A20: now :: thesis: not j |-count (n gcd m) < j |-count m
assume A21: j |-count (n gcd m) < j |-count m ; :: thesis: contradiction
then j |-count (n gcd m) < j |-count n by A10, A12, A19, XXREAL_0:2;
then A22: j |^ ((j |-count (n gcd m)) + 1) divides n by A3, Th4;
j |^ ((j |-count (n gcd m)) + 1) divides m by A8, A21, Th4;
hence contradiction by A6, A22, NAT_D:def 5; :: thesis: verum
end;
A23: j |-count (n gcd m) <= j |-count m by A7, A9, Th4;
(min ((pfexp n),(pfexp m))) . j = j |-count m by A12, A19, Def3;
hence (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i by A1, A23, A20, XXREAL_0:1; :: thesis: verum
end;
end;
end;
end;
hence pfexp (n gcd m) = min ((pfexp n),(pfexp m)) ; :: thesis: verum