:: Parity as a Property of Integers
:: by Rafa{\l} Ziobro
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


registration
let a be Integer;
cluster a mod a -> zero ;
coherence
a mod a is zero by INT_1:50;
cluster a mod 2 -> natural ;
coherence
a mod 2 is natural by INT_1:57, INT_1:3;
end;

registration
let a, b be Integer;
reduce (a * b) gcd |.a.| to |.a.|;
reducibility
(a * b) gcd |.a.| = |.a.|
proof end;
end;

registration
let a be odd Nat;
cluster a mod 2 -> non zero ;
coherence
not a mod 2 is zero
proof end;
end;

registration
let a be even Integer;
cluster a mod 2 -> zero ;
coherence
a mod 2 is zero
proof end;
reduce (a + 1) mod 2 to 1;
reducibility
(a + 1) mod 2 = 1
proof end;
end;

registration
let a, b be Real;
cluster (max (a,b)) - (min (a,b)) -> non negative ;
coherence
not (max (a,b)) - (min (a,b)) is negative
proof end;
end;

registration
let a be Nat;
let b be non zero Nat;
reduce a mod (a + b) to a;
reducibility
a mod (a + b) = a
proof end;
cluster a div (a + b) -> zero ;
coherence
a div (a + b) is zero
proof end;
end;

registration
let a be non trivial Nat;
cluster a |-count 1 -> zero ;
coherence
a |-count 1 is zero
proof end;
cluster a |-count (- 1) -> zero ;
coherence
a |-count (- 1) is zero
proof end;
end;

registration
let a be non trivial Nat;
let b be Nat;
reduce a |-count (a |^ b) to b;
reducibility
a |-count (a |^ b) = b
proof end;
reduce a |-count (- (a |^ b)) to b;
reducibility
a |-count (- (a |^ b)) = b
proof end;
end;

theorem Th1: :: NEWTON05:1
for a, b being Integer st a divides b holds
b / a is integer
proof end;

registration
cluster non zero complex V20() ext-real integer even for object ;
existence
not for b1 being even Integer holds b1 is zero
proof end;
cluster trivial natural non zero -> odd for set ;
coherence
for b1 being Nat st not b1 is zero & b1 is trivial holds
b1 is odd
proof end;
end;

registration
cluster V6() non trivial epsilon-transitive epsilon-connected ordinal natural non zero complex V20() ext-real positive non negative integer dim-like odd for set ;
existence
not for b1 being odd Nat holds b1 is trivial
proof end;
end;

registration
let a be Integer;
let b be even Integer;
cluster a lcm b -> even ;
coherence
a lcm b is even
proof end;
end;

registration
let a, b be odd Integer;
cluster a lcm b -> odd ;
coherence
not a lcm b is even
proof end;
end;

:: min, max, absolute value
registration
let a, b be Integer;
cluster (a + b) / (a gcd b) -> integer ;
coherence
(a + b) / (a gcd b) is integer
proof end;
cluster (a - b) / (a gcd b) -> integer ;
coherence
(a - b) / (a gcd b) is integer
proof end;
end;

theorem ABS: :: NEWTON05:2
for a, b being Real holds
( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| )
proof end;

theorem ABS1: :: NEWTON05:3
for a, b being Real holds
( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )
proof end;

