let h be non zero Nat; :: thesis: for q being Prime st not q,h are_coprime holds
q divides h
let q be Prime; :: thesis: ( not q,h are_coprime implies q divides h )
set pq = prime_factorization q;
set ph = prime_factorization h;
A1: q = Product (prime_factorization q) by NAT_3:61;
A2: h = Product (prime_factorization h) by NAT_3:61;
assume not q,h are_coprime ; :: thesis: q divides h
then (support (prime_factorization q)) /\ (support (prime_factorization h)) <> {} by XBOOLE_0:def 7, INT_7:12, A1, A2;
then (support (pfexp q)) /\ (support (prime_factorization h)) <> {} by NAT_3:def 9;
then (support (pfexp q)) /\ (support (pfexp h)) <> {} by NAT_3:def 9;
then {q} /\ (support (pfexp h)) <> {} by NAT_3:43;
then consider x being object such that
A3: x in {q} /\ (support (pfexp h)) by XBOOLE_0:def 1;
A4: ( x in {q} & x in support (pfexp h) ) by A3, XBOOLE_0:def 4;
x = q by A4, TARSKI:def 1;
hence q divides h by NAT_3:36, A4; :: thesis: verum