let i be Integer; :: thesis: ( not i is even iff ex j being Integer st i = (2 * j) + 1 )

hereby :: thesis: ( ex j being Integer st i = (2 * j) + 1 implies not i is even )

assume A1: not i is even ; :: thesis: not for j being Integer holds i <> (2 * j) + 1
assume A2: for j being Integer holds i <> (2 * j) + 1 ; :: thesis: contradiction
consider k being Element of NAT such that
A3: ( i = k or i = - k ) by INT_1:8;
consider m being Element of NAT such that
A4: ( k = 2 * m or k = (2 * m) + 1 ) by SCHEME1:1;

per cases ( ( i = k & k = 2 * m ) or ( i = - k & k = 2 * m ) or ( i = k & k = (2 * m) + 1 ) or ( i = - k & k = (2 * m) + 1 ) ) by A3, A4;

suppose ( i = k & k = 2 * m ) ; :: thesis: contradiction

hence contradiction by A1, Def1; :: thesis: verum

end;

suppose ( i = - k & k = 2 * m ) ; :: thesis: contradiction

then i = 2 * (- m) ;
hence contradiction by A1, Def1; :: thesis: verum

end;

suppose ( i = k & k = (2 * m) + 1 ) ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

suppose ( i = - k & k = (2 * m) + 1 ) ; :: thesis: contradiction

then i = (2 * (- (m + 1))) + 1 ;
hence contradiction by A2; :: thesis: verum

end;

end;

end;

given j being Integer such that A5: i = (2 * j) + 1 ; :: thesis: not i is even
given k being Integer such that A6: i = 2 * k ; :: according to ABIAN:def 1 :: thesis: contradiction
1 = 2 * (k - j) by A5, A6;
hence contradiction by INT_1:22; :: thesis: verum