theorem LmABS: :: NEWTON05:4
for a, b being Real holds
( |.(|.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = |.a.| + |.b.| )
proof end;

theorem LABS: :: NEWTON05:5
for a, b being Real holds
( |.(a + b).| = |.a.| + |.b.| iff |.(a - b).| = |.(|.a.| - |.b.|).| )
proof end;

theorem :: NEWTON05:6
for a, b being non zero Real holds
( ( |.(|.a.| - |.b.|).| = |.(a + b).| & |.(a - b).| = |.a.| + |.b.| ) iff ( not |.(|.a.| - |.b.|).| = |.(a - b).| or not |.(a + b).| = |.a.| + |.b.| ) )
proof end;

theorem :: NEWTON05:7
for a, b being positive Real
for n being Nat holds min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n
proof end;

theorem :: NEWTON05:8
for a, b being positive Real
for n being Nat holds max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n
proof end;

theorem MIN1: :: NEWTON05:9
for a being non zero Nat
for m, n being Nat holds min ((a |^ n),(a |^ m)) = a |^ (min (n,m))
proof end;

theorem :: NEWTON05:10
for a being non zero Nat
for m, n being Nat holds max ((a |^ n),(a |^ m)) = a |^ (max (n,m))
proof end;

:: modular arithmetic
theorem AMB: :: NEWTON05:11
for a, b being Nat holds a mod b <= a
proof end;

theorem :: NEWTON05:12
for a being Nat
for b, c being non zero Nat holds (a mod c) + (b mod c) >= (a + b) mod c
proof end;

theorem :: NEWTON05:13
for a being Nat
for b, c being non zero Nat holds (a mod c) * (b mod c) >= (a * b) mod c
proof end;

theorem :: NEWTON05:14
for a being Nat
for b, n being non zero Nat holds (a mod b) |^ n >= (a |^ n) mod b
proof end;

theorem :: NEWTON05:15
for a being Nat
for b, n being non zero Nat st a mod b = 1 holds
(a |^ n) mod b = 1
proof end;

theorem :: NEWTON05:16
for a, b being Nat
for c being non zero Nat holds
( (a mod c) * (b mod c) < c iff (a * b) mod c = (a mod c) * (b mod c) )
proof end;

theorem :: NEWTON05:17
for a, b, c being Nat st (a mod c) * (b mod c) = c holds
(a * b) mod c = 0
proof end;

theorem :: NEWTON05:18
for a, b being Nat
for c being non zero Nat st (a mod c) * (b mod c) >= c holds
a mod c > 1
proof end;

theorem MAB: :: NEWTON05:19
for a, b being Integer
for c being non zero Nat holds
( ( (a + b) mod c = b mod c implies a mod c = 0 ) & ( (a + b) mod c <> b mod c implies a mod c > 0 ) )
proof end;

theorem :: NEWTON05:20
for a being Nat
for b, c being non zero Nat st (a * b) mod c = b holds
(a * (b gcd c)) mod c = b gcd c
proof end;

theorem :: NEWTON05:21
for a, b being Integer holds a,b are_congruent_mod a gcd b
proof end;

theorem N0319: :: NEWTON05:22
for k, l being odd square Integer holds (k - l) mod 8 = 0
proof end;

theorem :: NEWTON05:23
for k, l being odd square Integer holds (k + l) mod 8 = 2
proof end;

:: Two definitions of parity, denoted by small and capital letters are introduced.
:: Both are defined according to a typical "even/odd" distinction, not the
:: property itself (therefore 1 has non zero "parity"/"Parity").
:: "Parity" denoted by a capital letter results in the largest power of 2
:: which divides certain number (or zero if no such number could be given)
:: At the same time "parity" denoted by a small letter refers only to the
:: divisibility by 2 (therefore 2 has zero "parity", which could be misleading).
:: Although "oddness" could be used here instead of "parity", it would not
:: be compatible with "Parity" (moreover "even oddness" is also confusing),
definition
let a be Integer;
func parity a -> trivial Nat equals :: NEWTON05:def 1
a mod 2;
coherence
a mod 2 is trivial Nat
proof end;
end;

:: deftheorem defines parity NEWTON05:def 1 :
for a being Integer holds parity a = a mod 2;

definition
let a be Integer;
:: original: parity
redefine func parity a -> trivial Nat equals :: NEWTON05:def 2
2 - (a gcd 2);
coherence
parity a is trivial Nat ;
compatibility
for b1 being trivial Nat holds
( b1 = parity a iff b1 = 2 - (a gcd 2) )
proof end;
end;

:: deftheorem defines parity NEWTON05:def 2 :
for a being Integer holds parity a = 2 - (a gcd 2);

registration
let a be even Integer;
cluster parity a -> trivial zero ;
coherence
parity a is zero ;
end;

registration
let a be odd Integer;
cluster parity a -> trivial non zero ;
coherence
not parity a is zero
proof end;
end;

definition
let a be Integer;
func Parity a -> Nat equals :Def1: :: NEWTON05:def 3
 0 if a = 0
otherwise 2 |^ (2 |-count a);
coherence
( ( a = 0 implies 0 is Nat ) & ( not a = 0 implies 2 |^ (2 |-count a) is Nat ) ) ;
consistency
for b1 being Nat holds verum ;
end;

:: deftheorem Def1 defines Parity NEWTON05:def 3 :
for a being Integer holds
( ( a = 0 implies Parity a = 0 ) & ( not a = 0 implies Parity a = 2 |^ (2 |-count a) ) );

registration
let a be non zero Integer;
cluster Parity a -> non zero ;
coherence
not Parity a is zero
proof end;
end;

registration
let a be non zero even Integer;
cluster Parity a -> non trivial ;
coherence
not Parity a is trivial
proof end;
cluster Parity a -> even ;
coherence
Parity a is even
proof end;
end;

registration
let a be even Integer;
cluster Parity a -> even ;
coherence
Parity a is even
proof end;
cluster Parity (a + 1) -> odd ;
coherence
not Parity (a + 1) is even
proof end;
end;

registration
let a be odd Integer;
cluster Parity a -> trivial ;
coherence
Parity a is trivial
proof end;
end;

reconsider dwa = 2 as prime Nat by INT_2:28;

registration
let n be Nat;
reduce Parity (2 |^ n) to 2 |^ n;
reducibility
Parity (2 |^ n) = 2 |^ n
proof end;
end;

registration
reduce Parity 1 to 1;
reducibility
Parity 1 = 1
proof end;
reduce Parity 2 to 2;
reducibility
Parity 2 = 2
proof end;
end;

theorem Th3: :: NEWTON05:24
for a being Integer holds Parity a divides a
proof end;

theorem ILP: :: NEWTON05:25
for a, b being Integer holds Parity (a * b) = (Parity a) * (Parity b)
proof end;

definition
let a be Integer;
func Oddity a -> Integer equals :: NEWTON05:def 4
a / (Parity a);
coherence
a / (Parity a) is Integer by Th1, Th3;
end;

:: deftheorem defines Oddity NEWTON05:def 4 :
for a being Integer holds Oddity a = a / (Parity a);

theorem ADI: :: NEWTON05:26
for a being non zero Integer holds a / (Parity a) = a div (Parity a)
proof end;

registration
let a be Integer;
reduce (Parity a) * (Oddity a) to a;
reducibility
(Parity a) * (Oddity a) = a
proof end;
reduce Parity (Parity a) to Parity a;
reducibility
Parity (Parity a) = Parity a
proof end;
reduce Oddity (Oddity a) to Oddity a;
reducibility
Oddity (Oddity a) = Oddity a
proof end;
cluster Parity (Oddity a) -> trivial ;
coherence
Parity (Oddity a) is trivial
proof end;
cluster a + (Parity a) -> even ;
coherence
a + (Parity a) is even
proof end;
cluster a - (Parity a) -> even ;
coherence
a - (Parity a) is even
proof end;
cluster a / (Parity a) -> integer ;
coherence
a / (Parity a) is integer by Th1, Th3;
end;

theorem OPA: :: NEWTON05:27
for a being non zero Integer holds Oddity (Parity a) = 1
proof end;

theorem ILO: :: NEWTON05:28
for a, b being Integer holds Oddity (a * b) = (Oddity a) * (Oddity b)
proof end;

registration
let a be non zero Integer;
cluster a / (Parity a) -> odd ;
coherence
not a / (Parity a) is even
proof end;
cluster a div (Parity a) -> odd ;
coherence
not a div (Parity a) is even
proof end;
end;

theorem Th4: :: NEWTON05:29
for a, b being Integer holds
( Parity a divides Parity b or Parity b divides Parity a )
proof end;

theorem PEPIN31: :: NEWTON05:30
for a, b being non zero Integer holds
( Parity a divides Parity b iff Parity b >= Parity a )
proof end;

theorem P2P: :: NEWTON05:31
for a, b being non zero Integer st Parity a > Parity b holds
2 * (Parity b) divides Parity a
proof end;

theorem PM: :: NEWTON05:32
for a being Integer holds Parity a = Parity (- a)
proof end;

theorem PMP: :: NEWTON05:33
for a being Integer holds Parity a = Parity |.a.|
proof end;

theorem :: NEWTON05:34
for a being Integer holds Parity a <= |.a.|
proof end;

theorem PYTHTRIP10: :: NEWTON05:35
for a, b being Integer holds
( not a,b are_coprime or a is odd or b is odd )
proof end;

theorem MPO: :: NEWTON05:36
for a, b being odd Integer st |.a.| <> |.b.| holds
min ((Parity (a - b)),(Parity (a + b))) = 2
proof end;

theorem ODP: :: NEWTON05:37
for a, b being odd Integer holds min ((Parity (a - b)),(Parity (a + b))) <= 2
proof end;

theorem :: NEWTON05:38
for a, b being Integer st a,b are_coprime holds
min ((Parity (a - b)),(Parity (a + b))) <= 2
proof end;

theorem CCM: :: NEWTON05:39
for a, b being non zero Integer
for c being non trivial Nat holds c |-count (a gcd b) = min ((c |-count a),(c |-count b))
proof end;

theorem PGC: :: NEWTON05:40
for a, b being non zero Integer holds Parity (a gcd b) = min ((Parity a),(Parity b))
proof end;

theorem PGG: :: NEWTON05:41
for a, b being Integer holds (Parity a) gcd (Parity b) = Parity (a gcd b)
proof end;

theorem :: NEWTON05:42
for a being Nat holds Parity (2 * a) = 2 * (Parity a)
proof end;

theorem PLG: :: NEWTON05:43
for a, b being Integer holds (Parity a) lcm (Parity b) = Parity (a lcm b)
proof end;

theorem :: NEWTON05:44
for a, b being non zero Integer holds Parity (a lcm b) = max ((Parity a),(Parity b))
proof end;

theorem :: NEWTON05:45
for a, b being Integer holds Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b)))
proof end;

