begin
begin
begin
begin
begin
theorem
for
m1,
m2,
m3,
a,
b,
c being ( (
integer ) (
complex real integer ext-real )
Integer) st
m1 : ( (
integer ) (
complex real integer ext-real )
Integer)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
m2 : ( (
integer ) (
complex real integer ext-real )
Integer)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
m3 : ( (
integer ) (
complex real integer ext-real )
Integer)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
m1 : ( (
integer ) (
complex real integer ext-real )
Integer) ,
m2 : ( (
integer ) (
complex real integer ext-real )
Integer)
are_relative_prime &
m1 : ( (
integer ) (
complex real integer ext-real )
Integer) ,
m3 : ( (
integer ) (
complex real integer ext-real )
Integer)
are_relative_prime &
m2 : ( (
integer ) (
complex real integer ext-real )
Integer) ,
m3 : ( (
integer ) (
complex real integer ext-real )
Integer)
are_relative_prime holds
ex
r,
s being ( (
integer ) (
complex real integer ext-real )
Integer) st
for
x being ( (
integer ) (
complex real integer ext-real )
Integer) st
(x : ( ( integer ) ( complex real integer ext-real ) Integer) - a : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) (
complex real integer ext-real )
set )
mod m1 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( (
integer ) (
complex real integer ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
(x : ( ( integer ) ( complex real integer ext-real ) Integer) - b : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) (
complex real integer ext-real )
set )
mod m2 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( (
integer ) (
complex real integer ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
(x : ( ( integer ) ( complex real integer ext-real ) Integer) - c : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) (
complex real integer ext-real )
set )
mod m3 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( (
integer ) (
complex real integer ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) holds
(
x : ( (
integer ) (
complex real integer ext-real )
Integer) ,
(a : ( ( integer ) ( complex real integer ext-real ) Integer) + (m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * r : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) ) : ( ( ) (
complex real integer ext-real )
set )
+ ((m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * m2 : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) * s : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) (
complex real integer ext-real )
set ) : ( ( ) (
complex real integer ext-real )
set )
are_congruent_mod (m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * m2 : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) (
complex real integer ext-real )
set )
* m3 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( ( ) (
complex real integer ext-real )
set ) &
((m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * r : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) - (b : ( ( integer ) ( complex real integer ext-real ) Integer) - a : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) ) : ( ( ) (
complex real integer ext-real )
set )
mod m2 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( (
integer ) (
complex real integer ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) &
(((m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * m2 : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) * s : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) - ((c : ( ( integer ) ( complex real integer ext-real ) Integer) - a : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) - (m1 : ( ( integer ) ( complex real integer ext-real ) Integer) * r : ( ( integer ) ( complex real integer ext-real ) Integer) ) : ( ( ) ( complex real integer ext-real ) set ) ) : ( ( ) ( complex real integer ext-real ) set ) ) : ( ( ) (
complex real integer ext-real )
set )
mod m3 : ( (
integer ) (
complex real integer ext-real )
Integer) : ( (
integer ) (
complex real integer ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real integer V31()
finite cardinal ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
NAT : ( ( ) ( non
empty V2()
epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() )
Element of
K6(
REAL : ( ( ) ( non
empty V2() non
finite complex-membered ext-real-membered real-membered V87() )
set ) ) : ( ( ) (
V2() non
finite )
set ) ) ) ) ;
begin