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

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