theorem PAN: :: NEWTON05:46
for a being Integer
for n being Nat holds Parity (a |^ n) = (Parity a) |^ n
proof end;

theorem :: NEWTON05:47
for a, b being non zero Integer
for n being Nat holds min ((Parity (a |^ n)),(Parity (b |^ n))) = (min ((Parity a),(Parity b))) |^ n
proof end;

registration
let a be odd Integer;
identify Parity a with parity a;
correctness
compatibility
Parity a = parity a;
proof end;
identify parity a with Parity a;
correctness
compatibility
parity a = Parity a;
;
reduce a |^ (parity a) to a;
reducibility
a |^ (parity a) = a
proof end;
end;

registration
let a be even Integer;
cluster a |^ (parity a) -> trivial non zero ;
coherence
( a |^ (parity a) is trivial & not a |^ (parity a) is zero )
proof end;
end;

registration
let a be Integer;
reduce parity (parity a) to parity a;
reducibility
parity (parity a) = parity a ;
reduce Parity (parity a) to parity a;
reducibility
Parity (parity a) = parity a
proof end;
end;

theorem PIP: :: NEWTON05:48
for a being Integer holds
( ( a is even implies parity a is even ) & ( parity a is even implies a is even ) & ( parity a is even implies Parity a is even ) & ( Parity a is even implies parity a is even ) )
proof end;

