:: 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 b₁ being even Integer holds b₁ is zero

proof end;

cluster trivial natural non zero -> odd for set ;

coherence
for b₁ being Nat st not b₁ is zero & b₁ is trivial holds
b₁ 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 b₁ being odd Nat holds b₁ 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 b₁ being trivial Nat holds
( b₁ = parity a iff b₁ = 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 b₁ 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;