let p1, p2 be Safe Prime; :: thesis: for N being Nat st p1 <> p2 & N = p1 * p2 holds

ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2

let N be Nat; :: thesis: ( p1 <> p2 & N = p1 * p2 implies ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 )

assume that

A1: p1 <> p2 and

A2: N = p1 * p2 ; :: thesis: ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2

A3: p2 > 1 by INT_2:def 4;

consider q2 being Sophie_Germain Prime such that

A4: Euler p2 = 2 * q2 by Th11;

consider q1 being Sophie_Germain Prime such that

A5: Euler p1 = 2 * q1 by Th11;

p1 > 1 by INT_2:def 4;

then Euler N = (Euler p1) * (Euler p2) by A1, A2, A3, EULER_1:21, INT_2:30

.= (4 * q1) * q2 by A5, A4 ;

hence ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 ; :: thesis: verum

ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2

let N be Nat; :: thesis: ( p1 <> p2 & N = p1 * p2 implies ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 )

assume that

A1: p1 <> p2 and

A2: N = p1 * p2 ; :: thesis: ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2

A3: p2 > 1 by INT_2:def 4;

consider q2 being Sophie_Germain Prime such that

A4: Euler p2 = 2 * q2 by Th11;

consider q1 being Sophie_Germain Prime such that

A5: Euler p1 = 2 * q1 by Th11;

p1 > 1 by INT_2:def 4;

then Euler N = (Euler p1) * (Euler p2) by A1, A2, A3, EULER_1:21, INT_2:30

.= (4 * q1) * q2 by A5, A4 ;

hence ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 ; :: thesis: verum