:: Application of Complex Classes to Number Theory
:: by Rafa{\l} Ziobro
::
:: Received May 11, 2025
:: Copyright (c) 2025 Association of Mizar Users

:: different registrations for COMPLEX3

registration

let a be weightless Complex;

cluster |.a.| -> weightless ;

coherence
|.a.| is weightless by COMPLEX3:def 3;

end;

registration

let a be light Complex;

cluster |.a.| -> light ;

coherence
|.a.| is light by COMPLEX3:def 2;

end;

registration

let a be heavy Complex;

cluster |.a.| -> heavy ;

coherence
|.a.| is heavy by COMPLEX3:def 1;

end;

registration

let a be positive heavy Real;
let b be negative Real;

cluster a - b -> heavy ;

coherence
a - b is heavy

proof end;

end;

registration

let a be negative heavy Real;
let b be positive Real;

cluster a - b -> heavy ;

coherence
a - b is heavy

proof end;

end;

registration

let a be positive non light Real;
let b be negative Real;

cluster a - b -> heavy ;

coherence
a - b is heavy

proof end;

end;

registration

let a be negative non light Real;
let b be positive Real;

cluster a - b -> heavy ;

coherence
a - b is heavy

proof end;

end;

registration

let a be non heavy Real;
let b be negative heavy Real;

cluster a - b -> positive ;

coherence
a - b is positive

proof end;

end;

registration

let a be light Real;
let b be negative non light Real;

cluster a - b -> positive ;

coherence
a - b is positive

proof end;

end;

registration

let a be non heavy Real;
let b be negative non light Real;

cluster a - b -> non negative ;

coherence
not a - b is negative

proof end;

end;

registration

let a be non heavy Real;
let b be positive heavy Real;

cluster a - b -> negative ;

coherence
a - b is negative

proof end;

end;

registration

let a be light Real;
let b be positive non light Real;

cluster a - b -> negative ;

coherence
a - b is negative

proof end;

end;

registration

let a be non heavy Real;
let b be positive non light Real;

cluster a - b -> non positive ;

coherence
not a - b is positive

proof end;

end;

registration

let a, b be positive light Real;

cluster a - b -> light ;

coherence
a - b is light

proof end;

end;

registration

let a, b be positive non heavy Real;

cluster a - b -> non heavy ;

coherence
not a - b is heavy

proof end;

end;

:: non integer numbers

registration

let a be Real;

cluster frac a -> non negative light ;

coherence
( frac a is light & not frac a is negative ) by INT_1:43;

reduce frac (frac a) to frac a;

reducibility
frac (frac a) = frac a

proof end;

end;

registration

let a be integer Real;

cluster frac a -> zero ;

coherence
frac a is zero by INT_1:45;

end;

registration

cluster complex real integer even ext-real weightless for object ;

existence
ex b₁ being even Integer st b₁ is weightless

proof end;

cluster non zero complex real integer odd ext-real weightless for object ;

existence
ex b₁ being odd Integer st b₁ is weightless

proof end;

cluster complex real integer ext-real heavy for object ;

existence
ex b₁ being Integer st b₁ is heavy

proof end;

cluster integer non weightless -> heavy for object ;

coherence
for b₁ being Integer st not b₁ is weightless holds
b₁ is heavy

proof end;

cluster non zero complex real integer odd ext-real heavy for object ;

existence
ex b₁ being odd Integer st b₁ is heavy

proof end;

cluster complex real integer even ext-real heavy for object ;

existence
ex b₁ being even Integer st b₁ is heavy

proof end;

cluster non zero complex real integer ext-real positive non negative heavy for object ;

existence
ex b₁ being positive Integer st b₁ is heavy

proof end;

cluster non zero complex real integer ext-real non positive negative heavy for object ;

existence
ex b₁ being negative Integer st b₁ is heavy

proof end;

end;

theorem N0344: :: NEWTON06:1

for a, b being non weightless Integer st a,b are_coprime holds
( not a divides b & not b divides a )

proof end;

registration

cluster complex real non integer ext-real for object ;

existence
not for b₁ being Real holds b₁ is integer

proof end;

end;

registration

let a be non integer Complex;

cluster - a -> non integer ;

coherence
not - a is integer

proof end;

end;

registration

let a be non integer Real;

cluster frac a -> positive light ;

coherence
( frac a is light & frac a is positive ) by INT_1:46;

end;

registration

let a be non integer Complex;
let b be non zero Integer;

cluster a + b -> non integer ;

