let a, b be non zero Integer; Parity (a + b) = (min ((Parity a),(Parity b))) * (Parity ((a + b) / (min ((Parity a),(Parity b)))))
A1:
( min ((Parity a),(Parity b)) = Parity a or min ((Parity a),(Parity b)) = Parity b )
by XXREAL_0:def 9;
min ((Parity a),(Parity b)) divides Parity a
by A1, XXREAL_0:def 9, PEPIN31;
then consider c being Nat such that
A2:
Parity a = (min ((Parity a),(Parity b))) * c
by NAT_D:def 3;
min ((Parity a),(Parity b)) divides Parity b
by A1, XXREAL_0:def 9, PEPIN31;
then consider d being Nat such that
A3:
Parity b = (min ((Parity a),(Parity b))) * d
by NAT_D:def 3;
( (Parity a) / (min ((Parity a),(Parity b))) = c & (Parity b) / (min ((Parity a),(Parity b))) = d )
by A2, A3, XCMPLX_1:89;
then A4:
( (Oddity a) * c = a / (min ((Parity a),(Parity b))) & (Oddity b) * d = b / (min ((Parity a),(Parity b))) )
by XCMPLX_1:98;
a + b =
((Oddity a) * ((min ((Parity a),(Parity b))) * c)) + ((Oddity b) * ((min ((Parity a),(Parity b))) * d))
by A2, A3
.=
(min ((Parity a),(Parity b))) * (((Oddity a) * c) + ((Oddity b) * d))
;
then Parity (a + b) =
(Parity (min ((Parity a),(Parity b)))) * (Parity (((Oddity a) * c) + ((Oddity b) * d)))
by ILP
.=
(min ((Parity a),(Parity b))) * (Parity (((Oddity a) * c) + ((Oddity b) * d)))
by A1
;
hence
Parity (a + b) = (min ((Parity a),(Parity b))) * (Parity ((a + b) / (min ((Parity a),(Parity b)))))
by A4, XCMPLX_1:62; verum