let m, n be non empty Nat; :: thesis: pfexp (n gcd m) = min (pfexp n),(pfexp m)

now

let i be set ; :: 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 lhs = pfexp (n gcd m);
set rhs = min (pfexp n),(pfexp m);
set x = j |-count n;
set y = j |-count m;
set z = j |-count (n gcd m);
A1: j <> 1 by INT_2:def 5;
A2: n gcd m <> 0 by INT_2:5;
A3: (pfexp (n gcd m)) . j = j |-count (n gcd m) by Def8;
A4: j |^ (j |-count (n gcd m)) divides n gcd m by A1, A2, Def7;
A5: not j |^ ((j |-count (n gcd m)) + 1) divides n gcd 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: n gcd m divides m by NAT_D:def 5;
A13: n gcd m divides n by NAT_D:def 5;
A14: j |^ (j |-count (n gcd m)) divides m by A4, A12, NAT_D:4;
A15: j |^ (j |-count (n gcd m)) divides n by A4, A13, NAT_D:4;
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 A16: (pfexp n) . j <= (pfexp m) . j ; :: thesis: (pfexp (n gcd m)) . i = (min (pfexp n),(pfexp m)) . i

then A17: (min (pfexp n),(pfexp m)) . j = j |-count n by A6, Def3;
A18: j |-count (n gcd m) <= j |-count n by A8, A15, Th4;

now

assume A19: j |-count (n gcd m) < j |-count n ; :: thesis: contradiction
then A20: j |^ ((j |-count (n gcd m)) + 1) divides n by A7, Th4;
j |-count (n gcd m) < j |-count m by A6, A9, A16, A19, XXREAL_0:2;
then j |^ ((j |-count (n gcd m)) + 1) divides m by A10, Th4;
hence contradiction by A5, A20, NAT_D:def 5; :: thesis: verum

end;

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

end;

suppose A21: (pfexp n) . j > (pfexp m) . j ; :: thesis: (pfexp (n gcd m)) . i = (min (pfexp n),(pfexp m)) . i

then A22: (min (pfexp n),(pfexp m)) . j = j |-count m by A9, Def3;
A23: j |-count (n gcd m) <= j |-count m by A11, A14, Th4;

now

assume A24: j |-count (n gcd m) < j |-count m ; :: thesis: contradiction
then A25: j |^ ((j |-count (n gcd m)) + 1) divides m by A10, Th4;
j |-count (n gcd m) < j |-count n by A6, A9, A21, A24, XXREAL_0:2;
then j |^ ((j |-count (n gcd m)) + 1) divides n by A7, Th4;
hence contradiction by A5, A25, NAT_D:def 5; :: thesis: verum

end;

hence (pfexp (n gcd m)) . i = (min (pfexp n),(pfexp m)) . i by A3, A22, A23, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

hence pfexp (n gcd m) = min (pfexp n),(pfexp m) by PBOOLE:3; :: thesis: verum