coherence
not a + b is integer

proof end;

cluster a - b -> non integer ;

coherence
not a - b is integer

proof end;

cluster a / b -> non integer ;

coherence
not a / b is integer

proof end;

end;

registration

let b be positive light Real;

cluster [/b\] -> positive weightless ;

coherence
( [/b\] is weightless & [/b\] is positive )

proof end;

cluster [\b/] -> zero ;

coherence
[\b/] is zero

proof end;

reduce frac b to b;

reducibility
frac b = b

proof end;

let a be Integer;

reduce [\(a + b)/] to a;

reducibility
[\(a + b)/] = a

proof end;

reduce [/(a - b)\] to a;

reducibility
[/(a - b)\] = a

proof end;

reduce frac (a + b) to b;

reducibility
frac (a + b) = b

proof end;

end;

registration

let a be positive Real;

cluster [\a/] -> non negative ;

coherence
not [\a/] is negative by INT_1:54, COMPLEX3:2;

cluster [/a\] -> positive ;

coherence
[/a\] is positive by INT_1:31, INT_1:30;

end;

registration

let a be positive heavy Real;

cluster [\a/] -> positive ;

coherence
[\a/] is positive by INT_1:54, COMPLEX3:2;

end;

registration

let a be negative Real;

cluster [\a/] -> negative ;

coherence
[\a/] is negative by INT_1:def 6;

cluster [/a\] -> non positive ;

coherence
not [/a\] is positive by INT_1:65, XXREAL_0:def 7;

end;

registration

let a be negative heavy Real;

cluster [/a\] -> negative ;

coherence
[/a\] is negative by INT_1:65, COMPLEX3:2;

end;

registration

let a be Integer;
let b be negative light Real;

reduce [\(a - b)/] to a;

reducibility
[\(a - b)/] = a

proof end;

reduce [/(a + b)\] to a;

reducibility
[/(a + b)\] = a

proof end;

end;

:: inequalities in rounding products and fractions

theorem PI1: :: NEWTON06:2

for a, b being positive Real holds
( [\a/] * [\b/] <= [\a/] * b & [\a/] * b <= a * b )

proof end;

theorem :: NEWTON06:3

for a, b being positive Real holds [\a/] * [\b/] <= [\(a * b)/]

proof end;

theorem :: NEWTON06:4

for a, b being positive Real holds [\a/] / b <= a / b

proof end;

theorem :: NEWTON06:5

for a being positive Real
for b being positive heavy Real holds a / [\b/] >= a / b

proof end;

theorem INT162: :: NEWTON06:6

for a being Integer
for b being non zero Integer holds
( b divides a iff a mod b = 0 )

proof end;

theorem :: NEWTON06:7

for a being positive Real
for n being Nat holds [\(n * a)/] >= n * [\a/]

proof end;

registration

let a be Integer;

cluster a mod 1 -> zero ;

coherence
a mod 1 is zero by INT_2:12, INT162;

cluster a mod (- 1) -> zero ;

coherence
a mod (- 1) is zero by INT_2:12, INT162;

cluster a mod 0 -> zero ;

coherence
a mod 0 is zero by INT_1:def 10;
let b be weightless Integer;

cluster a mod b -> zero ;

coherence
a mod b is zero

proof end;

end;

registration

let a be Integer;
let b be non zero Nat;

cluster (a |^ b) mod a -> zero ;

coherence
(a |^ b) mod a is zero

proof end;

end;

registration

let a be Integer;
let b be non negative Integer;

cluster a mod b -> natural ;

coherence
a mod b is natural by INT_1:3, INT_1:57;

end;

registration

let a be odd Integer;
let b be non zero even Integer;

cluster a mod b -> odd ;

coherence
not a mod b is even

proof end;

end;

registration

let a be even Integer;
let b be non zero even Integer;

cluster a mod b -> even ;

coherence
a mod b is even

proof end;

end;

registration

let a be even Integer;

cluster (a |^ 4) mod 8 -> zero ;

coherence
(a |^ 4) mod 8 is zero

proof end;

end;

:: square

registration

cluster epsilon-transitive epsilon-connected ordinal natural complex real integer dim-like odd square ext-real non negative for set ;

existence
ex b₁ being square Nat st b₁ is odd

proof end;

end;

registration

let a, b be odd Integer;

cluster ((a |^ 2) - (b |^ 2)) / 2 -> even ;

coherence
((a |^ 2) - (b |^ 2)) / 2 is even

proof end;

