:: by Rafa{\l} Ziobro

::

:: Received June 29, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

registration

let a be Integer;

coherence

a mod a is zero by INT_1:50;

coherence

a mod 2 is natural by INT_1:57, INT_1:3;

end;
coherence

a mod a is zero by INT_1:50;

coherence

a mod 2 is natural by INT_1:57, INT_1:3;

registration
end;

registration

let a be even Integer;

coherence

a mod 2 is zero

(a + 1) mod 2 = 1

end;
coherence

a mod 2 is zero

proof end;

reducibility (a + 1) mod 2 = 1

proof end;

registration

let a be Nat;

let b be non zero Nat;

reducibility

a mod (a + b) = a

a div (a + b) is zero

end;
let b be non zero Nat;

reducibility

a mod (a + b) = a

proof end;

coherence a div (a + b) is zero

proof end;

registration

let a be non trivial Nat;

coherence

a |-count 1 is zero

a |-count (- 1) is zero

end;
coherence

a |-count 1 is zero

proof end;

coherence a |-count (- 1) is zero

proof end;

registration

let a be non trivial Nat;

let b be Nat;

reducibility

a |-count (a |^ b) = b

a |-count (- (a |^ b)) = b

end;
let b be Nat;

reducibility

a |-count (a |^ b) = b

proof end;

reducibility a |-count (- (a |^ b)) = b

proof end;

registration

existence

not for b_{1} being even Integer holds b_{1} is zero

for b_{1} being Nat st not b_{1} is zero & b_{1} is trivial holds

b_{1} is odd

end;
not for b

proof end;

coherence for b

b

proof end;

registration

not for b_{1} being odd Nat holds b_{1} is trivial
end;

cluster V6() non trivial epsilon-transitive epsilon-connected ordinal natural non zero complex V20() ext-real positive non negative integer dim-like V42() cardinal V75() odd for set ;

existence not for b

proof end;

registration
end;

:: min, max, absolute value

registration

let a, b be Integer;

coherence

(a + b) / (a gcd b) is integer

(a - b) / (a gcd b) is integer

end;
coherence

(a + b) / (a gcd b) is integer

proof end;

coherence (a - b) / (a gcd b) is integer

proof end;

theorem ABS1: :: NEWTON05:3

for a, b being Real holds

( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.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.| ) )

( ( |.(|.a.| - |.b.|).| = |.(a + b).| & |.(a - b).| = |.a.| + |.b.| ) iff ( not |.(|.a.| - |.b.|).| = |.(a - b).| or not |.(a + b).| = |.a.| + |.b.| ) )

proof end;

:: modular arithmetic

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) )

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 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 ) )

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

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;

:: 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),

:: 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;

coherence

parity a is trivial Nat ;

compatibility

for b_{1} being trivial Nat holds

( b_{1} = parity a iff b_{1} = 2 - (a gcd 2) )

end;
coherence

parity a is trivial Nat ;

compatibility

for b

( b

proof end;

registration
end;

definition

let a be Integer;

coherence

( ( a = 0 implies 0 is Nat ) & ( not a = 0 implies 2 |^ (2 |-count a) is Nat ) ) ;

consistency

for b_{1} being Nat holds verum
;

end;
coherence

( ( a = 0 implies 0 is Nat ) & ( not a = 0 implies 2 |^ (2 |-count a) is Nat ) ) ;

consistency

for b

:: 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) ) );

for a being Integer holds

( ( a = 0 implies Parity a = 0 ) & ( not a = 0 implies Parity a = 2 |^ (2 |-count a) ) );

registration
end;

registration

let a be non zero even Integer;

coherence

not Parity a is trivial

Parity a is even

end;
coherence

not Parity a is trivial

proof end;

coherence Parity a is even

proof end;

registration

let a be even Integer;

coherence

Parity a is even

not Parity (a + 1) is even

end;
coherence

Parity a is even

proof end;

coherence not Parity (a + 1) is even

proof end;

registration
end;

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

registration
end;

registration

let a be Integer;

reducibility

(Parity a) * (Oddity a) = a

Parity (Parity a) = Parity a

Oddity (Oddity a) = Oddity a

Parity (Oddity a) is trivial

a + (Parity a) is even

a - (Parity a) is even

a / (Parity a) is integer by Th1, Th3;

end;
reducibility

(Parity a) * (Oddity a) = a

proof end;

reducibility Parity (Parity a) = Parity a

proof end;

reducibility Oddity (Oddity a) = Oddity a

proof end;

coherence Parity (Oddity a) is trivial

proof end;

coherence a + (Parity a) is even

proof end;

coherence a - (Parity a) is even

proof end;

coherence a / (Parity a) is integer by Th1, Th3;

registration

let a be non zero Integer;

coherence

not a / (Parity a) is even

not a div (Parity a) is even

end;
coherence

not a / (Parity a) is even

proof end;

coherence not a div (Parity a) is even

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))

for c being non trivial Nat holds c |-count (a gcd b) = min ((c |-count a),(c |-count b))

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

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;

correctness

compatibility

Parity a = parity a;

compatibility

parity a = Parity a;

;

reducibility

a |^ (parity a) = a

end;
correctness

compatibility

Parity a = parity a;

proof end;

correctness compatibility

parity a = Parity a;

;

reducibility

a |^ (parity a) = a

proof end;

registration

let a be even Integer;

coherence

( a |^ (parity a) is trivial & not a |^ (parity a) is zero )

end;
coherence

( a |^ (parity a) is trivial & not a |^ (parity a) is zero )

proof end;

registration

let a be Integer;

reducibility

parity (parity a) = parity a ;

reducibility

Parity (parity a) = parity a

end;
reducibility

parity (parity a) = parity a ;

reducibility

Parity (parity a) = parity a

proof 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 ) )

( ( 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;

coherence

(parity a) + (Parity a) is even

(Parity a) - (parity a) is even

(Parity a) - (parity a) is natural

a + (parity a) is even

a - (parity a) is even

end;
coherence

(parity a) + (Parity a) is even

proof end;

coherence (Parity a) - (parity a) is even

proof end;

coherence (Parity a) - (parity a) is natural

proof end;

coherence a + (parity a) is even

proof end;

coherence a - (parity a) is even

proof end;

:: Some obvious theorems on parity

theorem :: NEWTON05:52

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 ) )

( ( 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)) )

( 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;

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

Parity a = Parity b

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)

Parity (a + b) >= (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))

Parity (a + b) = min ((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) )

( 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)) )

( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) )

proof end;

theorem :: NEWTON05:73

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)) )

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: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 ) )

( Parity a > Parity b iff ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) )

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 )

( min ((Parity a),(Parity b)) divides a & min ((Parity a),(Parity b)) divides b )

proof end;

registration

let a, b be non zero Integer;

coherence

(a + b) / (min ((Parity a),(Parity b))) is integer

end;
coherence

(a + b) / (min ((Parity a),(Parity b))) is integer

proof end;

registration
end;

registration
end;

registration
end;

registration

let a be square Integer;

coherence

Parity a is square

Oddity a is square

end;
coherence

Parity a is square

proof end;

coherence Oddity a 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 )

( Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1 )

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 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) ) )

( 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)

Parity (a + b) > (Parity a) + (Parity b)

proof end;