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