cluster ((a |^ 2) + (b |^ 2)) / 2 -> odd ;

coherence
not ((a |^ 2) + (b |^ 2)) / 2 is even

proof end;

end;

registration

let a be square Integer;

cluster 2 -root a -> natural ;

coherence
2 -root a is natural

proof end;

reduce (2 -root a) * (2 -root a) to a;

reducibility
(2 -root a) * (2 -root a) = a

proof end;

end;

registration

let a be even square Integer;

cluster 2 -root a -> even ;

coherence
2 -root a is even

proof end;

cluster a / 2 -> even ;

coherence
a / 2 is even

proof end;

let b be odd square Integer;

cluster a - b -> non square ;

coherence
not a - b is square

proof end;

end;

registration

let a be odd square Integer;

cluster 2 -root a -> odd ;

coherence
not 2 -root a is even

proof end;

let b be odd square Integer;

cluster (a + b) / 2 -> odd ;

coherence
not (a + b) / 2 is even

proof end;

cluster (a - b) / 2 -> even ;

coherence
(a - b) / 2 is even

proof end;

end;

registration

let a be non negative Real;

cluster 2 -root a -> non negative ;

coherence
not 2 -root a is negative by POWER:7;

end;

registration

cluster natural complex real integer dim-like even square ext-real non negative for object ;

existence
ex b₁ being square Integer st b₁ is even

proof end;

cluster natural complex real integer dim-like odd square ext-real non negative for object ;

correctness
existence
ex b₁ being square Integer st b₁ is odd ;

proof end;

cluster epsilon-transitive epsilon-connected ordinal natural complex real integer dim-like even square ext-real non negative for set ;

existence
ex b₁ being square Nat st b₁ is even

proof end;

end;

registration

let n be non zero Nat;

reduce n -root 1 to 1;

reducibility
n -root 1 = 1 by POWER:6, NAT_1:14;

reduce n -root 0 to 0 ;

reducibility
n -root 0 = 0 by POWER:5, NAT_1:14;

end;

registration

let a be positive Real;
let n be non zero Nat;

cluster n -root a -> positive ;

coherence
n -root a is positive

proof end;

end;

theorem SFS: :: NEWTON06:8

for a being Nat holds
( ( a is square & a is square-free ) iff a = 1 )

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal natural complex real integer dim-like square square-free ext-real non negative for set ;

existence
ex b₁ being Nat st
( b₁ is square-free & b₁ is square )

proof end;

end;

registration

let a be even square Integer;

cluster a / 4 -> integer square ;

coherence
( a / 4 is square & a / 4 is integer )

proof end;

end;

registration

let a be non zero square Integer;

cluster 2 * a -> non square ;

coherence
not 2 * a is square by INT_2:28;

cluster a + a -> non square ;

coherence
not a + a is square

proof end;

end;

registration

let a be Integer;
let b, c be non zero Nat;

reduce (a mod b) mod (b * c) to a mod b;

reducibility
(a mod b) mod (b * c) = a mod b

proof end;

end;

registration

let b be non trivial Nat;

reduce 1 mod b to 1;

reducibility
1 mod b = 1 by NEWTON03:def 1, PEPIN:5;
let a be Nat;

reduce ((a * b) + 1) mod b to 1;

reducibility
((a * b) + 1) mod b = 1

proof end;

let n be Nat;

reduce (((a * b) + 1) |^ n) mod b to 1;

reducibility
(((a * b) + 1) |^ n) mod b = 1

proof end;

end;

registration

let b be non trivial Nat;
let n be even Nat;

reduce ((b - 1) |^ n) mod b to 1;

reducibility
((b - 1) |^ n) mod b = 1

proof end;

end;

registration

let b be non trivial Nat;
let n be odd Nat;

reduce ((b - 1) |^ n) mod b to b - 1;

reducibility
((b - 1) |^ n) mod b = b - 1

proof end;

end;

theorem MOP: :: NEWTON06:9

for a being Nat
for p being Prime holds
( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )

proof end;

registration

let a be Nat;

cluster a mod 2 -> square ;

coherence
a mod 2 is square

proof end;

cluster (a |^ 2) mod 3 -> square ;

coherence
(a |^ 2) mod 3 is square

proof end;

cluster (a |^ 2) mod 4 -> square ;

coherence
(a |^ 2) mod 4 is square

proof end;

cluster (a |^ 2) mod 5 -> square ;

coherence
(a |^ 2) mod 5 is square

proof end;

cluster (a |^ 2) mod 8 -> square ;

