let n be Nat; :: thesis: for p being Prime st p divides n holds

{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

let p be Prime; :: thesis: ( p divides n implies { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )

assume A1: p divides n ; :: thesis: { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

set B = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ;

set A = { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ;

thus { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } c= { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } :: according to XBOOLE_0:def 10 :: thesis: { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } c= { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }

assume x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ; :: thesis: x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }

then consider d being Element of NAT such that

A9: p * d = x and

A10: d > 0 and

A11: d divides n div p ;

reconsider d1 = x as Element of NAT by A9, ORDINAL1:def 12;

consider d2 being Nat such that

A12: n div p = d * d2 by A11, NAT_D:def 3;

(n div p) * p = (d * d2) * p by A12;

then n = d2 * (d * p) by A1, NAT_D:3;

then A13: d1 divides n by A9, NAT_D:def 3;

p divides d1 by A9, NAT_D:def 3;

hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A10, A13; :: thesis: verum

{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

let p be Prime; :: thesis: ( p divides n implies { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )

assume A1: p divides n ; :: thesis: { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

set B = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ;

set A = { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ;

thus { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } c= { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } :: according to XBOOLE_0:def 10 :: thesis: { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } c= { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } or x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } or x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )

assume x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ; :: thesis: x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

then consider d being Element of NAT such that

A2: d = x and

A3: d > 0 and

A4: d divides n and

A5: p divides d ;

consider d1 being Nat such that

A6: d = p * d1 by A5, NAT_D:def 3;

consider d2 being Nat such that

A7: n = d * d2 by A4, NAT_D:def 3;

n = p * (d1 * d2) by A6, A7;

then p divides n by NAT_D:def 3;

then p * (n div p) = p * (d1 * d2) by A6, A7, NAT_D:3;

then n div p = d1 * d2 by XCMPLX_1:5;

then A8: d1 divides n div p by NAT_D:def 3;

( d1 in NAT & d1 > 0 ) by A3, A6, ORDINAL1:def 12;

hence x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } by A2, A6, A8; :: thesis: verum

end;assume x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ; :: thesis: x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

then consider d being Element of NAT such that

A2: d = x and

A3: d > 0 and

A4: d divides n and

A5: p divides d ;

consider d1 being Nat such that

A6: d = p * d1 by A5, NAT_D:def 3;

consider d2 being Nat such that

A7: n = d * d2 by A4, NAT_D:def 3;

n = p * (d1 * d2) by A6, A7;

then p divides n by NAT_D:def 3;

then p * (n div p) = p * (d1 * d2) by A6, A7, NAT_D:3;

then n div p = d1 * d2 by XCMPLX_1:5;

then A8: d1 divides n div p by NAT_D:def 3;

( d1 in NAT & d1 > 0 ) by A3, A6, ORDINAL1:def 12;

hence x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } by A2, A6, A8; :: thesis: verum

assume x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ; :: thesis: x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }

then consider d being Element of NAT such that

A9: p * d = x and

A10: d > 0 and

A11: d divides n div p ;

reconsider d1 = x as Element of NAT by A9, ORDINAL1:def 12;

consider d2 being Nat such that

A12: n div p = d * d2 by A11, NAT_D:def 3;

(n div p) * p = (d * d2) * p by A12;

then n = d2 * (d * p) by A1, NAT_D:3;

then A13: d1 divides n by A9, NAT_D:def 3;

p divides d1 by A9, NAT_D:def 3;

hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A10, A13; :: thesis: verum