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

suppose A1: a is odd ; :: thesis: for b₁ being trivial Nat holds
( b₁ = parity a iff b₁ = 2 - (a gcd 2) )

then a mod 2 <> 0 by INT_1:62;
hence for b₁ being trivial Nat holds
( b₁ = parity a iff b₁ = 2 - (a gcd 2) ) by A1, PRE_FF:6; :: thesis: verum

end;

suppose a is even ; :: thesis: for b₁ being trivial Nat holds
( b₁ = parity a iff b₁ = 2 - (a gcd 2) )

hence for b₁ being trivial Nat holds
( b₁ = parity a iff b₁ = 2 - (a gcd 2) ) by INT_1:62; :: thesis: verum

end;

end;