let n be Nat; :: thesis: ex m being Element of NAT st
( n = 2 * m or n = (2 * m) + 1 )
take n div 2 ; :: thesis: ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 )
set k = n mod 2;
A1: ( n mod 2 = 0 or n mod 2 = 1 )
proof
n mod 2 < 1 + 1 by NAT_D:1;
then A2: n mod 2 <= 0 + 1 by NAT_1:13;
now :: thesis: ( n mod 2 = 0 or n mod 2 = 1 )
per cases ( n mod 2 <= 0 or n mod 2 = 0 + 1 ) by A2, NAT_1:8;
suppose n mod 2 <= 0 ; :: thesis: ( n mod 2 = 0 or n mod 2 = 1 )
hence ( n mod 2 = 0 or n mod 2 = 1 ) by NAT_1:2; :: thesis: verum
end;
suppose n mod 2 = 0 + 1 ; :: thesis: ( n mod 2 = 0 or n mod 2 = 1 )
hence ( n mod 2 = 0 or n mod 2 = 1 ) ; :: thesis: verum
end;
end;
end;
hence ( n mod 2 = 0 or n mod 2 = 1 ) ; :: thesis: verum
end;
n = (2 * (n div 2)) + (n mod 2) by NAT_D:2;
hence ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 ) by A1; :: thesis: verum