let n be Nat; :: thesis: ( n is odd iff ex k being Nat st n = (2 * k) + 1 )
hereby :: thesis: ( ex k being Nat st n = (2 * k) + 1 implies n is odd )
assume A1: n is odd ; :: thesis: ex j being Nat st n = (2 * j) + 1
then consider j being Integer such that
A2: n = (2 * j) + 1 by Th1;
now :: thesis: not j < 0
assume j < 0 ; :: thesis: contradiction
then A3: (2 * j) + 1 <= 2 * 0 by INT_1:7, XREAL_1:68;
per cases ( (2 * j) + 1 < 0 or (2 * j) + 1 = 0 ) by A3;
suppose (2 * j) + 1 < 0 ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum
end;
end;
end;
then j in NAT by INT_1:3;
then reconsider j = j as Nat ;
take j = j; :: thesis: n = (2 * j) + 1
thus n = (2 * j) + 1 by A2; :: thesis: verum
end;
thus ( ex k being Nat st n = (2 * k) + 1 implies n is odd ) ; :: thesis: verum