let R be Ring; :: thesis: for p being Polynomial of R
for r being Real st r in REAL+ holds
p <> r

let p be Polynomial of R; :: thesis: for r being Real st r in REAL+ holds
p <> r

let x be Real; :: thesis: ( x in REAL+ implies p <> x )
assume A1: x in REAL+ ; :: thesis: p <> x
A2: dom p = NAT by FUNCT_2:def 1;
then A3: ( [0,(p . 0)] in p & [1,(p . 1)] in p ) by FUNCT_1:def 2;
now :: thesis: not p = x
assume A4: p = x ; :: thesis: contradiction
per cases ( x is Rational or not x is Rational ) ;
suppose x is not Rational ; :: thesis: contradiction
then not x in RAT ;
then ( not x in RAT+ \/ or x in ) by ;
per cases then ( x in or ( not x in RAT+ & not x in ) ) by XBOOLE_0:def 3;
suppose ( not x in RAT+ & not x in ) ; :: thesis: contradiction
then x in DEDEKIND_CUTS by ;
then ( x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) )
}
& not x in ) by ;
then consider A being Subset of RAT+ such that
A6: ( x = A & ( for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ) ) ;
consider u being Element of A such that
A7: u = [0,(p . 0)] by A3, A4, A6;
u in A by A4, A6;
then reconsider u = u as Element of RAT+ ;
per cases ( u in omega or u 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;
suppose u in omega ; :: thesis: contradiction
then reconsider n = u as Element of omega ;
n = {1,1} by A7;
hence contradiction by A7; :: thesis: verum
end;
suppose u 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 A8: ( u in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } & not u 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
A9: ( u = [i,j] & i,j are_coprime & j <> {} ) ;
i = 0 by ;
then j = 1 by ;
hence contradiction by A8, A9; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence p <> x ; :: thesis: verum