coherence
(a |^ 2) mod 8 is square

proof end;

let p be prime Nat;

cluster (a |^ (p - 1)) mod p -> square ;

coherence
(a |^ (p - 1)) mod p is square

proof end;

end;

theorem FRA: :: NEWTON06:10

for a being non integer Real holds (frac a) + (frac (- a)) = 1

proof end;

registration

let a be non integer Real;

cluster (frac a) + (frac (- a)) -> trivial non zero ;

coherence
( not (frac a) + (frac (- a)) is zero & (frac a) + (frac (- a)) is trivial )

proof end;

end;

theorem :: NEWTON06:11

for a being non integer Real holds
( - 1 < (frac a) - (frac (- a)) & (frac a) - (frac (- a)) < 1 )

proof end;

EFR: for a being non integer Real st frac a = frac (- a) holds
2 * a is odd Integer

proof end;

theorem :: NEWTON06:12

for a being non integer Real holds
( frac a = frac (- a) iff 2 * a is odd Integer )

proof end;

theorem FR1: :: NEWTON06:13

for a, b being Real holds frac (a * b) = frac (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b)))

proof end;

theorem FR2: :: NEWTON06:14

for a, b being Real holds frac (a * b) = frac ((([\a/] * (frac b)) + ([\b/] * (frac a))) + ((frac a) * (frac b)))

proof end;

theorem FR3: :: NEWTON06:15

for a being Real
for b being Integer holds frac (a * b) = frac (b * (frac a))

proof end;

theorem :: NEWTON06:16

for a being Real holds frac (a * a) = frac (((2 * a) * (frac a)) - ((frac a) * (frac a)))

proof end;

theorem :: NEWTON06:17

for a being Real holds frac (a * a) = frac (((2 * [\a/]) * (frac a)) + ((frac a) * (frac a)))

proof end;

theorem :: NEWTON06:18

for a being positive Real st frac a = 1 / 2 holds
frac (2 * a) = 0

proof end;

theorem :: NEWTON06:19

for a being positive Real st 1 / 2 > frac a holds
frac (2 * a) = 2 * (frac a)

proof end;

theorem :: NEWTON06:20

for a being positive Real st 1 / 2 < frac a holds
frac (2 * a) < frac a

proof end;

theorem DIV: :: NEWTON06:21

for a being Integer
for b being non zero Integer st not b divides a holds
(a div b) + ((- a) div b) = - 1

proof end;

theorem MOD: :: NEWTON06:22

for a being Integer
for b being non zero Integer holds
( not b divides a iff (a mod b) + ((- a) mod b) = b )

proof end;

theorem :: NEWTON06:23

for a, b being Integer holds
( (a mod b) + ((- a) mod b) = 0 or (a mod b) + ((- a) mod b) = b )

proof end;

theorem :: NEWTON06:24

for a being even Integer
for b being odd Integer holds
( a div b is odd iff a mod b is odd )

proof end;

theorem :: NEWTON06:25

for a, b being odd Integer holds
( a mod b is odd iff a div b is even )

proof end;

theorem MOO: :: NEWTON06:26

for a being Integer
for b being odd Integer st not b divides a holds
( a mod b is odd iff (- a) mod b is even )

proof end;

theorem DIM: :: NEWTON06:27

for a being non zero Integer
for b being Integer holds
( a divides b iff a divides b mod a )

proof end;

theorem :: NEWTON06:28

for a being non weightless Integer
for b being odd non weightless Integer st a,b are_coprime holds
(b + a) mod b <> (b - a) mod b

proof end;

theorem :: NEWTON06:29

for a being Integer
for b being even Integer st not b divides a & a mod b is odd holds
(- a) mod b is odd

proof end;

theorem :: NEWTON06:30

for a, b being non zero Integer holds
( not b mod a = (- b) mod a or a is even or a divides b )

proof end;

theorem COM: :: NEWTON06:31

for a, b being Nat st a,b are_coprime holds
for n being non trivial Nat holds max ((a mod n),(b mod n)) > 0

proof end;

theorem SM3: :: NEWTON06:32

for s being square Integer holds s mod 3 is trivial Nat

proof end;

theorem ESS: :: NEWTON06:33

for a, b being square Nat st (a + b) / 2 is square holds
a mod 3 = b mod 3

proof end;

theorem :: NEWTON06:34

for a, b being odd Nat st a,b are_coprime & ((a |^ 2) + (b |^ 2)) / 2 is square holds
not 3 divides a * b

