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 7;
then (i / 2) - 1 < i div 2 by INT_1:def 4;
then ((i / 2) - 1) * 2 < (i div 2) * 2 by XREAL_1:70;
then - (i - 2) > - ((i div 2) * 2) by XREAL_1:26;
then i + (2 - i) > i + (- ((i div 2) * 2)) by XREAL_1:8;
then 2 > i - ((i div 2) * 2) ;
then A2: 2 > i mod 2 by INT_1:def 8;
i div 2 <= i / 2 by A1, INT_1:def 4;
then (i div 2) * 2 <= (i / 2) * 2 by XREAL_1:66;
then - i <= - ((i div 2) * 2) by XREAL_1:26;
then i + (- i) <= i + (- ((i div 2) * 2)) by XREAL_1:8;
then 0 <= i - ((i div 2) * 2) ;
then 0 <= i mod 2 by INT_1:def 8;
then reconsider M = i mod 2 as Element of NAT by INT_1:16;
M in { k where k is Element of NAT : k < 2 } by A2;
then M in 2 by AXIOMS:30;
hence ( i mod 2 = 0 or i mod 2 = 1 ) by CARD_1:88, TARSKI:def 2; :: thesis: verum