let a be Integer; :: thesis: ( |.a.| <> 1 implies not (2 * a) * a is Prime )
assume A1: |.a.| <> 1 ; :: thesis: (2 * a) * a is not Prime
reconsider b = |.a.| as Element of NAT ;
A2: a * a = a ^2
.= |.a.| ^2 by COMPLEX1:75
.= b * b ;

per cases ( b < 2 or 2 <= b ) ;

suppose b < 2 ; :: thesis: (2 * a) * a is not Prime

then ( b = 0 or b = 1 ) by NAT_1:23;
hence (2 * a) * a is not Prime by A1, A2; :: thesis: verum

end;

suppose A3: 2 <= b ; :: thesis: (2 * a) * a is not Prime

1 < b by XXREAL_0:2, A3;
then A4: b * 1 < b * b by XREAL_1:68;
A5: 1 * (b * b) < 2 * (b * b) by A3, XREAL_1:68;
b divides (2 * b) * b by INT_1:def 3;
hence (2 * a) * a is not Prime by A2, A5, A4, INT_2:def 4; :: thesis: verum

end;

end;