proof end;

theorem :: NEWTON06:35

for a, b being Integer holds a div b = (- a) div (- b)

proof end;

theorem :: NEWTON06:36

for a, b being square Nat st a,b are_coprime & (a - b) / 2 is square holds
b mod 3 = 1

proof end;

theorem :: NEWTON06:37

for a being odd Nat holds 3 divides (2 |^ a) + 1

proof end;

theorem N0141: :: NEWTON06:38

for a, b, c, d being Integer st (a * b) gcd (c * d) = 1 holds
a gcd c = 1

proof end;

theorem :: NEWTON06:39

for a, b being Integer
for m, n being non zero Nat holds
( a,b are_coprime iff a |^ m,b |^ n are_coprime )

proof end;

theorem N02193: :: NEWTON06:40

for a, b being square Nat st a,b are_coprime holds
not 3 divides a + b

proof end;

theorem :: NEWTON06:41

for a, b being odd square Nat st a,b are_coprime holds
not 3 divides (a + b) / 2

proof end;

:: the uniqueness of coprime factorization

theorem :: NEWTON06:42

for a, b, c, d being Nat st a,c are_coprime & b,d are_coprime & a * b = c * d holds
( a = d & b = c )

proof end;

:: may be proved the other way

theorem CDN: :: NEWTON06:43

for a, b, c being Nat st a,b are_coprime & c divides a * b holds
(a gcd c) * (b gcd c) = c

proof end;

theorem :: NEWTON06:44

for a, b, c, d being Nat st a,b are_coprime & a * b = c * d holds
a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d)

proof end;

theorem :: NEWTON06:45

for a, b, c, d being positive Real st a * b = c * d & a * c = b * d holds
a = d

proof end;

theorem SDC: :: NEWTON06:46

for a, b being Integer st a,b are_coprime holds
((a - b) * (a + b)) gcd (a * b) = 1

proof end;

theorem :: NEWTON06:47

for a being odd Integer
for b being even Integer st a,b are_coprime holds
((a - b) * (a + b)) gcd ((2 * a) * b) = 1

proof end;

theorem SCP: :: NEWTON06:48

for a being even Integer
for b being Integer st a,b are_coprime holds
a + b,a - b are_coprime

proof end;

theorem :: NEWTON06:49