registration
let a be Integer;
cluster (parity a) + (Parity a) -> even ;
coherence
(parity a) + (Parity a) is even
proof end;
cluster (Parity a) - (parity a) -> even ;
coherence
(Parity a) - (parity a) is even
proof end;
cluster (Parity a) - (parity a) -> natural ;
coherence
(Parity a) - (parity a) is natural
proof end;
cluster a + (parity a) -> even ;
coherence
a + (parity a) is even
proof end;
cluster a - (parity a) -> even ;
coherence
a - (parity a) is even
proof end;
end;

:: Some obvious theorems on parity
theorem :: NEWTON05:49
for a being Integer holds parity (Parity a) = parity a
proof end;

theorem P1: :: NEWTON05:50
for a being Integer holds parity a = parity (- a)
proof end;

theorem PMI: :: NEWTON05:51
for a, b being Integer holds parity (a - b) = |.((parity a) - (parity b)).|
proof end;

theorem :: NEWTON05:52
for a, b being Integer holds parity (a + b) = parity ((parity a) + (parity b)) by NAT_D:66;

theorem PPM: :: NEWTON05:53
for a, b being Integer holds parity (a + b) = parity (a - b)
proof end;

theorem ABP: :: NEWTON05:54
for a, b being Integer holds parity (a + b) = |.((parity a) - (parity b)).|
proof end;

