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 A1: ( p1 <> p2 & N = p1 * p2 ) ; :: thesis: ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2
consider q1 being Sophie_Germain Prime such that
A2: Euler p1 = 2 * q1 by SGSP3;
consider q2 being Sophie_Germain Prime such that
A3: Euler p2 = 2 * q2 by SGSP3;
( p1 > 1 & p2 > 1 ) by INT_2:def 5;
then Euler N = (Euler p1) * (Euler p2) by A1, INT_2:47, EULER_1:22
.= (4 * q1) * q2 by A2, A3 ;
hence ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 ; :: thesis: verum