let a, b be non zero Integer; :: thesis: ( Parity (a + b) = (Parity a) + (Parity b) iff ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) ) )
thus ( Parity (a + b) = (Parity a) + (Parity b) implies ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) ) ) :: thesis: ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) implies Parity (a + b) = (Parity a) + (Parity b) )

proof

assume A1: Parity (a + b) = (Parity a) + (Parity b) ; :: thesis: ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) )
then A2: Parity a = Parity b by LEQ;
then 2 * (Parity a) = Parity (((Parity a) * (Oddity a)) + ((Parity b) * (Oddity b))) by A1
.= Parity ((Parity a) * ((Oddity a) + (Oddity b))) by A2
.= (Parity (Parity a)) * (Parity ((Oddity a) + (Oddity b))) by ILP
.= (Parity a) * (Parity ((Oddity a) + (Oddity b))) ;
hence ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) ) by A1, LEQ, PPD, XCMPLX_1:5; :: thesis: verum

end;

assume A1: ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) ) ; :: thesis: Parity (a + b) = (Parity a) + (Parity b)
Parity (a + b) = Parity (((Parity a) * (Oddity a)) + ((Parity b) * (Oddity b)))
.= Parity ((Parity a) * ((Oddity a) + (Oddity b))) by A1
.= (Parity (Parity a)) * (Parity ((Oddity a) + (Oddity b))) by ILP
.= 2 * (Parity a) by A1, PPD ;
hence Parity (a + b) = (Parity a) + (Parity b) by A1; :: thesis: verum