theorem :: NEWTON05:55
for a, b being Nat holds
( ( parity (a + b) = parity b implies parity a = 0 ) & ( parity (a + b) <> parity b implies parity a = 1 ) )
proof end;

theorem :: NEWTON05:56
for a, b being Integer holds
( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )
proof end;

theorem EVP: :: NEWTON05:57
for a, b being Integer holds
( a + b is even iff parity a = parity b )
proof end;

theorem :: NEWTON05:58
for a, b being Integer holds parity (a * b) = (parity a) * (parity b)
proof end;

theorem :: NEWTON05:59
for a, b being Integer holds parity (a lcm b) = parity (a * b)
proof end;

theorem :: NEWTON05:60
for a, b being Integer holds parity (a gcd b) = max ((parity a),(parity b))
proof end;

theorem :: NEWTON05:61
for a, b being Integer holds parity (a * b) = min ((parity a),(parity b))
proof end;

theorem :: NEWTON05:62
for a being Integer
for n being non zero Nat holds parity (a |^ n) = parity a
proof end;

PAP: for a, b being non zero Integer st Parity a > Parity b holds
Parity (a + b) = Parity b
proof end;

theorem LEQ: :: NEWTON05:63
for a, b being non zero Integer st Parity (a + b) >= (Parity a) + (Parity b) holds
Parity a = Parity b
proof end;

theorem :: NEWTON05:64
for a, b being Integer st Parity (a + b) > (Parity a) + (Parity b) holds
Parity a = Parity b
proof end;

theorem :: NEWTON05:65
for a, b being odd Integer
for m being odd Nat holds Parity ((a |^ m) + (b |^ m)) = Parity (a + b)
proof end;

theorem :: NEWTON05:66
for a, b being odd Integer
for m being even Nat holds Parity ((a |^ m) + (b |^ m)) = 2
proof end;

theorem PEQ: :: NEWTON05:67
for a, b being non zero Integer st a + b <> 0 & Parity a = Parity b holds
Parity (a + b) >= (Parity a) + (Parity b)
proof end;

theorem :: NEWTON05:68
for a, b being non zero Integer holds
( Parity (a + b) = Parity b iff Parity a > Parity b )
proof end;

theorem :: NEWTON05:69
for a, b being non zero Nat st Parity (a + b) < (Parity a) + (Parity b) holds
Parity (a + b) = min ((Parity a),(Parity b))
proof end;

theorem :: NEWTON05:70
for a, b being non zero Integer st a + b <> 0 & Parity (a + b) = Parity a holds
Parity a < Parity b
proof end;

theorem PGP: :: NEWTON05:71
for a being Integer holds
( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) )
proof end;

theorem ADA: :: NEWTON05:72
for a being Integer holds
( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) )
proof end;

theorem :: NEWTON05:73
for a, b being Integer st Parity a = Parity b holds
Parity (a + b) = Parity ((a + (Parity a)) + (b - (Parity b))) ;

theorem :: NEWTON05:74
for a being Nat holds Parity (a + (Parity a)) >= 2 * (Parity a)
proof end;

theorem :: NEWTON05:75
for a being Nat holds
( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a )
proof end;

theorem PSD: :: NEWTON05:76
for a, b being odd Integer holds Parity (a + b) <> Parity (a - b)
proof end;

theorem :: NEWTON05:77
for a, b being odd Integer st Parity (a + 1) = Parity (b - 1) holds
a <> b
proof end;

theorem PMG: :: NEWTON05:78
for a being odd Nat
for b being non trivial odd Nat holds
( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )
proof end;

theorem :: NEWTON05:79
for a, b being non zero Integer st Parity a > Parity b holds
a div (Parity b) is even
proof end;

