let a be Real; :: thesis: ( frac a = frac (- a) iff 2 * a is integer )

per cases ( a is integer or not a is integer ) ;

suppose a is integer ; :: thesis: ( frac a = frac (- a) iff 2 * a is integer )

then ( frac a = 0 & 0 = frac (- a) & 2 * a is integer ) ;
hence ( frac a = frac (- a) iff 2 * a is integer ) ; :: thesis: verum

end;

suppose not a is integer ; :: thesis: ( frac a = frac (- a) iff 2 * a is integer )

then reconsider a = a as non integer Real ;
B1: ( frac a = frac (- a) implies 2 * a is integer )

proof

assume frac a = frac (- a) ; :: thesis: 2 * a is integer
then (frac a) + (frac a) = 1 by FAA;
then (2 * [\a/]) + 1 = 2 * ([\a/] + (frac a))
.= 2 * a by INT_1:42 ;
hence 2 * a is integer ; :: thesis: verum

end;

( 2 * a is integer implies frac a = frac (- a) )

proof

assume C1: 2 * a is integer ; :: thesis: frac a = frac (- a)
2 * a = 2 * ([\a/] + (frac a)) by INT_1:42
.= (2 * [\a/]) + (2 * (frac a)) ;
then 2 * (frac a) is integer by C1;
then reconsider k = 2 * (frac a) as Nat ;
frac a < 1 by COMPLEX3:1;
then k < 2 * 1 by XREAL_1:68;
then C3: ( 2 * (frac a) = 0 or 2 * (frac a) = 1 ) by NAT_1:23;
( frac a = 1 / 2 implies (frac a) + (frac (- a)) = 1 ) by FAA;
hence frac a = frac (- a) by C3; :: thesis: verum

end;

hence ( frac a = frac (- a) iff 2 * a is integer ) by B1; :: thesis: verum

end;

end;