let a be integer number ; :: thesis: Leg (a,2) = a mod 2

per cases
( a is even or a is odd )
;

end;

suppose A2:
a is odd
; :: thesis: Leg (a,2) = a mod 2

reconsider amod2 = a mod 2 as Element of NAT by INT_1:3, INT_1:57;

A3: ( amod2 = 0 or amod2 = 1 ) by NAT_1:23, INT_1:58;

a - 1 = (((a div 2) * 2) + 1) - 1 by A3, A2, INT_1:62, INT_1:59;

then A4: 1,a are_congruent_mod 2 by INT_1:def 5, INT_1:14;

a gcd 2 <= 2 by INT_2:27, INT_2:21;

then A5: not not a gcd 2 = 0 & ... & not a gcd 2 = 2 ;

1 |^ (1 + 1) = 1 ;

hence Leg (a,2) = a mod 2 by A4, INT_2:5, A5, INT_2:21, A3, A2, INT_1:62, Def3, Th22; :: thesis: verum

end;A3: ( amod2 = 0 or amod2 = 1 ) by NAT_1:23, INT_1:58;

a - 1 = (((a div 2) * 2) + 1) - 1 by A3, A2, INT_1:62, INT_1:59;

then A4: 1,a are_congruent_mod 2 by INT_1:def 5, INT_1:14;

a gcd 2 <= 2 by INT_2:27, INT_2:21;

then A5: not not a gcd 2 = 0 & ... & not a gcd 2 = 2 ;

1 |^ (1 + 1) = 1 ;

hence Leg (a,2) = a mod 2 by A4, INT_2:5, A5, INT_2:21, A3, A2, INT_1:62, Def3, Th22; :: thesis: verum