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

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

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

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 A1, A2;

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

hence contradiction by A3, Lm1; :: thesis: verum

end;

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

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

end;

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

hence contradiction by A4; :: thesis: verum

end;

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

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

end;

end;

end;

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