:: Some Number Relations
:: by Sebastian Koch
::
:: Received December 27, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

:: not necessarily into MEMBERED - will cause unneeded expansions

registration

cluster natural -> natural-membered for set ;

coherence
for b₁ being Nat holds b₁ is natural-membered

proof end;

end;

definition

let X be set ;

func succRel X -> Relation of X means :Def1: :: RELSET_3:def 1
for x, y being set holds
( [x,y] in it iff ( x in X & y in X & y = succ x ) );

existence
ex b₁ being Relation of X st
for x, y being set holds
( [x,y] in b₁ iff ( x in X & y in X & y = succ x ) )

proof end;

uniqueness
for b₁, b₂ being Relation of X st ( for x, y being set holds
( [x,y] in b₁ iff ( x in X & y in X & y = succ x ) ) ) & ( for x, y being set holds
( [x,y] in b₂ iff ( x in X & y in X & y = succ x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines succRel RELSET_3:def 1 :
for X being set
for b₂ being Relation of X holds
( b₂ = succRel X iff for x, y being set holds
( [x,y] in b₂ iff ( x in X & y in X & y = succ x ) ) );

registration

let X be set ;

cluster succRel X -> asymmetric ;

coherence
succRel X is asymmetric

proof end;

end;

registration

cluster succRel {} -> empty ;

coherence
succRel {} is empty ;
let X be trivial set ;

cluster succRel X -> empty ;

coherence
succRel X is empty

proof end;

end;

theorem Th1: :: RELSET_3:1

for X, Y being set st X c= Y holds
succRel X c= succRel Y

proof end;

theorem :: RELSET_3:2

for X, Y being set holds succRel (X /\ Y) = (succRel X) /\ (succRel Y)

proof end;

theorem :: RELSET_3:3

for X, Y being set holds (succRel X) \/ (succRel Y) c= succRel (X \/ Y)

proof end;

theorem Th4: :: RELSET_3:4

for A, B, C being Ordinal holds
( [B,C] in succRel A iff ( succ B in A & C = succ B ) )

proof end;

theorem Th5: :: RELSET_3:5

for A, B being Ordinal st succ B in A holds
[B,(succ B)] in succRel A by Th4;

theorem Th6: :: RELSET_3:6

succRel 2 = {[0,1]}

proof end;

theorem Th7: :: RELSET_3:7

succRel 3 = {[0,1],[1,2]}

proof end;

theorem Th8: :: RELSET_3:8

succRel 4 = {[0,1],[1,2],[2,3]}

proof end;

theorem Th9: :: RELSET_3:9

succRel 5 = {[0,1],[1,2],[2,3],[3,4]}

proof end;

theorem :: RELSET_3:10

succRel omega = { [n,(n + 1)] where n is Nat : verum }

proof end;

registration

let z be Complex;

cluster (curry addcomplex) . z -> Relation-like Function-like ;

coherence
( (curry addcomplex) . z is Function-like & (curry addcomplex) . z is Relation-like )

proof end;

end;

definition

let X be complex-membered set ;
let z be Complex;

func addRel (X,z) -> Relation of X equals :: RELSET_3:def 2
((curry addcomplex) . z) |_2 X;

correctness
coherence
((curry addcomplex) . z) |_2 X is Relation of X;
;

end;

:: deftheorem defines addRel RELSET_3:def 2 :
for X being complex-membered set
for z being Complex holds addRel (X,z) = ((curry addcomplex) . z) |_2 X;

registration

let z be Complex;

cluster addRel ({},z) -> empty ;

coherence
addRel ({},z) is empty ;

end;

theorem Th11: :: RELSET_3:11

for z, z1, z2 being Complex
for X being complex-membered set holds
( [z1,z2] in addRel (X,z) iff ( z1 in X & z2 in X & z2 = z + z1 ) )

proof end;

theorem :: RELSET_3:12

for X being complex-membered set holds addRel (X,0) = id X

proof end;

registration

let X be complex-membered set ;
let z be non zero Complex;

cluster addRel (X,z) -> asymmetric ;

coherence
addRel (X,z) is asymmetric

proof end;

end;

theorem Th13: :: RELSET_3:13

for z being Complex
for X, Y being complex-membered set st X c= Y holds
addRel (X,z) c= addRel (Y,z)

proof end;

theorem :: RELSET_3:14

for z being Complex
for X, Y being complex-membered set holds addRel ((X /\ Y),z) = (addRel (X,z)) /\ (addRel (Y,z))

proof end;

theorem :: RELSET_3:15

for z being Complex
for X, Y being complex-membered set holds (addRel (X,z)) \/ (addRel (Y,z)) c= addRel ((X \/ Y),z)

proof end;

theorem :: RELSET_3:16

for z being Complex
for X being complex-membered set holds (addRel (X,z)) ~ = addRel (X,(- z))

proof end;

theorem Th17: :: RELSET_3:17

for z1, z2 being Complex
for X being complex-membered set holds (addRel (X,z1)) * (addRel (X,z2)) c= addRel (X,(z1 + z2))

proof end;

theorem :: RELSET_3:18

for z1, z2 being Complex holds (addRel (COMPLEX,z1)) * (addRel (COMPLEX,z2)) = addRel (COMPLEX,(z1 + z2))

proof end;

theorem :: RELSET_3:19

for z, z1 being Complex holds [z1,(z1 + z)] in addRel (COMPLEX,z)

proof end;

theorem :: RELSET_3:20

for z being Complex holds addRel (COMPLEX,z) = { [z1,(z1 + z)] where z1 is Complex : verum }

proof end;

registration

let r be Real;

cluster (curry addreal) . r -> Relation-like Function-like ;

coherence
( (curry addreal) . r is Function-like & (curry addreal) . r is Relation-like )

proof end;

end;

theorem :: RELSET_3:21

for r being Real
for X being real-membered set holds addRel (X,r) = ((curry addreal) . r) |_2 X

proof end;

theorem :: RELSET_3:22

for r, r1, r2 being Real
for X being real-membered set holds
( [r1,r2] in addRel (X,r) iff ( r1 in X & r2 in X & r2 = r + r1 ) ) by Th11;

theorem :: RELSET_3:23

for r1, r2 being Real holds (addRel (REAL,r1)) * (addRel (REAL,r2)) = addRel (REAL,(r1 + r2))

proof end;

theorem :: RELSET_3:24

for r, r1 being Real holds [r1,(r1 + r)] in addRel (REAL,r)

proof end;

theorem :: RELSET_3:25

for r being Real holds addRel (REAL,r) = { [r1,(r1 + r)] where r1 is Real : verum }

proof end;

registration

let q be Rational;

cluster (curry addrat) . q -> Relation-like Function-like ;

coherence
( (curry addrat) . q is Function-like & (curry addrat) . q is Relation-like )

proof end;

end;

theorem :: RELSET_3:26

for q being Rational
for X being rational-membered set holds addRel (X,q) = ((curry addrat) . q) |_2 X

proof end;

theorem :: RELSET_3:27

for q, q1, q2 being Rational
for X being rational-membered set holds
( [q1,q2] in addRel (X,q) iff ( q1 in X & q2 in X & q2 = q + q1 ) ) by Th11;

theorem :: RELSET_3:28

for q1, q2 being Rational holds (addRel (RAT,q1)) * (addRel (RAT,q2)) = addRel (RAT,(q1 + q2))

proof end;

theorem :: RELSET_3:29

for q, q1 being Rational holds [q1,(q1 + q)] in addRel (RAT,q)

proof end;

theorem :: RELSET_3:30

for q being Rational holds addRel (RAT,q) = { [q1,(q1 + q)] where q1 is Rational : verum }

proof end;

registration

let i be Integer;

cluster (curry addint) . i -> Relation-like Function-like ;

coherence
( (curry addint) . i is Function-like & (curry addint) . i is Relation-like )

proof end;

end;

theorem :: RELSET_3:31

for i being Integer
for X being integer-membered set holds addRel (X,i) = ((curry addint) . i) |_2 X

proof end;

theorem :: RELSET_3:32

for i, i1, i2 being Integer
for X being integer-membered set holds
( [i1,i2] in addRel (X,i) iff ( i1 in X & i2 in X & i2 = i + i1 ) ) by Th11;

theorem :: RELSET_3:33

for i1, i2 being Integer holds (addRel (INT,i1)) * (addRel (INT,i2)) = addRel (INT,(i1 + i2))

proof end;

theorem :: RELSET_3:34

for i, i1 being Integer holds [i1,(i1 + i)] in addRel (INT,i)

proof end;

theorem :: RELSET_3:35

for i being Integer holds addRel (INT,i) = { [i1,(i1 + i)] where i1 is Integer : verum }

proof end;

registration

let n be Nat;

cluster (curry addnat) . n -> Relation-like Function-like ;

coherence
( (curry addnat) . n is Function-like & (curry addnat) . n is Relation-like )

proof end;

end;

theorem :: RELSET_3:36

for n being Nat
for X being natural-membered set holds addRel (X,n) = ((curry addnat) . n) |_2 X

proof end;

theorem :: RELSET_3:37

for n, n1, n2 being Nat
for X being natural-membered set holds
( [n1,n2] in addRel (X,n) iff ( n1 in X & n2 in X & n2 = n + n1 ) ) by Th11;

theorem :: RELSET_3:38

for n1, n2 being Nat holds (addRel (NAT,n1)) * (addRel (NAT,n2)) = addRel (NAT,(n1 + n2))

proof end;

theorem :: RELSET_3:39

for n, n1 being Nat holds [n1,(n1 + n)] in addRel (NAT,n)

proof end;

theorem :: RELSET_3:40

for n being Nat holds addRel (NAT,n) = { [n1,(n1 + n)] where n1 is Nat : verum }

proof end;

theorem Th41: :: RELSET_3:41

for X being natural-membered set holds addRel (X,1) = succRel X

proof end;

registration

let z be Complex;

cluster (curry multcomplex) . z -> Relation-like Function-like ;

coherence
( (curry multcomplex) . z is Function-like & (curry multcomplex) . z is Relation-like )

proof end;

end;

definition

let X be complex-membered set ;
let z be Complex;

func multRel (X,z) -> Relation of X equals :: RELSET_3:def 3
((curry multcomplex) . z) |_2 X;

coherence
((curry multcomplex) . z) |_2 X is Relation of X ;

end;

:: deftheorem defines multRel RELSET_3:def 3 :
for X being complex-membered set
for z being Complex holds multRel (X,z) = ((curry multcomplex) . z) |_2 X;

registration

let z be Complex;

cluster multRel ({},z) -> empty ;

coherence
multRel ({},z) is empty ;

end;

theorem Th42: :: RELSET_3:42

for z, z1, z2 being Complex
for X being complex-membered set holds
( [z1,z2] in multRel (X,z) iff ( z1 in X & z2 in X & z2 = z * z1 ) )

proof end;

theorem :: RELSET_3:43

for X being complex-membered set st 0 in X holds
multRel (X,0) = [:X,{0}:]

proof end;

theorem :: RELSET_3:44

for X being complex-membered set holds multRel (X,1) = id X

proof end;

theorem :: RELSET_3:45

for z being Complex
for X being complex-membered set st z <> 1 & z <> - 1 & not 0 in X holds
multRel (X,z) is asymmetric

proof end;

theorem Th47: :: RELSET_3:46

for z being Complex
for X, Y being complex-membered set st X c= Y holds
multRel (X,z) c= multRel (Y,z)

proof end;

theorem :: RELSET_3:47

for z being Complex
for X, Y being complex-membered set holds multRel ((X /\ Y),z) = (multRel (X,z)) /\ (multRel (Y,z))

proof end;

theorem :: RELSET_3:48

for z being Complex
for X, Y being complex-membered set holds (multRel (X,z)) \/ (multRel (Y,z)) c= multRel ((X \/ Y),z)

proof end;

theorem :: RELSET_3:49

for z being Complex
for X being complex-membered set st z <> 0 holds
(multRel (X,z)) ~ = multRel (X,(z "))

proof end;

theorem Th51: :: RELSET_3:50

for z1, z2 being Complex
for X being complex-membered set holds (multRel (X,z1)) * (multRel (X,z2)) c= multRel (X,(z1 * z2))

proof end;

theorem :: RELSET_3:51

for z1, z2 being Complex holds (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) = multRel (COMPLEX,(z1 * z2))

proof end;

theorem :: RELSET_3:52

for z, z1 being Complex holds [z1,(z1 * z)] in multRel (COMPLEX,z)

proof end;

theorem :: RELSET_3:53

for z being Complex holds multRel (COMPLEX,z) = { [z1,(z1 * z)] where z1 is Complex : verum }

proof end;

registration

let r be Real;

cluster (curry multreal) . r -> Relation-like Function-like ;

coherence
( (curry multreal) . r is Function-like & (curry multreal) . r is Relation-like )

proof end;

end;

theorem :: RELSET_3:54

for r being Real
for X being real-membered set holds multRel (X,r) = ((curry multreal) . r) |_2 X

proof end;

theorem :: RELSET_3:55

for r, r1, r2 being Real
for X being real-membered set holds
( [r1,r2] in multRel (X,r) iff ( r1 in X & r2 in X & r2 = r * r1 ) ) by Th42;

theorem :: RELSET_3:56

for r1, r2 being Real holds (multRel (REAL,r1)) * (multRel (REAL,r2)) = multRel (REAL,(r1 * r2))

proof end;

theorem :: RELSET_3:57

for r, r1 being Real holds [r1,(r1 * r)] in multRel (REAL,r)

proof end;

theorem :: RELSET_3:58

for r being Real holds multRel (REAL,r) = { [r1,(r1 * r)] where r1 is Real : verum }

proof end;

registration

let q be Rational;

cluster (curry multrat) . q -> Relation-like Function-like ;

coherence
( (curry multrat) . q is Function-like & (curry multrat) . q is Relation-like )

proof end;

end;

theorem :: RELSET_3:59

for q being Rational
for X being rational-membered set holds multRel (X,q) = ((curry multrat) . q) |_2 X

proof end;

theorem :: RELSET_3:60

for q, q1, q2 being Rational
for X being rational-membered set holds
( [q1,q2] in multRel (X,q) iff ( q1 in X & q2 in X & q2 = q * q1 ) ) by Th42;

theorem :: RELSET_3:61

for q1, q2 being Rational holds (multRel (RAT,q1)) * (multRel (RAT,q2)) = multRel (RAT,(q1 * q2))

proof end;

theorem :: RELSET_3:62

for q, q1 being Rational holds [q1,(q1 * q)] in multRel (RAT,q)

proof end;

theorem :: RELSET_3:63

for q being Rational holds multRel (RAT,q) = { [q1,(q1 * q)] where q1 is Rational : verum }

proof end;

registration

let i be Integer;

cluster (curry multint) . i -> Relation-like Function-like ;

coherence
( (curry multint) . i is Function-like & (curry multint) . i is Relation-like )

proof end;

end;

theorem :: RELSET_3:64

for i being Integer
for X being integer-membered set holds multRel (X,i) = ((curry multint) . i) |_2 X

proof end;

theorem :: RELSET_3:65

for i, i1, i2 being Integer
for X being integer-membered set holds
( [i1,i2] in multRel (X,i) iff ( i1 in X & i2 in X & i2 = i * i1 ) ) by Th42;

theorem :: RELSET_3:66

for i1, i2 being Integer holds (multRel (INT,i1)) * (multRel (INT,i2)) = multRel (INT,(i1 * i2))

proof end;

theorem :: RELSET_3:67

for i, i1 being Integer holds [i1,(i1 * i)] in multRel (INT,i)

proof end;

theorem :: RELSET_3:68

for i being Integer holds multRel (INT,i) = { [i1,(i1 * i)] where i1 is Integer : verum }

proof end;

registration

let n be Nat;

cluster (curry multnat) . n -> Relation-like Function-like ;

coherence
( (curry multnat) . n is Function-like & (curry multnat) . n is Relation-like )

proof end;

end;

theorem :: RELSET_3:69

for n being Nat
for X being natural-membered set holds multRel (X,n) = ((curry multnat) . n) |_2 X

proof end;

theorem :: RELSET_3:70

for n, n1, n2 being Nat
for X being natural-membered set holds
( [n1,n2] in multRel (X,n) iff ( n1 in X & n2 in X & n2 = n * n1 ) ) by Th42;

theorem :: RELSET_3:71

for n1, n2 being Nat holds (multRel (NAT,n1)) * (multRel (NAT,n2)) = multRel (NAT,(n1 * n2))

proof end;

theorem :: RELSET_3:72

for n, n1 being Nat holds [n1,(n1 * n)] in multRel (NAT,n)

proof end;

theorem :: RELSET_3:73

for n being Nat holds multRel (NAT,n) = { [n1,(n1 * n)] where n1 is Nat : verum }

proof end;

definition

let n be non zero Nat;

func modRel n -> Relation of n equals :: RELSET_3:def 4
(addRel (n,1)) \/ {[(n - 1),0]};

coherence
(addRel (n,1)) \/ {[(n - 1),0]} is Relation of n

proof end;

end;

:: deftheorem defines modRel RELSET_3:def 4 :
for n being non zero Nat holds modRel n = (addRel (n,1)) \/ {[(n - 1),0]};

theorem :: RELSET_3:74

modRel 1 = {[0,0]}

proof end;

theorem :: RELSET_3:75

modRel 2 = {[0,1],[1,0]}

proof end;

theorem :: RELSET_3:76

modRel 3 = {[0,1],[1,2],[2,0]}

proof end;

theorem :: RELSET_3:77

modRel 4 = {[0,1],[1,2],[2,3],[3,0]}

proof end;

theorem :: RELSET_3:78

modRel 5 = {[0,1],[1,2],[2,3],[3,4],[4,0]}

proof end;