let p be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}

set F = F_Rat ;

set FX = Polynom-Ring F_Rat;

set I = {p} -Ideal ;

set K = (Polynom-Ring F_Rat) / ({p} -Ideal);

set x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal));

set F = F_Rat ;

set FX = Polynom-Ring F_Rat;

set I = {p} -Ideal ;

set K = (Polynom-Ring F_Rat) / ({p} -Ideal);

set x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal));

now :: thesis: not the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) <> {}

hence
the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}
; :: thesis: verumassume AS:
the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) <> {}
; :: thesis: contradiction

reconsider x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) as Element of F_Rat by AS, XBOOLE_0:def 4;

reconsider q = x as Element of ((Polynom-Ring F_Rat) / ({p} -Ideal)) by AS, XBOOLE_0:def 4;

consider a being Element of (Polynom-Ring F_Rat) such that

A1: q = Class ((EqRel ((Polynom-Ring F_Rat),({p} -Ideal))),a) by RING_1:11;

reconsider pa = a as Polynomial of F_Rat by POLYNOM3:def 10;

a - a = 0. (Polynom-Ring F_Rat) by RLVECT_1:15;

then A2: a in q by A1, RING_1:5, IDEAL_1:3;

XZ: x in (RAT+ \/ [:{0},RAT+:]) \ {[0,0]} by NUMBERS:def 3, RAT_1:def 2;

XX: not x in RAT+

end;reconsider x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) as Element of F_Rat by AS, XBOOLE_0:def 4;

reconsider q = x as Element of ((Polynom-Ring F_Rat) / ({p} -Ideal)) by AS, XBOOLE_0:def 4;

consider a being Element of (Polynom-Ring F_Rat) such that

A1: q = Class ((EqRel ((Polynom-Ring F_Rat),({p} -Ideal))),a) by RING_1:11;

reconsider pa = a as Polynomial of F_Rat by POLYNOM3:def 10;

a - a = 0. (Polynom-Ring F_Rat) by RLVECT_1:15;

then A2: a in q by A1, RING_1:5, IDEAL_1:3;

XZ: x in (RAT+ \/ [:{0},RAT+:]) \ {[0,0]} by NUMBERS:def 3, RAT_1:def 2;

XX: not x in RAT+

proof

not x in [:{0},RAT+:]
assume
x in RAT+
; :: thesis: contradiction

end;per cases then
( x in omega or x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } )
by XBOOLE_0:def 3, ARYTM_3:def 7;

end;

suppose
x in omega
; :: thesis: contradiction

then reconsider n = x as Element of omega ;

n = { m where m is Nat : m < n } by AXIOMS:4;

then consider m being Nat such that

B1: ( a = m & m < n ) by A2;

dom pa = NAT by FUNCT_2:def 1;

hence contradiction by B1; :: thesis: verum

end;n = { m where m is Nat : m < n } by AXIOMS:4;

then consider m being Nat such that

B1: ( a = m & m < n ) by A2;

dom pa = NAT by FUNCT_2:def 1;

hence contradiction by B1; :: thesis: verum

suppose
x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum }
; :: thesis: contradiction

then
x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) }
;

then consider i, j being Element of omega such that

A4: ( x = [i,j] & i,j are_coprime & j <> {} ) ;

A5: dom pa = NAT by FUNCT_2:def 1;

pa in {{i},{i,j}} by A2, A4, TARSKI:def 5;

end;then consider i, j being Element of omega such that

A4: ( x = [i,j] & i,j are_coprime & j <> {} ) ;

A5: dom pa = NAT by FUNCT_2:def 1;

pa in {{i},{i,j}} by A2, A4, TARSKI:def 5;

proof

hence
contradiction
by XZ, XX, XBOOLE_0:def 3; :: thesis: verum
assume
x in [:{0},RAT+:]
; :: thesis: contradiction

then consider y, z being object such that

A4: ( y in {0} & z in RAT+ & x = [y,z] ) by ZFMISC_1:def 2;

reconsider y = y as Element of NAT by A4, TARSKI:def 1;

A5: dom pa = NAT by FUNCT_2:def 1;

pa in {{y},{y,z}} by A2, A4, TARSKI:def 5;

end;then consider y, z being object such that

A4: ( y in {0} & z in RAT+ & x = [y,z] ) by ZFMISC_1:def 2;

reconsider y = y as Element of NAT by A4, TARSKI:def 1;

A5: dom pa = NAT by FUNCT_2:def 1;

pa in {{y},{y,z}} by A2, A4, TARSKI:def 5;

per cases then
( pa = {y} or pa = {y,z} )
by TARSKI:def 2;

end;

suppose
pa = {y,z}
; :: thesis: contradiction

end;

per cases then
( [0,(pa . 0)] = y or [0,(pa . 0)] = z )
by A5;

end;

suppose A7:
[0,(pa . 0)] = z
; :: thesis: contradiction

end;

per cases
( z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } or z in omega )
by A4, ARYTM_3:def 7, XBOOLE_0:def 3;

end;

suppose A9:
z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum }
; :: thesis: contradiction

then
z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) }
;

then consider i, j being Element of omega such that

A8: ( z = [i,j] & i,j are_coprime & j <> {} ) ;

i = 0 by A7, A8, XTUPLE_0:1;

then j = 1 by A8, ARYTM_3:3;

then z in { [k,1] where k is Element of omega : verum } by A8;

hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum

end;then consider i, j being Element of omega such that

A8: ( z = [i,j] & i,j are_coprime & j <> {} ) ;

i = 0 by A7, A8, XTUPLE_0:1;

then j = 1 by A8, ARYTM_3:3;

then z in { [k,1] where k is Element of omega : verum } by A8;

hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum