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;

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

hence
p <> x
; :: thesis: verumassume A4:
p = x
; :: thesis: contradiction

end;per cases
( x is Rational or not x is Rational )
;

end;

suppose
x is not Rational
; :: thesis: contradiction

then
not x in RAT
;

then ( not x in RAT+ \/ [:{0},RAT+:] or x in {[0,0]} ) by NUMBERS:def 3, XBOOLE_0:def 5;

end;then ( not x in RAT+ \/ [:{0},RAT+:] or x in {[0,0]} ) by NUMBERS:def 3, XBOOLE_0:def 5;

per cases then
( x in {[0,0]} or ( not x in RAT+ & not x in [:{0},RAT+:] ) )
by XBOOLE_0:def 3;

end;

suppose
( not x in RAT+ & not x in [:{0},RAT+:] )
; :: thesis: contradiction

then
x in DEDEKIND_CUTS
by A1, ARYTM_2:def 2, XBOOLE_0:def 3;

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 {RAT+} ) by ARYTM_2:def 1, XBOOLE_0:def 5;

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+ ;

end;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 {RAT+} ) by ARYTM_2:def 1, XBOOLE_0:def 5;

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;

end;

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;n = {1,1} by A7;

hence contradiction by A7; :: thesis: verum

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 A7, A9, XTUPLE_0:1;

then j = 1 by A9, ARYTM_3:3;

hence contradiction by A8, A9; :: thesis: verum

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

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

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

then j = 1 by A9, ARYTM_3:3;

hence contradiction by A8, A9; :: thesis: verum