let h, k, s, t be non zero Nat; :: thesis: ( h,k are_coprime & s * t = h * k & ( for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ) & ( for q being Prime st q in support (prime_factorization t) holds

not q,k are_coprime ) implies ( s = h & t = k ) )

assume A1: h,k are_coprime ; :: thesis: ( not s * t = h * k or ex q being Prime st

( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A2: s * t = h * k ; :: thesis: ( ex q being Prime st

( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A3: for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ; :: thesis: ( ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A4: for q being Prime st q in support (prime_factorization t) holds

not q,k are_coprime ; :: thesis: ( s = h & t = k )

set ps = prime_factorization s;

set ph = prime_factorization h;

set pt = prime_factorization t;

set pk = prime_factorization k;

A5: support (prime_factorization s) c= support (prime_factorization h) by A3, Th6;

A6: support (prime_factorization t) c= support (prime_factorization k) by A4, Th6;

support (pfexp h) misses support (pfexp k) by NAT_3:44, A1;

then support (prime_factorization h) misses support (pfexp k) by NAT_3:def 9;

then A7: support (prime_factorization h) misses support (prime_factorization k) by NAT_3:def 9;

set f = (prime_factorization s) + (prime_factorization t);

set g = (prime_factorization h) + (prime_factorization k);

A8: (prime_factorization s) + (prime_factorization t) is prime-factorization-like by A7, A5, A6, XBOOLE_1:64, Lm1;

A9: (prime_factorization h) + (prime_factorization k) is prime-factorization-like by A7, Lm1;

A10: Product ((prime_factorization h) + (prime_factorization k)) = (Product (prime_factorization h)) * (Product (prime_factorization k)) by A7, NAT_3:19

.= h * (Product (prime_factorization k)) by NAT_3:61

.= h * k by NAT_3:61 ;

A11: Product ((prime_factorization s) + (prime_factorization t)) = (Product (prime_factorization s)) * (Product (prime_factorization t)) by A5, A6, XBOOLE_1:64, A7, NAT_3:19

.= s * (Product (prime_factorization t)) by NAT_3:61

.= s * t by NAT_3:61 ;

(support (prime_factorization s)) \/ (support (prime_factorization t)) = support ((prime_factorization s) + (prime_factorization t)) by PRE_POLY:38

.= support ((prime_factorization h) + (prime_factorization k)) by A11, INT_7:15, A8, A9, A10, A2

.= (support (prime_factorization h)) \/ (support (prime_factorization k)) by PRE_POLY:38 ;

then A12: ( support (prime_factorization s) = support (prime_factorization h) & support (prime_factorization t) = support (prime_factorization k) ) by A5, A6, A7, Th1;

A13: support (prime_factorization s) = support (pfexp h) by A12, NAT_3:def 9;

A14: support (prime_factorization t) = support (pfexp k) by A12, NAT_3:def 9;

A15: for p being Nat st p in support (pfexp h) holds

(prime_factorization s) . p = p |^ (p |-count h)

(prime_factorization t) . p = p |^ (p |-count k)

.= Product (prime_factorization h) by A15, A13, NAT_3:def 9

.= h by NAT_3:61 ; :: thesis: t = k

thus t = Product (prime_factorization t) by NAT_3:61

.= Product (prime_factorization k) by A19, A14, NAT_3:def 9

.= k by NAT_3:61 ; :: thesis: verum

not q,h are_coprime ) & ( for q being Prime st q in support (prime_factorization t) holds

not q,k are_coprime ) implies ( s = h & t = k ) )

assume A1: h,k are_coprime ; :: thesis: ( not s * t = h * k or ex q being Prime st

( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A2: s * t = h * k ; :: thesis: ( ex q being Prime st

( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A3: for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ; :: thesis: ( ex q being Prime st

( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )

assume A4: for q being Prime st q in support (prime_factorization t) holds

not q,k are_coprime ; :: thesis: ( s = h & t = k )

set ps = prime_factorization s;

set ph = prime_factorization h;

set pt = prime_factorization t;

set pk = prime_factorization k;

A5: support (prime_factorization s) c= support (prime_factorization h) by A3, Th6;

A6: support (prime_factorization t) c= support (prime_factorization k) by A4, Th6;

support (pfexp h) misses support (pfexp k) by NAT_3:44, A1;

then support (prime_factorization h) misses support (pfexp k) by NAT_3:def 9;

then A7: support (prime_factorization h) misses support (prime_factorization k) by NAT_3:def 9;

set f = (prime_factorization s) + (prime_factorization t);

set g = (prime_factorization h) + (prime_factorization k);

A8: (prime_factorization s) + (prime_factorization t) is prime-factorization-like by A7, A5, A6, XBOOLE_1:64, Lm1;

A9: (prime_factorization h) + (prime_factorization k) is prime-factorization-like by A7, Lm1;

A10: Product ((prime_factorization h) + (prime_factorization k)) = (Product (prime_factorization h)) * (Product (prime_factorization k)) by A7, NAT_3:19

.= h * (Product (prime_factorization k)) by NAT_3:61

.= h * k by NAT_3:61 ;

A11: Product ((prime_factorization s) + (prime_factorization t)) = (Product (prime_factorization s)) * (Product (prime_factorization t)) by A5, A6, XBOOLE_1:64, A7, NAT_3:19

.= s * (Product (prime_factorization t)) by NAT_3:61

.= s * t by NAT_3:61 ;

(support (prime_factorization s)) \/ (support (prime_factorization t)) = support ((prime_factorization s) + (prime_factorization t)) by PRE_POLY:38

.= support ((prime_factorization h) + (prime_factorization k)) by A11, INT_7:15, A8, A9, A10, A2

.= (support (prime_factorization h)) \/ (support (prime_factorization k)) by PRE_POLY:38 ;

then A12: ( support (prime_factorization s) = support (prime_factorization h) & support (prime_factorization t) = support (prime_factorization k) ) by A5, A6, A7, Th1;

A13: support (prime_factorization s) = support (pfexp h) by A12, NAT_3:def 9;

A14: support (prime_factorization t) = support (pfexp k) by A12, NAT_3:def 9;

A15: for p being Nat st p in support (pfexp h) holds

(prime_factorization s) . p = p |^ (p |-count h)

proof

A19:
for p being Nat st p in support (pfexp k) holds
let p be Nat; :: thesis: ( p in support (pfexp h) implies (prime_factorization s) . p = p |^ (p |-count h) )

assume A16: p in support (pfexp h) ; :: thesis: (prime_factorization s) . p = p |^ (p |-count h)

then A17: p in support (prime_factorization h) by NAT_3:def 9;

A18: p in support (prime_factorization s) by A16, A12, NAT_3:def 9;

thus (prime_factorization s) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th3, A18, A5, A6, XBOOLE_1:64, A7

.= (prime_factorization h) . p by Th3, A17, A7, INT_7:15, A8, A9, A10, A2, A11

.= p |^ (p |-count h) by A16, NAT_3:def 9 ; :: thesis: verum

end;assume A16: p in support (pfexp h) ; :: thesis: (prime_factorization s) . p = p |^ (p |-count h)

then A17: p in support (prime_factorization h) by NAT_3:def 9;

A18: p in support (prime_factorization s) by A16, A12, NAT_3:def 9;

thus (prime_factorization s) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th3, A18, A5, A6, XBOOLE_1:64, A7

.= (prime_factorization h) . p by Th3, A17, A7, INT_7:15, A8, A9, A10, A2, A11

.= p |^ (p |-count h) by A16, NAT_3:def 9 ; :: thesis: verum

(prime_factorization t) . p = p |^ (p |-count k)

proof

thus s =
Product (prime_factorization s)
by NAT_3:61
let p be Nat; :: thesis: ( p in support (pfexp k) implies (prime_factorization t) . p = p |^ (p |-count k) )

assume A20: p in support (pfexp k) ; :: thesis: (prime_factorization t) . p = p |^ (p |-count k)

then A21: p in support (prime_factorization k) by NAT_3:def 9;

A22: p in support (prime_factorization t) by A12, A20, NAT_3:def 9;

thus (prime_factorization t) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th4, A22, A5, A6, XBOOLE_1:64, A7

.= (prime_factorization k) . p by Th4, A21, A7, A11, INT_7:15, A8, A9, A10, A2

.= p |^ (p |-count k) by A20, NAT_3:def 9 ; :: thesis: verum

end;assume A20: p in support (pfexp k) ; :: thesis: (prime_factorization t) . p = p |^ (p |-count k)

then A21: p in support (prime_factorization k) by NAT_3:def 9;

A22: p in support (prime_factorization t) by A12, A20, NAT_3:def 9;

thus (prime_factorization t) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th4, A22, A5, A6, XBOOLE_1:64, A7

.= (prime_factorization k) . p by Th4, A21, A7, A11, INT_7:15, A8, A9, A10, A2

.= p |^ (p |-count k) by A20, NAT_3:def 9 ; :: thesis: verum

.= Product (prime_factorization h) by A15, A13, NAT_3:def 9

.= h by NAT_3:61 ; :: thesis: t = k

thus t = Product (prime_factorization t) by NAT_3:61

.= Product (prime_factorization k) by A19, A14, NAT_3:def 9

.= k by NAT_3:61 ; :: thesis: verum