let i be Integer; :: thesis: ( i mod 2 = 0 or i mod 2 = 1 )
set A = (i div 2) * 2;
set M = i mod 2;
A1: i div 2 = [\(i / 2)/] by INT_1:def 9;
then (i / 2) - 1 < i div 2 by INT_1:def 6;
then ((i / 2) - 1) * 2 < (i div 2) * 2 by XREAL_1:68;
then - (i - 2) > - ((i div 2) * 2) by XREAL_1:24;
then i + (2 - i) > i + (- ((i div 2) * 2)) by XREAL_1:6;
then 2 > i - ((i div 2) * 2) ;
then A2: 2 > i mod 2 by INT_1:def 10;
i div 2 <= i / 2 by A1, INT_1:def 6;
then (i div 2) * 2 <= (i / 2) * 2 by XREAL_1:64;
then - i <= - ((i div 2) * 2) by XREAL_1:24;
then i + (- i) <= i + (- ((i div 2) * 2)) by XREAL_1:6;
then 0 <= i - ((i div 2) * 2) ;
then 0 <= i mod 2 by INT_1:def 10;
then reconsider M = i mod 2 as Element of NAT by INT_1:3;
M in { k where k is Nat : k < 2 } by A2;
then M in 2 by AXIOMS:4;
hence ( i mod 2 = 0 or i mod 2 = 1 ) by CARD_1:50, TARSKI:def 2; :: thesis: verum