for a being even Integer
for b being Integer
for n being non zero Nat st a,b are_coprime holds
(b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime

proof end;

theorem RMI: :: NEWTON06:50

for a, b being Nat
for c, d being non zero Nat st a mod (c * d) = b mod (c * d) holds
a mod c = b mod c

proof end;

theorem MRS: :: NEWTON06:51

for a, b being non zero Nat holds (a - b) mod (2 * b) = (a + b) mod (2 * b)

proof end;

theorem :: NEWTON06:52

for a, b being non zero Nat st (a |^ 2) - (b |^ 2) in NAT holds
((a |^ 2) - (b |^ 2)) mod (2 * b) = ((a |^ 2) + (b |^ 2)) mod (2 * b)

proof end;

theorem :: NEWTON06:53

for a, b being non zero Nat holds ((a - b) |^ 2) mod ((4 * a) * b) = ((a + b) |^ 2) mod ((4 * a) * b)

proof end;

theorem :: NEWTON06:54

for a, b being odd Nat holds (((a - b) / 2) |^ 2) mod (a * b) = (((a + b) / 2) |^ 2) mod (a * b)

proof end;

theorem :: NEWTON06:55

for a, b, c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 holds
( (b |^ 2) mod a = (c |^ 2) mod a & (a |^ 2) mod b = (c |^ 2) mod b )

proof end;

theorem MT: :: NEWTON06:56

for a being Nat
for b being non trivial Nat
for c being non zero Nat st a mod (b * c) = 1 holds
a mod b = 1

proof end;

theorem :: NEWTON06:57

for a being Nat
for b, m, n being non zero Nat st m >= n & a mod (b |^ m) = 1 holds
a mod (b |^ n) = 1

proof end;

theorem :: NEWTON06:58

for i being Integer holds
( (i |^ 2) mod 4 = 0 or (i |^ 2) mod 4 = 1 )

proof end;

theorem MOS8: :: NEWTON06:59

for i being Integer holds
( (i |^ 2) mod 8 = 0 or (i |^ 2) mod 8 = 1 or (i |^ 2) mod 8 = 4 )

proof end;

theorem MOQ8: :: NEWTON06:60

for i being Integer holds
( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )

proof end;

theorem SDM: :: NEWTON06:61

for a, b being odd Integer holds
( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 )

proof end;

theorem SDO: :: NEWTON06:62

for a, b being odd Integer holds
( (a + b) mod 4 = 0 or (a - b) mod 4 = 0 )

proof end;

theorem :: NEWTON06:63

for a, b being odd Integer holds max (((a + b) mod 4),((a - b) mod 4)) = 2

proof end;

theorem :: NEWTON06:64

for a, b being odd Integer holds min (((a + b) mod 4),((a - b) mod 4)) = 0

proof end;

theorem MO5: :: NEWTON06:65

for a, b being Nat holds
( not a,b are_coprime or ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )

proof end;

theorem R3: :: NEWTON06:66

for a, b being Integer holds a mod b = b * (frac (a / b))

proof end;

theorem :: NEWTON06:67

for a being Integer
for b being non zero Integer holds frac (b * (frac (a / b))) = 0

proof end;

registration

let a be positive heavy Real;

cluster 1 / a -> positive light ;

coherence
( 1 / a is light & 1 / a is positive )

proof end;

end;

theorem :: NEWTON06:68

for b, c being positive Nat holds c * (frac (1 / (b + c))) < 1

proof end;

registration

let a be Integer;

reduce a div 1 to a;

reducibility
a div 1 = a by PRE_FF:2;

end;

registration

let a be non zero Integer;

reduce (1 * a) div a to 1;

reducibility
(1 * a) div a = 1 by INT_1:49;

end;

registration

let a be positive heavy Integer;

cluster 1 div a -> zero ;

coherence
1 div a is zero

proof end;

end;

registration

let a be positive heavy Integer;
let b be Integer;

cluster b div (a * b) -> zero ;

coherence
b div (a * b) is zero

proof end;

reduce b mod (a * b) to b;

reducibility
b mod (a * b) = b

proof end;

end;

theorem :: NEWTON06:69

for a, b, c being Integer holds (a * b) mod (a * c) = a * (b mod c)

proof end;

theorem CMI: :: NEWTON06:70

for a, b being non zero Integer
for c being Integer holds (c mod (a * b)) mod a = c mod a

proof end;

theorem :: NEWTON06:71

for a being Integer
for b being non zero Integer
for n being non zero Nat holds (a mod (b |^ n)) mod b = a mod b

proof end;

theorem MFR: :: NEWTON06:72

for a being non zero Nat
for b being Nat st b mod a < [/(a / 2)\] holds
frac (b / a) < 1 / 2

proof end;

theorem :: NEWTON06:73

for a being non zero Nat
for b being Nat st b mod a < [/(a / 2)\] holds
(2 * b) mod a = 2 * (b mod a)

proof end;

theorem MOD8: :: NEWTON06:74

for a being odd square Integer holds a mod 8 = 1

proof end;

registration

let a be square Integer;

cluster a mod 3 -> square ;

coherence
a mod 3 is square by SM3;

cluster a mod 4 -> square ;

coherence
a mod 4 is square

proof end;

cluster a mod 8 -> square ;

coherence
a mod 8 is square

proof end;

end;

theorem :: NEWTON06:75

for a being Integer holds (a |^ 4) mod 8 is trivial Nat

proof end;

theorem :: NEWTON06:76

for a being odd Integer holds (a |^ 4) mod 8 = 1

proof end;

theorem :: NEWTON06:77

for i being Integer holds
( (i |^ 4) mod 5 = 0 or (i |^ 4) mod 5 = 1 )

proof end;

theorem :: NEWTON06:78

for a, b being odd Nat holds
( not a,b are_coprime or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 )

proof end;

theorem :: NEWTON06:79

for a, b being Nat st a,b are_coprime holds
((a |^ 4) - (b |^ 4)) mod 5 is square

proof end;

theorem GRCY330: :: NEWTON06:80

for a, b being Integer
for n being Nat holds (a |^ n) mod b = ((a mod b) |^ n) mod b

proof end;

theorem :: NEWTON06:81

for a being Integer
for b being non zero Integer holds (a |^ 2) mod b = ((b - a) |^ 2) mod b

proof end;

theorem :: NEWTON06:82

for a, b being Integer
for c being odd Integer st (a + b) mod c = (a - b) mod c holds
c divides b

proof end;

theorem :: NEWTON06:83

for k being Integer holds
( ex a, b being Integer st (a |^ 2) - (b |^ 2) = k iff k mod 4 <> 2 )

proof end;