let b be Nat; for a, m being non zero Nat st a,b are_coprime holds
(rng (ArProg (b,a))) /\ (Coprimes m) is infinite
let a, m be non zero Nat; ( a,b are_coprime implies (rng (ArProg (b,a))) /\ (Coprimes m) is infinite )
assume A1:
a,b are_coprime
; (rng (ArProg (b,a))) /\ (Coprimes m) is infinite
set P1 = { p where p is Prime : ( p divides m & p divides a ) } ;
set Q1 = { q where q is Prime : ( q divides m & q divides b ) } ;
set R1 = { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ;
A2:
{ p where p is Prime : ( p divides m & p divides a ) } is with_non-empty_elements
by Lm15;
A3:
{ p where p is Prime : ( p divides m & p divides a ) } is finite
by Lm17;
A4:
{ p where p is Prime : ( p divides m & p divides a ) } is natural-membered
by Lm19;
A5:
{ q where q is Prime : ( q divides m & q divides b ) } is with_non-empty_elements
by Lm15;
A6:
{ q where q is Prime : ( q divides m & q divides b ) } is finite
by Lm17;
A7:
{ q where q is Prime : ( q divides m & q divides b ) } is natural-membered
by Lm19;
A8:
{ r where r is Prime : ( r divides m & not r divides a & not r divides b ) } is with_non-empty_elements
by Lm16;
A9:
{ r where r is Prime : ( r divides m & not r divides a & not r divides b ) } is finite
by Lm18;
A10:
{ r where r is Prime : ( r divides m & not r divides a & not r divides b ) } is natural-membered
by Lm20;
set P = Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } );
set Q = Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } );
set R = Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } );
A11:
((a * (Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ))) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) + b,m are_coprime
proof
assume
not
((a * (Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ))) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) + b,
m are_coprime
;
contradiction
then consider p being
Prime such that A12:
p divides ((a * (Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ))) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) + b
and A13:
p divides m
by PYTHTRIP:def 2;
A14:
not
p divides Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } )
A16:
not
p divides Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } )
A19:
not
p divides Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } )
( (
p divides a or not
p divides a ) & (
p divides b or not
p divides b ) )
;
then
(
p in { p where p is Prime : ( p divides m & p divides a ) } or
p in { q where q is Prime : ( q divides m & q divides b ) } or
p in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } )
by A13;
hence
contradiction
by A2, A3, A4, A5, A6, A7, A8, A9, A10, A14, A16, A19, Th16;
verum
end;
set g = ArProg (b,a);
set X = (rng (ArProg (b,a))) /\ (Coprimes m);
A21:
dom (ArProg (b,a)) = NAT
by FUNCT_2:def 1;
A22:
(ArProg (b,a)) . ((Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } )) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) in rng (ArProg (b,a))
by A21, FUNCT_1:def 3;
(ArProg (b,a)) . ((Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } )) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) = (a * ((Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } )) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } )))) + b
by NUMBER06:7;
then
(ArProg (b,a)) . ((Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } )) * (Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ))) in Coprimes m
by A11;
then A23:
not (rng (ArProg (b,a))) /\ (Coprimes m) is empty
by A22, XBOOLE_0:def 4;
for x being Nat st x in (rng (ArProg (b,a))) /\ (Coprimes m) holds
ex y being Nat st
( y > x & y in (rng (ArProg (b,a))) /\ (Coprimes m) )
proof
let x be
Nat;
( x in (rng (ArProg (b,a))) /\ (Coprimes m) implies ex y being Nat st
( y > x & y in (rng (ArProg (b,a))) /\ (Coprimes m) ) )
assume A24:
x in (rng (ArProg (b,a))) /\ (Coprimes m)
;
ex y being Nat st
( y > x & y in (rng (ArProg (b,a))) /\ (Coprimes m) )
then
x in rng (ArProg (b,a))
by XBOOLE_0:def 4;
then consider w being
object such that A25:
w in dom (ArProg (b,a))
and A26:
(ArProg (b,a)) . w = x
by FUNCT_1:def 3;
reconsider w =
w as
Element of
NAT by A25, FUNCT_2:def 1;
take
b + ((m + w) * a)
;
( b + ((m + w) * a) > x & b + ((m + w) * a) in (rng (ArProg (b,a))) /\ (Coprimes m) )
A27:
(ArProg (b,a)) . w = b + (w * a)
by NUMBER06:7;
m + w > 0 + w
by XREAL_1:8;
then
(m + w) * a > w * a
by XREAL_1:68;
hence
b + ((m + w) * a) > x
by A26, A27, XREAL_1:8;
b + ((m + w) * a) in (rng (ArProg (b,a))) /\ (Coprimes m)
x in Coprimes m
by A24, XBOOLE_0:def 4;
then
ex
j being
Integer st
(
x = j &
j,
m are_coprime )
;
then
(a * m) + (b + (w * a)),
m are_coprime
by A26, A27, NUMBER04:64;
then A28:
b + ((m + w) * a) in Coprimes m
;
b + ((m + w) * a) = (ArProg (b,a)) . (m + w)
by NUMBER06:7;
then
b + ((m + w) * a) in rng (ArProg (b,a))
by A21, FUNCT_1:def 3;
hence
b + ((m + w) * a) in (rng (ArProg (b,a))) /\ (Coprimes m)
by A28, XBOOLE_0:def 4;
verum
end;
hence
(rng (ArProg (b,a))) /\ (Coprimes m) is infinite
by A23, NUMBER04:1; verum