theorem :: NEWTON05:80
for a, b being non zero Integer holds
( Parity a > Parity b iff ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) )
proof end;

theorem :: NEWTON05:81
for a being odd Nat holds Parity (a - 1) = 2 * (Parity (a div 2))
proof end;

theorem MPA: :: NEWTON05:82
for a, b being non zero Integer holds
( min ((Parity a),(Parity b)) divides a & min ((Parity a),(Parity b)) divides b )
proof end;

registration
let a, b be non zero Integer;
cluster (a + b) / (min ((Parity a),(Parity b))) -> integer ;
coherence
(a + b) / (min ((Parity a),(Parity b))) is integer
proof end;
end;

registration
let p be non square Integer;
let n be odd Nat;
cluster p |^ n -> non square ;
coherence
not p |^ n is square
proof end;
end;

registration
let a be Integer;
let n be even Nat;
cluster a |^ n -> square ;
coherence
a |^ n is square
proof end;
end;

registration
let p be prime Nat;
let a be non zero square Integer;
cluster p |-count a -> even ;
coherence
p |-count a is even
proof end;
end;

registration
let a be odd Integer;
cluster 2 * a -> non square ;
coherence
not 2 * a is square
proof end;
end;

registration
let a be square Integer;
cluster Parity a -> square ;
coherence
Parity a is square
proof end;
cluster Oddity a -> square ;
coherence
Oddity a is square
proof end;
end;

registration
let a be non zero square Integer;
cluster 2 |-count a -> even ;
coherence
2 |-count a is even by INT_2:28;
end;

theorem MMD: :: NEWTON05:83
for a, b being non negative Real holds (max (a,b)) - (min (a,b)) = |.(a - b).|
proof end;

theorem A4I: :: NEWTON05:84
for a being even Integer st not 4 divides a holds
not a is square
proof end;

theorem :: NEWTON05:85
for a, b being odd Integer st a - b is square holds
not a + b is square
proof end;

theorem :: NEWTON05:86
for a, b being non zero Integer holds Parity (a + b) = (min ((Parity a),(Parity b))) * (Parity ((a + b) / (min ((Parity a),(Parity b)))))
proof end;

theorem OPC: :: NEWTON05:87
for a, b being non zero Integer holds
( Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1 )
proof end;

theorem OMO: :: NEWTON05:88
for a being Integer holds |.(Oddity a).| = Oddity |.a.|
proof end;

theorem :: NEWTON05:89
for a, b being Integer holds (Oddity a) gcd (Oddity b) = Oddity (a gcd b)
proof end;

theorem :: NEWTON05:90
for a, b being non zero Integer holds a gcd b = ((Parity a) gcd (Parity b)) * ((Oddity a) gcd (Oddity b))
proof end;

theorem :: NEWTON05:91
for a being odd Nat holds
( Parity (a + 1) = 2 iff parity (a div 2) = 0 )
proof end;

theorem :: NEWTON05:92
for a being even Integer holds a div 2 = (a + 1) div 2
proof end;

theorem SAB: :: NEWTON05:93
for a, b being Integer holds a + b = ((2 * ((a div 2) + (b div 2))) + (parity a)) + (parity b)
proof end;

theorem SPA: :: NEWTON05:94
for a, b being odd Integer holds Parity (a + b) = 2 * (Parity (((a div 2) + (b div 2)) + 1))
proof end;

theorem PPD: :: NEWTON05:95
for a, b being odd Integer holds
( Parity (a + b) = 2 iff parity (a div 2) = parity (b div 2) )
proof end;

theorem PSU: :: NEWTON05:96
for a, b being non zero Integer holds
( Parity (a + b) = (Parity a) + (Parity b) iff ( Parity a = Parity b & parity ((Oddity a) div 2) = parity ((Oddity b) div 2) ) )
proof end;

theorem :: NEWTON05:97
for a, b being non zero Integer st a + b <> 0 & Parity a = Parity b & parity ((Oddity a) div 2) <> parity ((Oddity b) div 2) holds
Parity (a + b) > (Parity a) + (Parity b)
proof end;