let a, b be non zero Integer; :: thesis: ( a + b <> 0 & Parity a = Parity b implies Parity (a + b) >= (Parity a) + (Parity b) )
assume A0: a + b <> 0 ; :: thesis: ( not Parity a = Parity b or Parity (a + b) >= (Parity a) + (Parity b) )
reconsider k = 2 |-count a as Nat ;
assume A1: Parity a = Parity b ; :: thesis: Parity (a + b) >= (Parity a) + (Parity b)
reconsider l = (a / (Parity a)) + (b / (Parity b)) as even Integer ;
A2: l * (Parity a) = ((a / (Parity a)) * (Parity a)) + ((b / (Parity b)) * (Parity b)) by A1
.= ((a / (Parity a)) * (Parity a)) + b by XCMPLX_1:87
.= a + b by XCMPLX_1:87 ;
A3: 2 * (Parity a) = 2 * (2 |^ k) by Def1
.= 2 |^ (k + 1) by NEWTON:6 ;
2 divides l by ABIAN:def 1;
then ( not 2 is trivial & 2 |^ (k + 1) divides a + b ) by NEWTON03:5, A2, A3;
then 2 |-count (a + b) >= k + 1 by A0, NEWTON03:59;
then 2 |^ (k + 1) divides 2 |^ (2 |-count (a + b)) by PEPIN:31;
then 2 |^ (k + 1) divides Parity (a + b) by A0, Def1;
hence Parity (a + b) >= (Parity a) + (Parity b) by A0, A1, A3, NAT_D:7; :: thesis: verum