let n0, m0 be non zero Nat; :: thesis: for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds

n1 * m1 in NatDivisors (n0 * m0)

let n1, m1 be Nat; :: thesis: ( n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1 * m1 in NatDivisors (n0 * m0) )

reconsider b = n0 * m0 as non zero Nat ;

assume A1: n1 in NatDivisors n0 ; :: thesis: ( not m1 in NatDivisors m0 or n1 * m1 in NatDivisors (n0 * m0) )

then A2: 0 < n1 ;

A3: n1 divides n0 by A1, MOEBIUS1:39;

assume A4: m1 in NatDivisors m0 ; :: thesis: n1 * m1 in NatDivisors (n0 * m0)

then A5: 0 < m1 ;

then reconsider a = n1 * m1 as non zero Nat by A2;

A6: m1 divides m0 by A4, MOEBIUS1:39;

A7: n1 * m1 in NAT by ORDINAL1:def 12;

for p being Element of NAT st p is prime holds

p |-count a <= p |-count b

then n1 * m1 divides n0 * m0 by NAT_D:def 3;

hence n1 * m1 in NatDivisors (n0 * m0) by A2, A5, A7; :: thesis: verum

n1 * m1 in NatDivisors (n0 * m0)

let n1, m1 be Nat; :: thesis: ( n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1 * m1 in NatDivisors (n0 * m0) )

reconsider b = n0 * m0 as non zero Nat ;

assume A1: n1 in NatDivisors n0 ; :: thesis: ( not m1 in NatDivisors m0 or n1 * m1 in NatDivisors (n0 * m0) )

then A2: 0 < n1 ;

A3: n1 divides n0 by A1, MOEBIUS1:39;

assume A4: m1 in NatDivisors m0 ; :: thesis: n1 * m1 in NatDivisors (n0 * m0)

then A5: 0 < m1 ;

then reconsider a = n1 * m1 as non zero Nat by A2;

A6: m1 divides m0 by A4, MOEBIUS1:39;

A7: n1 * m1 in NAT by ORDINAL1:def 12;

for p being Element of NAT st p is prime holds

p |-count a <= p |-count b

proof

then
ex c being Element of NAT st n0 * m0 = (n1 * m1) * c
by NAT_4:20;
reconsider n19 = n1, m19 = m1 as non zero Nat by A1, A4;

let p be Element of NAT ; :: thesis: ( p is prime implies p |-count a <= p |-count b )

assume p is prime ; :: thesis: p |-count a <= p |-count b

then reconsider p9 = p as Prime ;

A8: ( p9 |-count (n19 * m19) = (p9 |-count n19) + (p9 |-count m19) & p9 |-count (n0 * m0) = (p9 |-count n0) + (p9 |-count m0) ) by NAT_3:28;

( p9 |-count n19 <= p9 |-count n0 & p9 |-count m19 <= p9 |-count m0 ) by A3, A6, NAT_3:30;

hence p |-count a <= p |-count b by A8, XREAL_1:7; :: thesis: verum

end;let p be Element of NAT ; :: thesis: ( p is prime implies p |-count a <= p |-count b )

assume p is prime ; :: thesis: p |-count a <= p |-count b

then reconsider p9 = p as Prime ;

A8: ( p9 |-count (n19 * m19) = (p9 |-count n19) + (p9 |-count m19) & p9 |-count (n0 * m0) = (p9 |-count n0) + (p9 |-count m0) ) by NAT_3:28;

( p9 |-count n19 <= p9 |-count n0 & p9 |-count m19 <= p9 |-count m0 ) by A3, A6, NAT_3:30;

hence p |-count a <= p |-count b by A8, XREAL_1:7; :: thesis: verum

then n1 * m1 divides n0 * m0 by NAT_D:def 3;

hence n1 * m1 in NatDivisors (n0 * m0) by A2, A5, A7; :: thesis: verum