let R be Ring; :: thesis: for p being Polynomial of R
for r being Rational st r in RAT+ & p = r holds
r = [1,2]

let p be Polynomial of R; :: thesis: for r being Rational st r in RAT+ & p = r holds
r = [1,2]

let r be Rational; :: thesis: ( r in RAT+ & p = r implies r = [1,2] )
assume A1: ( r in RAT+ & p = r ) ; :: thesis: r = [1,2]
A2: dom p = NAT by FUNCT_2:def 1;
not r in omega by ;
then r 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 ;
then A3: ( r in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } & not r in { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 5;
then consider i, j being Element of omega such that
A4: ( r = [i,j] & i,j are_coprime & j <> {} ) ;
[i,(p . i)] in p by ;
then {{i,(p . i)},{i}} in p by TARSKI:def 5;
then A5: {{i,(p . i)},{i}} in {{i,j},{i}} by ;
per cases ( {{i,(p . i)},{i}} = {i,j} or {{i,(p . i)},{i}} = {i} ) by ;
suppose A6: {{i,(p . i)},{i}} = {i,j} ; :: thesis: r = [1,2]
A7: j in {i,j} by TARSKI:def 2;
per cases ( j = {i} or j = {i,(p . i)} ) by ;
suppose j = {i} ; :: thesis: r = [1,2]
then i = 0 by Th2;
then j = 1 by ;
hence r = [1,2] by A3, A4; :: thesis: verum
end;
suppose A8: j = {i,(p . i)} ; :: thesis: r = [1,2]
per cases ( i = p . i or i <> p . i ) ;
suppose i = p . i ; :: thesis: r = [1,2]
then for o being object holds
( o in j iff o = i ) by ;
then j = {i} by TARSKI:def 1;
then i = {} by Th2;
then j = 1 by ;
hence r = [1,2] by A3, A4; :: thesis: verum
end;
suppose i <> p . i ; :: thesis: r = [1,2]
per cases then ( ( i = 1 & p . i = 0 ) or ( i = 0 & p . i = 1 ) ) by ;
suppose ( i = 1 & p . i = 0 ) ; :: thesis: r = [1,2]
hence r = [1,2] by ; :: thesis: verum
end;
suppose ( i = 0 & p . i = 1 ) ; :: thesis: r = [1,2]
then j = 1 by ;
hence r = [1,2] by A3, A4; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A11: {{i,(p . i)},{i}} = {i} ; :: thesis: r = [1,2]
{i,(p . i)} in {{i,(p . i)},{i}} by TARSKI:def 2;
then {i,(p . i)} = i by ;
then i in i by TARSKI:def 2;
hence r = [1,2] ; :: thesis: verum
end;
end;