:: ARYTM_2 semantic presentation begin definition func DEDEKIND_CUTS -> Subset-Family of RAT+ equals :: ARYTM_2:def 1 { 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 ) ) } \ {RAT+}; coherence { 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 ) ) } \ {RAT+} is Subset-Family of RAT+ proof set C = { 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 ) ) } ; { 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 ) ) } c= bool RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e 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 ) ) } or e in bool RAT+ ) assume e 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 ) ) } ; ::_thesis: e in bool RAT+ then ex A being Subset of RAT+ st ( e = 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 ) ) ) ) ; hence e in bool RAT+ ; ::_thesis: verum end; hence { 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 ) ) } \ {RAT+} is Subset-Family of RAT+ by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem defines DEDEKIND_CUTS ARYTM_2:def_1_:_ DEDEKIND_CUTS = { 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 ) ) } \ {RAT+}; registration cluster DEDEKIND_CUTS -> non empty ; coherence not DEDEKIND_CUTS is empty proof set X = { s where s is Element of RAT+ : s < one } ; A1: { s where s is Element of RAT+ : s < one } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < one } or e in RAT+ ) assume e in { s where s is Element of RAT+ : s < one } ; ::_thesis: e in RAT+ then ex s being Element of RAT+ st ( s = e & s < one ) ; hence e in RAT+ ; ::_thesis: verum end; now__::_thesis:_not_one_in__{__s_where_s_is_Element_of_RAT+_:_s_<_one__}_ assume one in { s where s is Element of RAT+ : s < one } ; ::_thesis: contradiction then ex s being Element of RAT+ st ( s = one & s < one ) ; hence contradiction ; ::_thesis: verum end; then A2: { s where s is Element of RAT+ : s < one } <> RAT+ ; {} <=' one by ARYTM_3:64; then {} < one by ARYTM_3:68; then {} in { s where s is Element of RAT+ : s < one } ; then reconsider X = { s where s is Element of RAT+ : s < one } as non empty Subset of RAT+ by A1; for r being Element of RAT+ st r in X holds ( ( for s being Element of RAT+ st s <=' r holds s in X ) & ex s being Element of RAT+ st ( s in X & r < s ) ) proof let r be Element of RAT+ ; ::_thesis: ( r in X implies ( ( for s being Element of RAT+ st s <=' r holds s in X ) & ex s being Element of RAT+ st ( s in X & r < s ) ) ) assume r in X ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds s in X ) & ex s being Element of RAT+ st ( s in X & r < s ) ) then A3: ex s being Element of RAT+ st ( s = r & s < one ) ; thus for s being Element of RAT+ st s <=' r holds s in X ::_thesis: ex s being Element of RAT+ st ( s in X & r < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in X ) assume s <=' r ; ::_thesis: s in X then s < one by A3, ARYTM_3:67; hence s in X ; ::_thesis: verum end; consider s being Element of RAT+ such that A4: r < s and A5: s < one by A3, ARYTM_3:93; take s ; ::_thesis: ( s in X & r < s ) thus s in X by A5; ::_thesis: r < s thus r < s by A4; ::_thesis: verum 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 ) ) } ; hence not DEDEKIND_CUTS is empty by A2, ZFMISC_1:56; ::_thesis: verum end; end; definition func REAL+ -> set equals :: ARYTM_2:def 2 (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; coherence (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } is set ; end; :: deftheorem defines REAL+ ARYTM_2:def_2_:_ REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; set IR = { 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 ) ) } ; set RA = { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; Lm1: for x, y being set holds not [x,y] 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 ) ) } proof given x, y being set such that A1: [x,y] 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 ) ) } ; ::_thesis: contradiction consider A being Subset of RAT+ such that A2: [x,y] = A and A3: 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 ) ) by A1; ( {x} in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds s in A ) ) by A2, A3, TARSKI:def_2; then consider r1, r2, r3 being Element of RAT+ such that A4: r1 in A and A5: r2 in A and A6: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75; A7: ( r2 = {x,y} or r2 = {x} ) by A2, A5, TARSKI:def_2; ( r1 = {x,y} or r1 = {x} ) by A2, A4, TARSKI:def_2; hence contradiction by A2, A6, A7, TARSKI:def_2; ::_thesis: verum end; Lm2: RAT+ misses { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } proof assume RAT+ meets { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction then consider e being set such that A1: e in RAT+ and A2: e in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:3; consider t being Element of RAT+ such that A3: e = { s where s is Element of RAT+ : s < t } and A4: t <> {} by A2; {} <=' t by ARYTM_3:64; then {} < t by A4, ARYTM_3:68; then A5: {} in e by A3; e c= RAT+ proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in e or u in RAT+ ) assume u in e ; ::_thesis: u in RAT+ then ex s being Element of RAT+ st ( s = u & s < t ) by A3; hence u in RAT+ ; ::_thesis: verum end; then reconsider e = e as non empty Subset of RAT+ by A5; consider s being Element of RAT+ such that A6: s in e and A7: for r being Element of RAT+ st r in e holds r <=' s by A1, ARYTM_3:91; ex r being Element of RAT+ st ( r = s & r < t ) by A3, A6; then consider r being Element of RAT+ such that A8: s < r and A9: r < t by ARYTM_3:93; r in e by A3, A9; hence contradiction by A7, A8; ::_thesis: verum end; theorem Th1: :: ARYTM_2:1 RAT+ c= REAL+ by Lm2, XBOOLE_1:7, XBOOLE_1:86; RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { 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 ) ) } by XBOOLE_1:9; then Lm3: REAL+ c= RAT+ \/ { 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 ) ) } by XBOOLE_1:1; REAL+ = RAT+ \/ (( { 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 ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ) by Lm2, XBOOLE_1:87; then Lm4: DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } c= REAL+ by XBOOLE_1:7; Lm5: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega by XBOOLE_1:7; theorem :: ARYTM_2:2 omega c= REAL+ by Lm5, Th1, XBOOLE_1:1; registration cluster REAL+ -> non empty ; coherence not REAL+ is empty by Th1; end; definition let x be Element of REAL+ ; func DEDEKIND_CUT x -> Element of DEDEKIND_CUTS means :Def3: :: ARYTM_2:def 3 ex r being Element of RAT+ st ( x = r & it = { s where s is Element of RAT+ : s < r } ) if x in RAT+ otherwise it = x; existence ( ( x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS ex r being Element of RAT+ st ( x = r & b1 = { s where s is Element of RAT+ : s < r } ) ) & ( not x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS st b1 = x ) ) proof thus ( x in RAT+ implies ex IT being Element of DEDEKIND_CUTS ex r being Element of RAT+ st ( x = r & IT = { s where s is Element of RAT+ : s < r } ) ) ::_thesis: ( not x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS st b1 = x ) proof assume x in RAT+ ; ::_thesis: ex IT being Element of DEDEKIND_CUTS ex r being Element of RAT+ st ( x = r & IT = { s where s is Element of RAT+ : s < r } ) then reconsider r = x as Element of RAT+ ; set IT = { s where s is Element of RAT+ : s < r } ; A1: { s where s is Element of RAT+ : s < r } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r } or e in RAT+ ) assume e in { s where s is Element of RAT+ : s < r } ; ::_thesis: e in RAT+ then ex s being Element of RAT+ st ( s = e & s < r ) ; hence e in RAT+ ; ::_thesis: verum end; for s being Element of RAT+ holds ( not s = r or not s < r ) ; then not r in { s where s is Element of RAT+ : s < r } ; then A2: { s where s is Element of RAT+ : s < r } <> RAT+ ; reconsider IT = { s where s is Element of RAT+ : s < r } as Subset of RAT+ by A1; for t being Element of RAT+ st t in IT holds ( ( for s being Element of RAT+ st s <=' t holds s in IT ) & ex s being Element of RAT+ st ( s in IT & t < s ) ) proof let t be Element of RAT+ ; ::_thesis: ( t in IT implies ( ( for s being Element of RAT+ st s <=' t holds s in IT ) & ex s being Element of RAT+ st ( s in IT & t < s ) ) ) assume t in IT ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds s in IT ) & ex s being Element of RAT+ st ( s in IT & t < s ) ) then A3: ex s being Element of RAT+ st ( t = s & s < r ) ; then consider s0 being Element of RAT+ such that A4: t < s0 and A5: s0 < r by ARYTM_3:93; thus for s being Element of RAT+ st s <=' t holds s in IT ::_thesis: ex s being Element of RAT+ st ( s in IT & t < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in IT ) assume s <=' t ; ::_thesis: s in IT then s < r by A3, ARYTM_3:69; hence s in IT ; ::_thesis: verum end; take s0 ; ::_thesis: ( s0 in IT & t < s0 ) thus s0 in IT by A5; ::_thesis: t < s0 thus t < s0 by A4; ::_thesis: verum end; then IT 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 ) ) } ; then reconsider IT = IT as Element of DEDEKIND_CUTS by A2, ZFMISC_1:56; take IT ; ::_thesis: ex r being Element of RAT+ st ( x = r & IT = { s where s is Element of RAT+ : s < r } ) take r ; ::_thesis: ( x = r & IT = { s where s is Element of RAT+ : s < r } ) thus ( x = r & IT = { s where s is Element of RAT+ : s < r } ) ; ::_thesis: verum end; A6: x in REAL+ ; assume not x in RAT+ ; ::_thesis: ex b1 being Element of DEDEKIND_CUTS st b1 = x then x in DEDEKIND_CUTS by A6, XBOOLE_0:def_3; hence ex b1 being Element of DEDEKIND_CUTS st b1 = x ; ::_thesis: verum end; uniqueness for b1, b2 being Element of DEDEKIND_CUTS holds ( ( x in RAT+ & ex r being Element of RAT+ st ( x = r & b1 = { s where s is Element of RAT+ : s < r } ) & ex r being Element of RAT+ st ( x = r & b2 = { s where s is Element of RAT+ : s < r } ) implies b1 = b2 ) & ( not x in RAT+ & b1 = x & b2 = x implies b1 = b2 ) ) ; consistency for b1 being Element of DEDEKIND_CUTS holds verum ; end; :: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def_3_:_ for x being Element of REAL+ for b2 being Element of DEDEKIND_CUTS holds ( ( x in RAT+ implies ( b2 = DEDEKIND_CUT x iff ex r being Element of RAT+ st ( x = r & b2 = { s where s is Element of RAT+ : s < r } ) ) ) & ( not x in RAT+ implies ( b2 = DEDEKIND_CUT x iff b2 = x ) ) ); theorem :: ARYTM_2:3 for y being set holds not [{},y] in REAL+ proof given y being set such that A1: [{},y] in REAL+ ; ::_thesis: contradiction percases ( [{},y] in RAT+ or [{},y] 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 ) ) } ) by A1, Lm3, XBOOLE_0:def_3; suppose [{},y] in RAT+ ; ::_thesis: contradiction hence contradiction by ARYTM_3:61; ::_thesis: verum end; suppose [{},y] 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 ) ) } ; ::_thesis: contradiction hence contradiction by Lm1; ::_thesis: verum end; end; end; Lm6: for s, t being Element of RAT+ st ( for r being Element of RAT+ holds ( r < s iff r < t ) ) holds s = t proof let s, t be Element of RAT+ ; ::_thesis: ( ( for r being Element of RAT+ holds ( r < s iff r < t ) ) implies s = t ) assume A1: for r being Element of RAT+ holds ( r < s iff r < t ) ; ::_thesis: s = t s <=' s ; then A2: t <=' s by A1; t <=' t ; then s <=' t by A1; hence s = t by A2, ARYTM_3:66; ::_thesis: verum end; definition let x be Element of DEDEKIND_CUTS ; func GLUED x -> Element of REAL+ means :Def4: :: ARYTM_2:def 4 ex r being Element of RAT+ st ( it = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) if ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) otherwise it = x; uniqueness for b1, b2 being Element of REAL+ holds ( ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) & ex r being Element of RAT+ st ( b1 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) & ex r being Element of RAT+ st ( b2 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) implies b1 = b2 ) & ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & b1 = x & b2 = x implies b1 = b2 ) ) proof let IT1, IT2 be Element of REAL+ ; ::_thesis: ( ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) & ex r being Element of RAT+ st ( IT1 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) & ex r being Element of RAT+ st ( IT2 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) implies IT1 = IT2 ) & ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) ) hereby ::_thesis: ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) assume ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) ; ::_thesis: ( ex r1 being Element of RAT+ st ( IT1 = r1 & ( for s being Element of RAT+ holds ( s in x iff s < r1 ) ) ) & ex r2 being Element of RAT+ st ( IT2 = r2 & ( for s being Element of RAT+ holds ( s in x iff s < r2 ) ) ) implies IT1 = IT2 ) given r1 being Element of RAT+ such that A1: IT1 = r1 and A2: for s being Element of RAT+ holds ( s in x iff s < r1 ) ; ::_thesis: ( ex r2 being Element of RAT+ st ( IT2 = r2 & ( for s being Element of RAT+ holds ( s in x iff s < r2 ) ) ) implies IT1 = IT2 ) given r2 being Element of RAT+ such that A3: IT2 = r2 and A4: for s being Element of RAT+ holds ( s in x iff s < r2 ) ; ::_thesis: IT1 = IT2 for s being Element of RAT+ holds ( s < r1 iff s < r2 ) proof let s be Element of RAT+ ; ::_thesis: ( s < r1 iff s < r2 ) ( s in x iff s < r1 ) by A2; hence ( s < r1 iff s < r2 ) by A4; ::_thesis: verum end; hence IT1 = IT2 by A1, A3, Lm6; ::_thesis: verum end; thus ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) ; ::_thesis: verum end; existence ( ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) implies ex b1 being Element of REAL+ ex r being Element of RAT+ st ( b1 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) ) & ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) implies ex b1 being Element of REAL+ st b1 = x ) ) proof hereby ::_thesis: ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) implies ex b1 being Element of REAL+ st b1 = x ) given r being Element of RAT+ such that A5: for s being Element of RAT+ holds ( s in x iff s < r ) ; ::_thesis: ex y being Element of REAL+ ex r being Element of RAT+ st ( y = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) r in RAT+ ; then reconsider y = r as Element of REAL+ by Th1; take y = y; ::_thesis: ex r being Element of RAT+ st ( y = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) take r = r; ::_thesis: ( y = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) thus y = r ; ::_thesis: for s being Element of RAT+ holds ( s in x iff s < r ) thus for s being Element of RAT+ holds ( s in x iff s < r ) by A5; ::_thesis: verum end; assume A6: for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ; ::_thesis: ex b1 being Element of REAL+ st b1 = x now__::_thesis:_not_x_in__{___{__s_where_s_is_Element_of_RAT+_:_s_<_t__}__where_t_is_Element_of_RAT+_:_t_<>_{}__}_ assume x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction then consider t being Element of RAT+ such that A7: x = { s where s is Element of RAT+ : s < t } and t <> {} ; for s being Element of RAT+ holds ( s in x iff s < t ) proof let s be Element of RAT+ ; ::_thesis: ( s in x iff s < t ) hereby ::_thesis: ( s < t implies s in x ) assume s in x ; ::_thesis: s < t then ex r being Element of RAT+ st ( s = r & r < t ) by A7; hence s < t ; ::_thesis: verum end; thus ( s < t implies s in x ) by A7; ::_thesis: verum end; hence contradiction by A6; ::_thesis: verum end; then x in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:def_5; then reconsider y = x as Element of REAL+ by Lm4; take y ; ::_thesis: y = x thus y = x ; ::_thesis: verum end; consistency for b1 being Element of REAL+ holds verum ; end; :: deftheorem Def4 defines GLUED ARYTM_2:def_4_:_ for x being Element of DEDEKIND_CUTS for b2 being Element of REAL+ holds ( ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in x iff s < r ) implies ( b2 = GLUED x iff ex r being Element of RAT+ st ( b2 = r & ( for s being Element of RAT+ holds ( s in x iff s < r ) ) ) ) ) & ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) implies ( b2 = GLUED x iff b2 = x ) ) ); Lm7: for r being Element of RAT+ for B being set st B in DEDEKIND_CUTS & r in B holds ex s being Element of RAT+ st ( s in B & r < s ) proof let r be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS & r in B holds ex s being Element of RAT+ st ( s in B & r < s ) let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & r in B implies ex s being Element of RAT+ st ( s in B & r < s ) ) assume B in DEDEKIND_CUTS ; ::_thesis: ( not r in B or ex s being Element of RAT+ st ( s in B & r < s ) ) then B 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 ) ) } ; then ex A being Subset of RAT+ st ( B = A & ( for t being Element of RAT+ st t in A holds ( ( for s being Element of RAT+ st s <=' t holds s in A ) & ex s being Element of RAT+ st ( s in A & t < s ) ) ) ) ; hence ( not r in B or ex s being Element of RAT+ st ( s in B & r < s ) ) ; ::_thesis: verum end; Lm8: {} in DEDEKIND_CUTS proof reconsider B = {} as Subset of RAT+ by XBOOLE_1:2; for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; then {} 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 ) ) } ; hence {} in DEDEKIND_CUTS by ZFMISC_1:56; ::_thesis: verum end; Lm9: DEDEKIND_CUTS /\ RAT+ = {{}} proof now__::_thesis:_for_e_being_set_holds_ (_(_e_in_DEDEKIND_CUTS_/\_RAT+_implies_e_=_{}_)_&_(_e_=_{}_implies_e_in_DEDEKIND_CUTS_/\_RAT+_)_) let e be set ; ::_thesis: ( ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) & ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) ) thus ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) ::_thesis: ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) proof assume that A1: e in DEDEKIND_CUTS /\ RAT+ and A2: e <> {} ; ::_thesis: contradiction reconsider A = e as non empty Subset of RAT+ by A1, A2; A in RAT+ by A1, XBOOLE_0:def_4; then A3: ex s being Element of RAT+ st ( s in A & ( for r being Element of RAT+ st r in A holds r <=' s ) ) by ARYTM_3:91; e in DEDEKIND_CUTS by A1, XBOOLE_0:def_4; hence contradiction by A3, Lm7; ::_thesis: verum end; thus ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) by Lm8, XBOOLE_0:def_4; ::_thesis: verum end; hence DEDEKIND_CUTS /\ RAT+ = {{}} by TARSKI:def_1; ::_thesis: verum end; Lm10: for x being Element of REAL+ holds ( DEDEKIND_CUT x = {} iff x = {} ) proof let x be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x = {} iff x = {} ) A1: for e being set holds not e in { s where s is Element of RAT+ : s < {} } proof given e being set such that A2: e in { s where s is Element of RAT+ : s < {} } ; ::_thesis: contradiction ex s being Element of RAT+ st ( s = e & s < {} ) by A2; hence contradiction by ARYTM_3:64; ::_thesis: verum end; thus ( DEDEKIND_CUT x = {} implies x = {} ) ::_thesis: ( x = {} implies DEDEKIND_CUT x = {} ) proof assume A3: DEDEKIND_CUT x = {} ; ::_thesis: x = {} percases ( x in RAT+ or not x in RAT+ ) ; supposeA4: x in RAT+ ; ::_thesis: x = {} assume A5: x <> {} ; ::_thesis: contradiction consider r being Element of RAT+ such that A6: x = r and A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } by A4, Def3; {} <=' r by ARYTM_3:64; then {} < r by A6, A5, ARYTM_3:68; then {} in DEDEKIND_CUT x by A7; hence contradiction by A3; ::_thesis: verum end; suppose not x in RAT+ ; ::_thesis: x = {} hence x = {} by A3, Def3; ::_thesis: verum end; end; end; assume x = {} ; ::_thesis: DEDEKIND_CUT x = {} then ex r being Element of RAT+ st ( {} = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3; hence DEDEKIND_CUT x = {} by A1, XBOOLE_0:def_1; ::_thesis: verum end; Lm11: for A being Element of DEDEKIND_CUTS holds ( GLUED A = {} iff A = {} ) proof let A be Element of DEDEKIND_CUTS ; ::_thesis: ( GLUED A = {} iff A = {} ) thus ( GLUED A = {} implies A = {} ) ::_thesis: ( A = {} implies GLUED A = {} ) proof assume A1: GLUED A = {} ; ::_thesis: A = {} percases ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in A iff s < r ) or for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in A iff s < r ) ) ; supposeA2: ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in A iff s < r ) ; ::_thesis: A = {} assume A <> {} ; ::_thesis: contradiction then consider r being Element of RAT+ such that A3: r in A by SUBSET_1:4; ex r being Element of RAT+ st ( GLUED A = r & ( for s being Element of RAT+ holds ( s in A iff s < r ) ) ) by A2, Def4; then r < {} by A1, A3; hence contradiction by ARYTM_3:64; ::_thesis: verum end; suppose for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in A iff s < r ) ; ::_thesis: A = {} hence A = {} by A1, Def4; ::_thesis: verum end; end; end; assume A4: A = {} ; ::_thesis: GLUED A = {} then for s being Element of RAT+ holds ( s in A iff s < {} ) by ARYTM_3:64; then consider r being Element of RAT+ such that A5: GLUED A = r and A6: for s being Element of RAT+ holds ( s in A iff s < r ) by Def4; assume A7: GLUED A <> {} ; ::_thesis: contradiction {} <=' r by ARYTM_3:64; then {} < r by A5, A7, ARYTM_3:68; hence contradiction by A4, A6; ::_thesis: verum end; Lm12: for A being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED A) = A proof let A be Element of DEDEKIND_CUTS ; ::_thesis: DEDEKIND_CUT (GLUED A) = A percases ( ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in A iff s < r ) or A = {} or ( A <> {} & ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in A iff s < r ) ) ) ) ; suppose ex r being Element of RAT+ st for s being Element of RAT+ holds ( s in A iff s < r ) ; ::_thesis: DEDEKIND_CUT (GLUED A) = A then consider r being Element of RAT+ such that A1: r = GLUED A and A2: for s being Element of RAT+ holds ( s in A iff s < r ) by Def4; consider s being Element of RAT+ such that A3: r = s and A4: DEDEKIND_CUT (GLUED A) = { t where t is Element of RAT+ : t < s } by A1, Def3; thus DEDEKIND_CUT (GLUED A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= DEDEKIND_CUT (GLUED A) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in DEDEKIND_CUT (GLUED A) or e in A ) assume e in DEDEKIND_CUT (GLUED A) ; ::_thesis: e in A then ex t being Element of RAT+ st ( t = e & t < s ) by A4; hence e in A by A2, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in DEDEKIND_CUT (GLUED A) ) assume A5: e in A ; ::_thesis: e in DEDEKIND_CUT (GLUED A) then reconsider s = e as Element of RAT+ ; s < r by A2, A5; hence e in DEDEKIND_CUT (GLUED A) by A3, A4; ::_thesis: verum end; supposeA6: A = {} ; ::_thesis: DEDEKIND_CUT (GLUED A) = A then GLUED A = {} by Lm11; hence DEDEKIND_CUT (GLUED A) = A by A6, Lm10; ::_thesis: verum end; supposethat A7: A <> {} and A8: for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in A iff s < r ) ; ::_thesis: DEDEKIND_CUT (GLUED A) = A A9: GLUED A = A by A8, Def4; now__::_thesis:_not_GLUED_A_in_RAT+ assume GLUED A in RAT+ ; ::_thesis: contradiction then GLUED A in RAT+ /\ DEDEKIND_CUTS by A9, XBOOLE_0:def_4; then GLUED A = {} by Lm9, TARSKI:def_1; hence contradiction by A7, Lm11; ::_thesis: verum end; hence DEDEKIND_CUT (GLUED A) = A by A9, Def3; ::_thesis: verum end; end; end; Lm13: for x, y being set st 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 ) ) } & y 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 c= y holds y c= x proof let x, y be set ; ::_thesis: ( 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 ) ) } & y 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 c= y implies y c= x ) assume 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 ) ) } ; ::_thesis: ( not y 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 ) ) } or x c= y or y c= x ) then A1: ex A9 being Subset of RAT+ st ( x = A9 & ( for r being Element of RAT+ st r in A9 holds ( ( for s being Element of RAT+ st s <=' r holds s in A9 ) & ex s being Element of RAT+ st ( s in A9 & r < s ) ) ) ) ; assume y 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 ) ) } ; ::_thesis: ( x c= y or y c= x ) then A2: ex B9 being Subset of RAT+ st ( y = B9 & ( for r being Element of RAT+ st r in B9 holds ( ( for s being Element of RAT+ st s <=' r holds s in B9 ) & ex s being Element of RAT+ st ( s in B9 & r < s ) ) ) ) ; assume not x c= y ; ::_thesis: y c= x then consider s being set such that A3: s in x and A4: not s in y by TARSKI:def_3; reconsider s = s as Element of RAT+ by A1, A3; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in x ) assume A5: e in y ; ::_thesis: e in x then reconsider r = e as Element of RAT+ by A2; r <=' s by A2, A4, A5; hence e in x by A1, A3; ::_thesis: verum end; definition let x, y be Element of REAL+ ; predx <=' y means :Def5: :: ARYTM_2:def 5 ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x9 <=' y9 ) if ( x in RAT+ & y in RAT+ ) x in y if ( x in RAT+ & not y in RAT+ ) not y in x if ( not x in RAT+ & y in RAT+ ) otherwise x c= y; consistency ( ( x in RAT+ & y in RAT+ & x in RAT+ & not y in RAT+ implies ( ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x9 <=' y9 ) iff x in y ) ) & ( x in RAT+ & y in RAT+ & not x in RAT+ & y in RAT+ implies ( ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x9 <=' y9 ) iff not y in x ) ) & ( x in RAT+ & not y in RAT+ & not x in RAT+ & y in RAT+ implies ( x in y iff not y in x ) ) ) ; connectedness for x, y being Element of REAL+ st ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds ( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) holds ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st ( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) proof let x, y be Element of REAL+ ; ::_thesis: ( ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds ( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) implies ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st ( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) ) assume A1: ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds ( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( not ( x in RAT+ & y in RAT+ ) & not ( x in RAT+ & not y in RAT+ ) & not ( not x in RAT+ & y in RAT+ ) & not x c= y ) ) ; ::_thesis: ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st ( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) thus ( y in RAT+ & x in RAT+ implies ex y9, x9 being Element of RAT+ st ( y = y9 & x = x9 & y9 <=' x9 ) ) ::_thesis: ( ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) proof assume ( y in RAT+ & x in RAT+ ) ; ::_thesis: ex y9, x9 being Element of RAT+ st ( y = y9 & x = x9 & y9 <=' x9 ) then reconsider y9 = y, x9 = x as Element of RAT+ ; y9 <=' x9 by A1; hence ex y9, x9 being Element of RAT+ st ( y = y9 & x = x9 & y9 <=' x9 ) ; ::_thesis: verum end; thus ( y in RAT+ & not x in RAT+ implies y in x ) by A1; ::_thesis: ( ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) thus ( not y in RAT+ & x in RAT+ implies not x in y ) by A1; ::_thesis: ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) assume A2: ( not ( y in RAT+ & x in RAT+ ) & not ( y in RAT+ & not x in RAT+ ) & not ( not y in RAT+ & x in RAT+ ) ) ; ::_thesis: y c= x y in REAL+ ; then A3: y 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 ) ) } by A2, Lm3, XBOOLE_0:def_3; x in REAL+ ; 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 ) ) } by A2, Lm3, XBOOLE_0:def_3; hence y c= x by A1, A2, A3, Lm13; ::_thesis: verum end; end; :: deftheorem Def5 defines <=' ARYTM_2:def_5_:_ for x, y being Element of REAL+ holds ( ( x in RAT+ & y in RAT+ implies ( x <=' y iff ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in RAT+ & not y in RAT+ implies ( x <=' y iff x in y ) ) & ( not x in RAT+ & y in RAT+ implies ( x <=' y iff not y in x ) ) & ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) implies ( x <=' y iff x c= y ) ) ); notation let x, y be Element of REAL+ ; antonym y < x for x <=' y; end; Lm14: for x9, y9 being Element of RAT+ for x, y being Element of REAL+ st x = x9 & y = y9 holds ( x <=' y iff x9 <=' y9 ) proof let x9, y9 be Element of RAT+ ; ::_thesis: for x, y being Element of REAL+ st x = x9 & y = y9 holds ( x <=' y iff x9 <=' y9 ) let x, y be Element of REAL+ ; ::_thesis: ( x = x9 & y = y9 implies ( x <=' y iff x9 <=' y9 ) ) assume A1: ( x = x9 & y = y9 ) ; ::_thesis: ( x <=' y iff x9 <=' y9 ) hereby ::_thesis: ( x9 <=' y9 implies x <=' y ) assume x <=' y ; ::_thesis: x9 <=' y9 then ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x9 <=' y9 ) by A1, Def5; hence x9 <=' y9 by A1; ::_thesis: verum end; thus ( x9 <=' y9 implies x <=' y ) by A1, Def5; ::_thesis: verum end; Lm15: for B being set st B in DEDEKIND_CUTS & B <> {} holds ex r being Element of RAT+ st ( r in B & r <> {} ) proof let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & B <> {} implies ex r being Element of RAT+ st ( r in B & r <> {} ) ) assume that A1: B in DEDEKIND_CUTS and A2: B <> {} ; ::_thesis: ex r being Element of RAT+ st ( r in B & r <> {} ) B 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 ) ) } by A1; then consider A being Subset of RAT+ such that A3: B = A and A4: 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 ) ) ; reconsider A = A as non empty Subset of RAT+ by A2, A3; consider r0 being Element of RAT+ such that A5: r0 in A by SUBSET_1:4; consider r1 being Element of RAT+ such that A6: r1 in A and A7: r0 < r1 by A4, A5; A8: ( r1 <> {} or r0 <> {} ) by A7; for r, s being Element of RAT+ st r in A & s <=' r holds s in A by A4; then consider r1, r2, r3 being Element of RAT+ such that A9: ( r1 in A & r2 in A ) and r3 in A and A10: r1 <> r2 and r2 <> r3 and r3 <> r1 by A5, A6, A8, ARYTM_3:75; ( r1 <> {} or r2 <> {} ) by A10; hence ex r being Element of RAT+ st ( r in B & r <> {} ) by A3, A9; ::_thesis: verum end; Lm16: for r, s being Element of RAT+ for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds s in B proof let r, s be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds s in B let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & r in B & s <=' r implies s in B ) assume that A1: B in DEDEKIND_CUTS and A2: ( r in B & s <=' r ) ; ::_thesis: s in B B 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 ) ) } by A1; then ex A being Subset of RAT+ st ( B = A & ( for t being Element of RAT+ st t in A holds ( ( for s being Element of RAT+ st s <=' t holds s in A ) & ex s being Element of RAT+ st ( s in A & t < s ) ) ) ) ; hence s in B by A2; ::_thesis: verum end; Lm17: for B being set st B in DEDEKIND_CUTS & B <> {} holds {} in B proof let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & B <> {} implies {} in B ) assume that A1: B in DEDEKIND_CUTS and A2: B <> {} ; ::_thesis: {} in B reconsider B = B as non empty Subset of RAT+ by A1, A2; ex r being Element of RAT+ st r in B by SUBSET_1:4; hence {} in B by A1, Lm16, ARYTM_3:64; ::_thesis: verum end; Lm18: for r being Element of RAT+ for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds ex s being Element of RAT+ st ( not s in B & s < r ) proof let r be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds ex s being Element of RAT+ st ( not s in B & s < r ) let B be set ; ::_thesis: ( B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} implies ex s being Element of RAT+ st ( not s in B & s < r ) ) assume that A1: B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } and A2: not r in B and A3: B <> {} ; ::_thesis: ex s being Element of RAT+ st ( not s in B & s < r ) A4: B in DEDEKIND_CUTS by A1, XBOOLE_0:def_5; assume A5: for s being Element of RAT+ st not s in B holds not s < r ; ::_thesis: contradiction A6: B = { s where s is Element of RAT+ : s < r } proof thus B c= { s where s is Element of RAT+ : s < r } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < r } c= B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in { s where s is Element of RAT+ : s < r } ) assume A7: e in B ; ::_thesis: e in { s where s is Element of RAT+ : s < r } reconsider B = B as Element of DEDEKIND_CUTS by A1, XBOOLE_0:def_5; B c= RAT+ ; then reconsider t = e as Element of RAT+ by A7; not r <=' t by A2, A4, A7, Lm16; hence e in { s where s is Element of RAT+ : s < r } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r } or e in B ) assume e in { s where s is Element of RAT+ : s < r } ; ::_thesis: e in B then ex s being Element of RAT+ st ( s = e & s < r ) ; hence e in B by A5; ::_thesis: verum end; r <> {} by A2, A3, A4, Lm17; then B in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A6; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; Lm19: for x being Element of REAL+ st DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } holds x in RAT+ proof let x be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } implies x in RAT+ ) assume A1: DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: x in RAT+ assume not x in RAT+ ; ::_thesis: contradiction then DEDEKIND_CUT x = x by Def3; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; Lm20: for x, y being Element of REAL+ st DEDEKIND_CUT x c= DEDEKIND_CUT y holds x <=' y proof let x, y be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x c= DEDEKIND_CUT y implies x <=' y ) assume A1: DEDEKIND_CUT x c= DEDEKIND_CUT y ; ::_thesis: x <=' y percases ( ( x = {} & not y in RAT+ ) or y = {} or ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ & x <> {} ) or ( not x in RAT+ & y in RAT+ & y <> {} ) or ( not x in RAT+ & not y in RAT+ ) ) ; supposethat A2: x = {} and A3: not y in RAT+ ; ::_thesis: x <=' y ( DEDEKIND_CUT y = y & y <> {} ) by A3, Def3; then x in y by A2, Lm17; hence x <=' y by A2, A3, Def5; ::_thesis: verum end; supposeA4: y = {} ; ::_thesis: x <=' y then DEDEKIND_CUT y = {} by Lm10; then DEDEKIND_CUT x = {} by A1; then x = {} by Lm10; hence x <=' y by A4; ::_thesis: verum end; supposethat A5: x in RAT+ and A6: y in RAT+ ; ::_thesis: x <=' y consider ry being Element of RAT+ such that A7: y = ry and A8: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A6, Def3; consider rx being Element of RAT+ such that A9: x = rx and A10: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A5, Def3; assume y < x ; ::_thesis: contradiction then ry < rx by A9, A7, Lm14; then ry in DEDEKIND_CUT x by A10; then ry in DEDEKIND_CUT y by A1; then ex s being Element of RAT+ st ( s = ry & s < ry ) by A8; hence contradiction ; ::_thesis: verum end; supposethat A11: x in RAT+ and A12: not y in RAT+ and A13: x <> {} ; ::_thesis: x <=' y A14: DEDEKIND_CUT y = y by A12, Def3; consider rx being Element of RAT+ such that A15: x = rx and A16: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A11, Def3; DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A13, A15, A16; then DEDEKIND_CUT x <> y by A12, A14, Lm19; then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A14, XBOOLE_0:def_10; then consider r0 being Element of RAT+ such that A17: r0 in y and A18: not r0 in DEDEKIND_CUT x by A14, SUBSET_1:2; rx <=' r0 by A16, A18; then x in y by A15, A14, A17, Lm16; hence x <=' y by A11, A12, Def5; ::_thesis: verum end; supposethat A19: not x in RAT+ and A20: y in RAT+ and A21: y <> {} ; ::_thesis: x <=' y consider ry being Element of RAT+ such that A22: y = ry and A23: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A20, Def3; A24: DEDEKIND_CUT y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A21, A22, A23; A25: DEDEKIND_CUT x = x by A19, Def3; then not x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A19, Lm19; then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A24, A25, XBOOLE_0:def_10; then consider r0 being Element of RAT+ such that A26: r0 in DEDEKIND_CUT y and A27: not r0 in x by A25, SUBSET_1:2; ex s being Element of RAT+ st ( s = r0 & s < ry ) by A23, A26; then not y in x by A22, A25, A27, Lm16; hence x <=' y by A19, A20, Def5; ::_thesis: verum end; supposeA28: ( not x in RAT+ & not y in RAT+ ) ; ::_thesis: x <=' y ( x = DEDEKIND_CUT x & y = DEDEKIND_CUT y ) by A28, Def3; hence x <=' y by A1, A28, Def5; ::_thesis: verum end; end; end; Lm21: for x, y being Element of REAL+ st x <=' y & y <=' x holds x = y proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' x implies x = y ) assume that A1: x <=' y and A2: y <=' x ; ::_thesis: x = y percases ( ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ; suppose ( x in RAT+ & y in RAT+ ) ; ::_thesis: x = y then reconsider x9 = x, y9 = y as Element of RAT+ ; ( x9 <=' y9 & y9 <=' x9 ) by A1, A2, Lm14; hence x = y by ARYTM_3:66; ::_thesis: verum end; supposeA3: ( x in RAT+ & not y in RAT+ ) ; ::_thesis: x = y x in y by A1, A3, Def5; hence x = y by A2, A3, Def5; ::_thesis: verum end; supposeA4: ( not x in RAT+ & y in RAT+ ) ; ::_thesis: x = y y in x by A2, A4, Def5; hence x = y by A1, A4, Def5; ::_thesis: verum end; suppose ( not x in RAT+ & not y in RAT+ ) ; ::_thesis: x = y then ( x c= y & y c= x ) by A1, A2, Def5; hence x = y by XBOOLE_0:def_10; ::_thesis: verum end; end; end; Lm22: for x, y being Element of REAL+ st DEDEKIND_CUT x = DEDEKIND_CUT y holds x = y proof let x, y be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x = DEDEKIND_CUT y implies x = y ) assume DEDEKIND_CUT x = DEDEKIND_CUT y ; ::_thesis: x = y then ( x <=' y & y <=' x ) by Lm20; hence x = y by Lm21; ::_thesis: verum end; Lm23: for x being Element of REAL+ holds GLUED (DEDEKIND_CUT x) = x proof let x be Element of REAL+ ; ::_thesis: GLUED (DEDEKIND_CUT x) = x DEDEKIND_CUT (GLUED (DEDEKIND_CUT x)) = DEDEKIND_CUT x by Lm12; hence GLUED (DEDEKIND_CUT x) = x by Lm22; ::_thesis: verum end; definition let A, B be Element of DEDEKIND_CUTS ; funcA + B -> Element of DEDEKIND_CUTS equals :Def6: :: ARYTM_2:def 6 { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; coherence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS proof { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS proof set C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ; { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } or e in RAT+ ) assume e in { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ; ::_thesis: e in RAT+ then ex s, t being Element of RAT+ st ( e = s + t & s in A & t in B ) ; hence e in RAT+ ; ::_thesis: verum end; then reconsider C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } as Subset of RAT+ ; A <> RAT+ by ZFMISC_1:56; then consider a0 being Element of RAT+ such that A1: not a0 in A by SUBSET_1:28; for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) proof let r be Element of RAT+ ; ::_thesis: ( r in C implies ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ) assume r in C ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) then consider s0, t0 being Element of RAT+ such that A2: r = s0 + t0 and A3: s0 in A and A4: t0 in B ; thus for s being Element of RAT+ st s <=' r holds s in C ::_thesis: ex s being Element of RAT+ st ( s in C & r < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in C ) assume s <=' r ; ::_thesis: s in C then consider s1, t1 being Element of RAT+ such that A5: s = s1 + t1 and A6: ( s1 <=' s0 & t1 <=' t0 ) by A2, ARYTM_3:87; ( s1 in A & t1 in B ) by A3, A4, A6, Lm16; hence s in C by A5; ::_thesis: verum end; consider s1 being Element of RAT+ such that A7: s1 in A and A8: s0 < s1 by A3, Lm7; take t2 = s1 + t0; ::_thesis: ( t2 in C & r < t2 ) thus t2 in C by A4, A7; ::_thesis: r < t2 thus r < t2 by A2, A8, ARYTM_3:76; ::_thesis: verum end; then A9: C 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 ) ) } ; B <> RAT+ by ZFMISC_1:56; then consider b0 being Element of RAT+ such that A10: not b0 in B by SUBSET_1:28; now__::_thesis:_not_a0_+_b0_in_C assume a0 + b0 in C ; ::_thesis: contradiction then consider s, t being Element of RAT+ such that A11: a0 + b0 = s + t and A12: ( s in A & t in B ) ; ( a0 <=' s or b0 <=' t ) by A11, ARYTM_3:81; hence contradiction by A1, A10, A12, Lm16; ::_thesis: verum end; then C <> RAT+ ; hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS by A9, ZFMISC_1:56; ::_thesis: verum end; hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS ; ::_thesis: verum end; commutativity for b1, A, B being Element of DEDEKIND_CUTS st b1 = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds b1 = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } proof let IT, A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) set C = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; set D = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; A13: { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } c= { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ) assume e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; ::_thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } then ex r, s being Element of RAT+ st ( e = r + s & r in B & s in A ) ; hence e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: verum end; { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } c= { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) assume e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } then ex r, s being Element of RAT+ st ( e = r + s & r in A & s in B ) ; hence e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; ::_thesis: verum end; hence ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) by A13, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def6 defines + ARYTM_2:def_6_:_ for A, B being Element of DEDEKIND_CUTS holds A + B = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; Lm24: for B being set st B in DEDEKIND_CUTS holds ex r being Element of RAT+ st not r in B proof let B be set ; ::_thesis: ( B in DEDEKIND_CUTS implies ex r being Element of RAT+ st not r in B ) assume A1: B in DEDEKIND_CUTS ; ::_thesis: not for r being Element of RAT+ holds r in B then reconsider B = B as Subset of RAT+ ; B <> RAT+ by A1, ZFMISC_1:56; hence not for r being Element of RAT+ holds r in B by SUBSET_1:28; ::_thesis: verum end; definition let A, B be Element of DEDEKIND_CUTS ; funcA *' B -> Element of DEDEKIND_CUTS equals :: ARYTM_2:def 7 { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; coherence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS proof percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS for e being set holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } proof given e being set such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: contradiction ex r, s being Element of RAT+ st ( e = r *' s & r in A & s in B ) by A2; hence contradiction by A1; ::_thesis: verum end; hence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS by Lm8, XBOOLE_0:def_1; ::_thesis: verum end; supposeA3: A <> {} ; ::_thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS set C = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } or e in RAT+ ) assume e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: e in RAT+ then ex r, s being Element of RAT+ st ( r *' s = e & r in A & s in B ) ; hence e in RAT+ ; ::_thesis: verum end; then reconsider C = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } as Subset of RAT+ ; for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) proof let r be Element of RAT+ ; ::_thesis: ( r in C implies ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ) assume r in C ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) then consider r0, s0 being Element of RAT+ such that A4: r = r0 *' s0 and A5: r0 in A and A6: s0 in B ; thus for s being Element of RAT+ st s <=' r holds s in C ::_thesis: ex s being Element of RAT+ st ( s in C & r < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in C ) assume s <=' r ; ::_thesis: s in C then consider t0 being Element of RAT+ such that A7: s = r0 *' t0 and A8: t0 <=' s0 by A4, ARYTM_3:79; t0 in B by A6, A8, Lm16; hence s in C by A5, A7; ::_thesis: verum end; consider t0 being Element of RAT+ such that A9: t0 in B and A10: s0 < t0 by A6, Lm7; percases ( r0 = {} or r0 <> {} ) ; supposeA11: r0 = {} ; ::_thesis: ex s being Element of RAT+ st ( s in C & r < s ) consider r1 being Element of RAT+ such that A12: r1 in A and A13: r1 <> {} by A3, Lm15; take r1 *' t0 ; ::_thesis: ( r1 *' t0 in C & r < r1 *' t0 ) thus r1 *' t0 in C by A9, A12; ::_thesis: r < r1 *' t0 t0 <> {} by A10, ARYTM_3:64; then A14: r1 *' t0 <> {} by A13, ARYTM_3:78; A15: r = {} by A4, A11, ARYTM_3:48; then r <=' r1 *' t0 by ARYTM_3:64; hence r < r1 *' t0 by A15, A14, ARYTM_3:68; ::_thesis: verum end; supposeA16: r0 <> {} ; ::_thesis: ex s being Element of RAT+ st ( s in C & r < s ) s0 <> t0 by A10; then A17: r <> r0 *' t0 by A4, A16, ARYTM_3:56; take r0 *' t0 ; ::_thesis: ( r0 *' t0 in C & r < r0 *' t0 ) thus r0 *' t0 in C by A5, A9; ::_thesis: r < r0 *' t0 r <=' r0 *' t0 by A4, A10, ARYTM_3:82; hence r < r0 *' t0 by A17, ARYTM_3:68; ::_thesis: verum end; end; end; then A18: C 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 ) ) } ; consider r0 being Element of RAT+ such that A19: not r0 in A by Lm24; consider s0 being Element of RAT+ such that A20: not s0 in B by Lm24; now__::_thesis:_not_r0_*'_s0_in_C assume r0 *' s0 in C ; ::_thesis: contradiction then consider r1, s1 being Element of RAT+ such that A21: r0 *' s0 = r1 *' s1 and A22: ( r1 in A & s1 in B ) ; ( r0 <=' r1 or s0 <=' s1 ) by A21, ARYTM_3:83; hence contradiction by A19, A20, A22, Lm16; ::_thesis: verum end; then C <> RAT+ ; hence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS by A18, ZFMISC_1:56; ::_thesis: verum end; end; end; commutativity for b1, A, B being Element of DEDEKIND_CUTS st b1 = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds b1 = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } proof let D, A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) assume A23: D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } now__::_thesis:_for_e_being_set_holds_ (_e_in_D_iff_e_in__{__(r_*'_s)_where_r,_s_is_Element_of_RAT+_:_(_r_in_B_&_s_in_A_)__}__) let e be set ; ::_thesis: ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) ( e in D iff ex r, s being Element of RAT+ st ( e = r *' s & r in A & s in B ) ) by A23; then ( e in D iff ex r, s being Element of RAT+ st ( e = r *' s & r in B & s in A ) ) ; hence ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) ; ::_thesis: verum end; hence D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines *' ARYTM_2:def_7_:_ for A, B being Element of DEDEKIND_CUTS holds A *' B = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; definition let x, y be Element of REAL+ ; funcx + y -> Element of REAL+ equals :Def8: :: ARYTM_2:def 8 x if y = {} y if x = {} otherwise GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)); coherence ( ( y = {} implies x is Element of REAL+ ) & ( x = {} implies y is Element of REAL+ ) & ( not y = {} & not x = {} implies GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) is Element of REAL+ ) ) ; consistency for b1 being Element of REAL+ st y = {} & x = {} holds ( b1 = x iff b1 = y ) ; commutativity for b1, x, y being Element of REAL+ st ( y = {} implies b1 = x ) & ( x = {} implies b1 = y ) & ( not y = {} & not x = {} implies b1 = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) holds ( ( x = {} implies b1 = y ) & ( y = {} implies b1 = x ) & ( not x = {} & not y = {} implies b1 = GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT x)) ) ) ; funcx *' y -> Element of REAL+ equals :: ARYTM_2:def 9 GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)); coherence GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) is Element of REAL+ ; commutativity for b1, x, y being Element of REAL+ st b1 = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) holds b1 = GLUED ((DEDEKIND_CUT y) *' (DEDEKIND_CUT x)) ; end; :: deftheorem Def8 defines + ARYTM_2:def_8_:_ for x, y being Element of REAL+ holds ( ( y = {} implies x + y = x ) & ( x = {} implies x + y = y ) & ( not y = {} & not x = {} implies x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) ); :: deftheorem defines *' ARYTM_2:def_9_:_ for x, y being Element of REAL+ holds x *' y = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)); theorem Th4: :: ARYTM_2:4 for x, y being Element of REAL+ st x = {} holds x *' y = {} proof let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies x *' y = {} ) set A = DEDEKIND_CUT x; set B = DEDEKIND_CUT y; assume A1: x = {} ; ::_thesis: x *' y = {} for e being set holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } proof given e being set such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } ; ::_thesis: contradiction ex r, s being Element of RAT+ st ( e = r *' s & r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) by A2; hence contradiction by A1, Lm10; ::_thesis: verum end; then { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } = {} by XBOOLE_0:def_1; hence x *' y = {} by Lm11; ::_thesis: verum end; theorem Th5: :: ARYTM_2:5 for x, y being Element of REAL+ st x + y = {} holds x = {} proof let x, y be Element of REAL+ ; ::_thesis: ( x + y = {} implies x = {} ) assume A1: x + y = {} ; ::_thesis: x = {} percases ( y = {} or y <> {} ) ; suppose y = {} ; ::_thesis: x = {} hence x = {} by A1, Def8; ::_thesis: verum end; supposeA2: y <> {} ; ::_thesis: x = {} then DEDEKIND_CUT y <> {} by Lm10; then consider s0 being Element of RAT+ such that A3: s0 in DEDEKIND_CUT y by SUBSET_1:4; assume A4: x <> {} ; ::_thesis: contradiction then DEDEKIND_CUT x <> {} by Lm10; then consider r0 being Element of RAT+ such that A5: r0 in DEDEKIND_CUT x by SUBSET_1:4; A6: r0 + s0 in { (r + s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } by A5, A3; GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {} by A1, A2, A4, Def8; hence contradiction by A6, Lm11; ::_thesis: verum end; end; end; Lm25: for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) c= (A + B) + C proof let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A + (B + C) c= (A + B) + C let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A + (B + C) or e in (A + B) + C ) assume e in A + (B + C) ; ::_thesis: e in (A + B) + C then consider r0, s0 being Element of RAT+ such that A1: ( e = r0 + s0 & r0 in A ) and A2: s0 in B + C ; consider r1, s1 being Element of RAT+ such that A3: ( s0 = r1 + s1 & r1 in B ) and A4: s1 in C by A2; ( e = (r0 + r1) + s1 & r0 + r1 in A + B ) by A1, A3, ARYTM_3:51; hence e in (A + B) + C by A4; ::_thesis: verum end; Lm26: for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) = (A + B) + C proof let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A + (B + C) = (A + B) + C ( A + (B + C) c= (A + B) + C & (A + B) + C c= A + (B + C) ) by Lm25; hence A + (B + C) = (A + B) + C by XBOOLE_0:def_10; ::_thesis: verum end; Lm27: for A, B being Element of DEDEKIND_CUTS holds ( not A + B = {} or A = {} or B = {} ) proof let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( not A + B = {} or A = {} or B = {} ) assume A1: A + B = {} ; ::_thesis: ( A = {} or B = {} ) assume A <> {} ; ::_thesis: B = {} then consider r0 being Element of RAT+ such that A2: r0 in A by SUBSET_1:4; assume B <> {} ; ::_thesis: contradiction then consider s0 being Element of RAT+ such that A3: s0 in B by SUBSET_1:4; r0 + s0 in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } by A2, A3; hence contradiction by A1; ::_thesis: verum end; theorem Th6: :: ARYTM_2:6 for x, y, z being Element of REAL+ holds x + (y + z) = (x + y) + z proof let x, y, z be Element of REAL+ ; ::_thesis: x + (y + z) = (x + y) + z percases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ; supposeA1: x = {} ; ::_thesis: x + (y + z) = (x + y) + z hence x + (y + z) = y + z by Def8 .= (x + y) + z by A1, Def8 ; ::_thesis: verum end; supposeA2: y = {} ; ::_thesis: x + (y + z) = (x + y) + z hence x + (y + z) = x + z by Def8 .= (x + y) + z by A2, Def8 ; ::_thesis: verum end; supposeA3: z = {} ; ::_thesis: x + (y + z) = (x + y) + z hence x + (y + z) = x + y by Def8 .= (x + y) + z by A3, Def8 ; ::_thesis: verum end; supposethat A4: x <> {} and A5: y <> {} and A6: z <> {} ; ::_thesis: x + (y + z) = (x + y) + z A7: now__::_thesis:_not_GLUED_((DEDEKIND_CUT_y)_+_(DEDEKIND_CUT_z))_=_{} assume GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z)) = {} ; ::_thesis: contradiction then (DEDEKIND_CUT y) + (DEDEKIND_CUT z) = {} by Lm11; then ( DEDEKIND_CUT y = {} or DEDEKIND_CUT z = {} ) by Lm27; hence contradiction by A5, A6, Lm10; ::_thesis: verum end; A8: now__::_thesis:_not_GLUED_((DEDEKIND_CUT_x)_+_(DEDEKIND_CUT_y))_=_{} assume GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {} ; ::_thesis: contradiction then (DEDEKIND_CUT x) + (DEDEKIND_CUT y) = {} by Lm11; then ( DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} ) by Lm27; hence contradiction by A4, A5, Lm10; ::_thesis: verum end; thus x + (y + z) = x + (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by A5, A6, Def8 .= GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))))) by A4, A7, Def8 .= GLUED ((DEDEKIND_CUT x) + ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by Lm12 .= GLUED (((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) + (DEDEKIND_CUT z)) by Lm26 .= GLUED ((DEDEKIND_CUT (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)))) + (DEDEKIND_CUT z)) by Lm12 .= (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y))) + z by A6, A8, Def8 .= (x + y) + z by A4, A5, Def8 ; ::_thesis: verum end; end; end; theorem :: ARYTM_2:7 { 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 ) ) } is c=-linear proof set IR = { 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 ) ) } ; let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not 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 ) ) } or not y 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 ) ) } or x,y are_c=-comparable ) assume 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 ) ) } ; ::_thesis: ( not y 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 ) ) } or x,y are_c=-comparable ) then A1: ex A9 being Subset of RAT+ st ( x = A9 & ( for r being Element of RAT+ st r in A9 holds ( ( for s being Element of RAT+ st s <=' r holds s in A9 ) & ex s being Element of RAT+ st ( s in A9 & r < s ) ) ) ) ; assume y 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 ) ) } ; ::_thesis: x,y are_c=-comparable then A2: ex B9 being Subset of RAT+ st ( y = B9 & ( for r being Element of RAT+ st r in B9 holds ( ( for s being Element of RAT+ st s <=' r holds s in B9 ) & ex s being Element of RAT+ st ( s in B9 & r < s ) ) ) ) ; assume not x c= y ; :: according to XBOOLE_0:def_9 ::_thesis: y c= x then consider s being set such that A3: s in x and A4: not s in y by TARSKI:def_3; reconsider s = s as Element of RAT+ by A1, A3; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in x ) assume A5: e in y ; ::_thesis: e in x then reconsider r = e as Element of RAT+ by A2; r <=' s by A2, A4, A5; hence e in x by A1, A3; ::_thesis: verum end; Lm28: for e being set st e in REAL+ holds e <> RAT+ proof let e be set ; ::_thesis: ( e in REAL+ implies e <> RAT+ ) assume e in REAL+ ; ::_thesis: e <> RAT+ then ( e in RAT+ or e in DEDEKIND_CUTS ) by XBOOLE_0:def_3; hence e <> RAT+ by ZFMISC_1:56; ::_thesis: verum end; Lm29: for r, s being Element of RAT+ for B being set st B 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 ) ) } & r in B & s <=' r holds s in B proof let r, s be Element of RAT+ ; ::_thesis: for B being set st B 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 ) ) } & r in B & s <=' r holds s in B let B be set ; ::_thesis: ( B 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 ) ) } & r in B & s <=' r implies s in B ) assume that A1: B 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 ) ) } and A2: ( r in B & s <=' r ) ; ::_thesis: s in B ex A being Subset of RAT+ st ( B = A & ( for t being Element of RAT+ st t in A holds ( ( for s being Element of RAT+ st s <=' t holds s in A ) & ex s being Element of RAT+ st ( s in A & t < s ) ) ) ) by A1; hence s in B by A2; ::_thesis: verum end; Lm30: for y, x being Element of REAL+ st y < x holds ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) proof let y, x be Element of REAL+ ; ::_thesis: ( y < x implies ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) ) assume A1: y < x ; ::_thesis: ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) percases ( ( x in RAT+ & y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ; suppose ( x in RAT+ & y in RAT+ ) ; ::_thesis: ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) then reconsider x9 = x, y9 = y as Element of RAT+ ; y9 < x9 by A1, Lm14; then consider z9 being Element of RAT+ such that A2: ( y9 < z9 & z9 < x9 ) by ARYTM_3:93; z9 in RAT+ ; then reconsider z = z9 as Element of REAL+ by Th1; take z ; ::_thesis: ( z in RAT+ & z < x & y < z ) thus ( z in RAT+ & z < x & y < z ) by A2, Lm14; ::_thesis: verum end; supposethat A3: not x in RAT+ and A4: y in RAT+ ; ::_thesis: ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) reconsider y9 = y as Element of RAT+ by A4; x in REAL+ ; 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 ) ) } by A3, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A5: x = A and A6: 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 ) ) ; y9 in x by A1, A3, Def5; then consider s being Element of RAT+ such that A7: s in A and A8: y9 < s by A5, A6; s in RAT+ ; then reconsider z = s as Element of REAL+ by Th1; take z ; ::_thesis: ( z in RAT+ & z < x & y < z ) thus z in RAT+ ; ::_thesis: ( z < x & y < z ) thus z < x by A3, A5, A7, Def5; ::_thesis: y < z thus y < z by A8, Lm14; ::_thesis: verum end; supposethat A9: x in RAT+ and A10: not y in RAT+ ; ::_thesis: ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) reconsider x9 = x as Element of RAT+ by A9; A11: not x9 in y by A1, A10, Def5; y in REAL+ ; then y 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 ) ) } by A10, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A12: y = B and A13: for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; B <> {} by A10, A12; then consider y1 being Element of RAT+ such that A14: y1 in B by SUBSET_1:4; {} <=' y1 by ARYTM_3:64; then A15: x9 <> {} by A12, A13, A11, A14; ex z9 being Element of RAT+ st ( z9 < x9 & not z9 in y ) proof set C = { s where s is Element of RAT+ : s < x9 } ; assume A16: for z9 being Element of RAT+ holds ( not z9 < x9 or z9 in y ) ; ::_thesis: contradiction y = { s where s is Element of RAT+ : s < x9 } proof thus y c= { s where s is Element of RAT+ : s < x9 } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < x9 } c= y proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in { s where s is Element of RAT+ : s < x9 } ) assume A17: e in y ; ::_thesis: e in { s where s is Element of RAT+ : s < x9 } then reconsider z9 = e as Element of RAT+ by A12; not x9 <=' z9 by A12, A13, A11, A17; hence e in { s where s is Element of RAT+ : s < x9 } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < x9 } or e in y ) assume e in { s where s is Element of RAT+ : s < x9 } ; ::_thesis: e in y then ex s being Element of RAT+ st ( e = s & s < x9 ) ; hence e in y by A16; ::_thesis: verum end; then y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then consider z9 being Element of RAT+ such that A18: z9 < x9 and A19: not z9 in y ; z9 in RAT+ ; then reconsider z = z9 as Element of REAL+ by Th1; take z ; ::_thesis: ( z in RAT+ & z < x & y < z ) thus z in RAT+ ; ::_thesis: ( z < x & y < z ) thus z < x by A18, Lm14; ::_thesis: y < z thus y < z by A10, A19, Def5; ::_thesis: verum end; supposethat A20: not x in RAT+ and A21: not y in RAT+ ; ::_thesis: ex z being Element of REAL+ st ( z in RAT+ & z < x & y < z ) y in REAL+ ; then y 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 ) ) } by A21, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A22: y = B and for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; x in REAL+ ; 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 ) ) } by A20, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A23: x = A and 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 c= y by A1, A20, A21, Def5; then consider z9 being Element of RAT+ such that A24: z9 in A and A25: not z9 in B by A23, A22, SUBSET_1:2; z9 in RAT+ ; then reconsider z = z9 as Element of REAL+ by Th1; take z ; ::_thesis: ( z in RAT+ & z < x & y < z ) thus z in RAT+ ; ::_thesis: ( z < x & y < z ) thus z < x by A20, A23, A24, Def5; ::_thesis: y < z thus y < z by A21, A22, A25, Def5; ::_thesis: verum end; end; end; Lm31: for x, y, z being Element of REAL+ st x <=' y & y <=' z holds x <=' z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' z implies x <=' z ) assume that A1: x <=' y and A2: y <=' z ; ::_thesis: x <=' z percases ( ( x in RAT+ & y in RAT+ & z in RAT+ ) or ( x in RAT+ & y in RAT+ & not z in RAT+ ) or ( x in RAT+ & not y in RAT+ & z in RAT+ ) or ( x in RAT+ & not y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & y in RAT+ & z in RAT+ ) or ( not x in RAT+ & y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & not z in RAT+ ) ) ; supposethat A3: x in RAT+ and A4: y in RAT+ and A5: z in RAT+ ; ::_thesis: x <=' z reconsider z9 = z as Element of RAT+ by A5; reconsider y9 = y as Element of RAT+ by A4; reconsider x9 = x as Element of RAT+ by A3; ( x9 <=' y9 & y9 <=' z9 ) by A1, A2, Lm14; then x9 <=' z9 by ARYTM_3:67; hence x <=' z by Lm14; ::_thesis: verum end; supposethat A6: x in RAT+ and A7: y in RAT+ and A8: not z in RAT+ ; ::_thesis: x <=' z reconsider y9 = y as Element of RAT+ by A7; reconsider x9 = x as Element of RAT+ by A6; A9: x9 <=' y9 by A1, Lm14; z in REAL+ ; then z 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 ) ) } by A8, Lm3, XBOOLE_0:def_3; then consider C being Subset of RAT+ such that A10: z = C and A11: for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ; y in C by A2, A7, A8, A10, Def5; then x9 in C by A11, A9; hence x <=' z by A8, A10, Def5; ::_thesis: verum end; supposethat A12: x in RAT+ and A13: not y in RAT+ and A14: z in RAT+ ; ::_thesis: x <=' z reconsider z9 = z as Element of RAT+ by A14; reconsider x9 = x as Element of RAT+ by A12; y in REAL+ ; then y 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 ) ) } by A13, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A15: y = B and A16: for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; ( x9 in B & not z9 in B ) by A1, A2, A13, A15, Def5; then x9 <=' z9 by A16; hence x <=' z by Lm14; ::_thesis: verum end; supposethat A17: x in RAT+ and A18: not y in RAT+ and A19: not z in RAT+ ; ::_thesis: x <=' z reconsider x9 = x as Element of RAT+ by A17; y in REAL+ ; then y 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 ) ) } by A18, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A20: y = B and for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; A21: x9 in B by A1, A18, A20, Def5; z in REAL+ ; then z 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 ) ) } by A19, Lm3, XBOOLE_0:def_3; then consider C being Subset of RAT+ such that A22: z = C and for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ; B c= C by A2, A18, A19, A20, A22, Def5; hence x <=' z by A19, A22, A21, Def5; ::_thesis: verum end; supposethat A23: not x in RAT+ and A24: y in RAT+ and A25: z in RAT+ ; ::_thesis: x <=' z reconsider z9 = z as Element of RAT+ by A25; reconsider y9 = y as Element of RAT+ by A24; A26: y9 <=' z9 by A2, Lm14; x in REAL+ ; 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 ) ) } by A23, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A27: x = A and A28: 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 y9 in A by A1, A23, A27, Def5; then not z9 in A by A28, A26; hence x <=' z by A23, A27, Def5; ::_thesis: verum end; supposethat A29: not x in RAT+ and A30: y in RAT+ and A31: not z in RAT+ ; ::_thesis: x <=' z x in REAL+ ; 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 ) ) } by A29, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A32: x = A and A33: 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 ) ) ; A34: not y in A by A1, A29, A32, Def5; reconsider y9 = y as Element of RAT+ by A30; z in REAL+ ; then z 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 ) ) } by A31, Lm3, XBOOLE_0:def_3; then consider C being Subset of RAT+ such that A35: z = C and A36: for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ; A37: y in C by A2, A30, A31, A35, Def5; A c= C proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in C ) assume A38: e in A ; ::_thesis: e in C then reconsider x9 = e as Element of RAT+ ; x9 <=' y9 by A33, A34, A38; hence e in C by A36, A37; ::_thesis: verum end; hence x <=' z by A29, A31, A32, A35, Def5; ::_thesis: verum end; supposethat A39: not x in RAT+ and A40: not y in RAT+ and A41: z in RAT+ ; ::_thesis: x <=' z reconsider z9 = z as Element of RAT+ by A41; x in REAL+ ; 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 ) ) } by A39, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A42: x = A and 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 ) ) ; y in REAL+ ; then y 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 ) ) } by A40, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A43: y = B and for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; A c= B by A1, A39, A40, A42, A43, Def5; then not z9 in A by A2, A40, A43, Def5; hence x <=' z by A39, A42, Def5; ::_thesis: verum end; supposethat A44: not x in RAT+ and A45: not y in RAT+ and A46: not z in RAT+ ; ::_thesis: x <=' z z in REAL+ ; then z 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 ) ) } by A46, Lm3, XBOOLE_0:def_3; then consider C being Subset of RAT+ such that A47: z = C and for r being Element of RAT+ st r in C holds ( ( for s being Element of RAT+ st s <=' r holds s in C ) & ex s being Element of RAT+ st ( s in C & r < s ) ) ; y in REAL+ ; then y 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 ) ) } by A45, Lm3, XBOOLE_0:def_3; then consider B being Subset of RAT+ such that A48: y = B and for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ; A49: B c= C by A2, A45, A46, A48, A47, Def5; x in REAL+ ; 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 ) ) } by A44, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A50: x = A and 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 ) ) ; A c= B by A1, A44, A45, A50, A48, Def5; then A c= C by A49, XBOOLE_1:1; hence x <=' z by A44, A46, A50, A47, Def5; ::_thesis: verum end; end; end; theorem :: ARYTM_2:8 for X, Y being Subset of REAL+ st ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds x <=' y ) holds ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) proof let X, Y be Subset of REAL+; ::_thesis: ( ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds x <=' y ) implies ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) ) given x1 being Element of REAL+ such that A1: x1 in Y ; ::_thesis: ( ex x, y being Element of REAL+ st ( x in X & y in Y & not x <=' y ) or ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) ) set Z = { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ; assume A2: for x, y being Element of REAL+ st x in X & y in Y holds x <=' y ; ::_thesis: ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) percases ( ex z9 being Element of RAT+ st for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < z9 ) or for z9 being Element of RAT+ holds not for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < z9 ) ) ; suppose ex z9 being Element of RAT+ st for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; ::_thesis: ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) then consider z9 being Element of RAT+ such that A3: for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; z9 in RAT+ ; then reconsider z = z9 as Element of REAL+ by Th1; take z ; ::_thesis: for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) let x, y be Element of REAL+ ; ::_thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) ) assume that A4: x in X and A5: y in Y ; ::_thesis: ( x <=' z & z <=' y ) thus x <=' z ::_thesis: z <=' y proof assume z < x ; ::_thesis: contradiction then consider x0 being Element of REAL+ such that A6: x0 in RAT+ and A7: ( x0 < x & z < x0 ) by Lm30; reconsider x9 = x0 as Element of RAT+ by A6; ( z9 < x9 & x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ) by A4, A7, Lm14; hence contradiction by A3; ::_thesis: verum end; assume y < z ; ::_thesis: contradiction then consider y0 being Element of REAL+ such that A8: y0 in RAT+ and A9: y0 < z and A10: y < y0 by Lm30; reconsider y9 = y0 as Element of RAT+ by A8; y9 < z9 by A9, Lm14; then y9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } by A3; then ex y99 being Element of RAT+ st ( y9 = y99 & ex x, z being Element of REAL+ st ( z = y99 & x in X & z < x ) ) ; then consider x1, y1 being Element of REAL+ such that A11: y1 = y9 and A12: x1 in X and A13: y1 < x1 ; y < x1 by A10, A11, A13, Lm31; hence contradiction by A2, A5, A12; ::_thesis: verum end; supposeA14: for z9 being Element of RAT+ holds not for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; ::_thesis: ex z being Element of REAL+ st for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) A15: now__::_thesis:_not__{__z9_where_z9_is_Element_of_RAT+_:_ex_x,_z_being_Element_of_REAL+_st_ (_z_=_z9_&_x_in_X_&_z_<_x_)__}__in__{___{__s_where_s_is_Element_of_RAT+_:_s_<_t__}__where_t_is_Element_of_RAT+_:_t_<>_{}__}_ assume { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction then consider t being Element of RAT+ such that A16: { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } = { s where s is Element of RAT+ : s < t } and t <> {} ; for x9 being Element of RAT+ holds ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < t ) proof let x9 be Element of RAT+ ; ::_thesis: ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } iff x9 < t ) hereby ::_thesis: ( x9 < t implies x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ) assume x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ; ::_thesis: x9 < t then ex s being Element of RAT+ st ( s = x9 & s < t ) by A16; hence x9 < t ; ::_thesis: verum end; thus ( x9 < t implies x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ) by A16; ::_thesis: verum end; hence contradiction by A14; ::_thesis: verum end; A17: { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } or e in RAT+ ) assume e in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } ; ::_thesis: e in RAT+ then ex z9 being Element of RAT+ st ( e = z9 & ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) ) ; hence e in RAT+ ; ::_thesis: verum end; now__::_thesis:_not__{__z9_where_z9_is_Element_of_RAT+_:_ex_x,_z_being_Element_of_REAL+_st_ (_z_=_z9_&_x_in_X_&_z_<_x_)__}__=_{} assume { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } = {} ; ::_thesis: contradiction then A18: for x9 being Element of RAT+ st x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } holds x9 < {} ; for x9 being Element of RAT+ st x9 < {} holds x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } by ARYTM_3:64; hence contradiction by A14, A18; ::_thesis: verum end; then reconsider Z = { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) } as non empty Subset of RAT+ by A17; A19: now__::_thesis:_not_Z_=_RAT+ assume A20: Z = RAT+ ; ::_thesis: contradiction percases ( x1 in RAT+ or not x1 in RAT+ ) ; suppose x1 in RAT+ ; ::_thesis: contradiction then reconsider x9 = x1 as Element of RAT+ ; x9 in Z by A20; then ex z9 being Element of RAT+ st ( x9 = z9 & ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) ) ; hence contradiction by A1, A2; ::_thesis: verum end; supposeA21: not x1 in RAT+ ; ::_thesis: contradiction x1 in REAL+ ; then x1 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 ) ) } by A21, Lm3, XBOOLE_0:def_3; then consider A being Subset of RAT+ such that A22: x1 = A and 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 ) ) ; x1 <> RAT+ by Lm28; then consider x9 being Element of RAT+ such that A23: not x9 in A by A22, SUBSET_1:28; x9 in RAT+ ; then reconsider x2 = x9 as Element of REAL+ by Th1; x2 in Z by A20; then ex z9 being Element of RAT+ st ( x9 = z9 & ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) ) ; then consider x being Element of REAL+ such that A24: x in X and A25: x2 < x ; x1 < x2 by A21, A22, A23, Def5; then x1 < x by A25, Lm31; hence contradiction by A1, A2, A24; ::_thesis: verum end; end; end; for t being Element of RAT+ st t in Z holds ( ( for s being Element of RAT+ st s <=' t holds s in Z ) & ex s being Element of RAT+ st ( s in Z & t < s ) ) proof let t be Element of RAT+ ; ::_thesis: ( t in Z implies ( ( for s being Element of RAT+ st s <=' t holds s in Z ) & ex s being Element of RAT+ st ( s in Z & t < s ) ) ) t in RAT+ ; then reconsider y0 = t as Element of REAL+ by Th1; assume t in Z ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds s in Z ) & ex s being Element of RAT+ st ( s in Z & t < s ) ) then ex z9 being Element of RAT+ st ( z9 = t & ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) ) ; then consider x0 being Element of REAL+ such that A26: x0 in X and A27: y0 < x0 ; thus for s being Element of RAT+ st s <=' t holds s in Z ::_thesis: ex s being Element of RAT+ st ( s in Z & t < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in Z ) s in RAT+ ; then reconsider z = s as Element of REAL+ by Th1; assume s <=' t ; ::_thesis: s in Z then z <=' y0 by Lm14; then z < x0 by A27, Lm31; hence s in Z by A26; ::_thesis: verum end; consider z being Element of REAL+ such that A28: z in RAT+ and A29: z < x0 and A30: y0 < z by A27, Lm30; reconsider z9 = z as Element of RAT+ by A28; take z9 ; ::_thesis: ( z9 in Z & t < z9 ) thus z9 in Z by A26, A29; ::_thesis: t < z9 thus t < z9 by A30, Lm14; ::_thesis: verum end; then Z 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 ) ) } ; then A31: Z 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 ) ) } \ {RAT+} by A19, ZFMISC_1:56; then Z 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 ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15, XBOOLE_0:def_5; then reconsider z = Z as Element of REAL+ by Lm4; take z ; ::_thesis: for x, y being Element of REAL+ st x in X & y in Y holds ( x <=' z & z <=' y ) let x, y be Element of REAL+ ; ::_thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) ) assume that A32: x in X and A33: y in Y ; ::_thesis: ( x <=' z & z <=' y ) A34: now__::_thesis:_not_z_in_RAT+ assume z in RAT+ ; ::_thesis: contradiction then z in {{}} by A31, Lm9, XBOOLE_0:def_4; hence contradiction by TARSKI:def_1; ::_thesis: verum end; hereby ::_thesis: z <=' y assume z < x ; ::_thesis: contradiction then consider x0 being Element of REAL+ such that A35: x0 in RAT+ and A36: x0 < x and A37: z < x0 by Lm30; reconsider x9 = x0 as Element of RAT+ by A35; x9 in z by A32, A36; hence contradiction by A34, A37, Def5; ::_thesis: verum end; assume y < z ; ::_thesis: contradiction then consider y0 being Element of REAL+ such that A38: y0 in RAT+ and A39: y0 < z and A40: y < y0 by Lm30; reconsider y9 = y0 as Element of RAT+ by A38; y9 in z by A34, A39, Def5; then ex z9 being Element of RAT+ st ( y9 = z9 & ex x, z being Element of REAL+ st ( z = z9 & x in X & z < x ) ) ; then consider x0 being Element of REAL+ such that A41: x0 in X and A42: y0 < x0 ; y < x0 by A40, A42, Lm31; hence contradiction by A2, A33, A41; ::_thesis: verum end; end; end; Lm32: one = 1 ; Lm33: {} = {} ; Lm34: for A, B being Element of DEDEKIND_CUTS st A + B = A & A <> {} holds B = {} proof let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( A + B = A & A <> {} implies B = {} ) assume that A1: A + B = A and A2: A <> {} and A3: B <> {} ; ::_thesis: contradiction A4: ex A0 being Element of RAT+ st A0 in A by A2, SUBSET_1:4; consider y9 being Element of RAT+ such that A5: y9 in B and A6: y9 <> {} by A3, Lm15; defpred S1[ Element of RAT+ ] means $1 *' y9 in A; {} *' y9 = {} by ARYTM_3:48; then A7: S1[ {} ] by A4, Lm16, ARYTM_3:64; A <> RAT+ by ZFMISC_1:56; then consider r being Element of RAT+ such that A8: not r in A by SUBSET_1:28; consider n being Element of RAT+ such that A9: n in omega and A10: r <=' n *' y9 by A6, ARYTM_3:95; A11: not S1[n] by A8, A10, Lm16; consider n0 being Element of RAT+ such that n0 in omega and A12: ( S1[n0] & not S1[n0 + one] ) from ARYTM_3:sch_1(Lm32, Lm33, A9, A7, A11); (n0 + one) *' y9 = (n0 *' y9) + (one *' y9) by ARYTM_3:57 .= (n0 *' y9) + y9 by ARYTM_3:53 ; hence contradiction by A1, A5, A12; ::_thesis: verum end; Lm35: for x, y being Element of REAL+ st x + y = x holds y = {} proof let x, y be Element of REAL+ ; ::_thesis: ( x + y = x implies y = {} ) assume that A1: x + y = x and A2: y <> {} ; ::_thesis: contradiction A3: x <> {} by A1, A2, Th5; then A4: DEDEKIND_CUT x <> {} by Lm10; DEDEKIND_CUT x = DEDEKIND_CUT (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y))) by A1, A2, A3, Def8 .= (DEDEKIND_CUT x) + (DEDEKIND_CUT y) by Lm12 ; then DEDEKIND_CUT y = {} by A4, Lm34; hence contradiction by A2, Lm10; ::_thesis: verum end; Lm36: for A, B being Element of DEDEKIND_CUTS st A <> {} & A c= B & A <> B holds ex C being Element of DEDEKIND_CUTS st A + C = B proof let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( A <> {} & A c= B & A <> B implies ex C being Element of DEDEKIND_CUTS st A + C = B ) assume that A1: A <> {} and A2: ( A c= B & A <> B ) ; ::_thesis: ex C being Element of DEDEKIND_CUTS st A + C = B not B c= A by A2, XBOOLE_0:def_10; then consider s1 being Element of RAT+ such that A3: ( s1 in B & not s1 in A ) by SUBSET_1:2; set DIF = { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } ; A4: { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } or e in RAT+ ) assume e in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } ; ::_thesis: e in RAT+ then ex t being Element of RAT+ st ( t = e & ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) ) ; hence e in RAT+ ; ::_thesis: verum end; s1 + {} = s1 by ARYTM_3:84; then A5: {} in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } by A3; then reconsider DIF = { t where t is Element of RAT+ : ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) } as non empty Subset of RAT+ by A4; for t being Element of RAT+ st t in DIF holds ( ( for s being Element of RAT+ st s <=' t holds s in DIF ) & ex s being Element of RAT+ st ( s in DIF & t < s ) ) proof let t be Element of RAT+ ; ::_thesis: ( t in DIF implies ( ( for s being Element of RAT+ st s <=' t holds s in DIF ) & ex s being Element of RAT+ st ( s in DIF & t < s ) ) ) assume t in DIF ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds s in DIF ) & ex s being Element of RAT+ st ( s in DIF & t < s ) ) then ex x9 being Element of RAT+ st ( x9 = t & ex r, s being Element of RAT+ st ( not r in A & s in B & r + x9 = s ) ) ; then consider r0, s0 being Element of RAT+ such that A6: not r0 in A and A7: s0 in B and A8: r0 + t = s0 ; thus for s being Element of RAT+ st s <=' t holds s in DIF ::_thesis: ex s being Element of RAT+ st ( s in DIF & t < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in DIF ) assume s <=' t ; ::_thesis: s in DIF then consider p being Element of RAT+ such that A9: s + p = t by ARYTM_3:def_13; A10: t <=' s0 by A8, ARYTM_3:77; p <=' t by A9, ARYTM_3:77; then p <=' s0 by A10, ARYTM_3:67; then consider q being Element of RAT+ such that A11: p + q = s0 by ARYTM_3:def_13; (r0 + s) + p = q + p by A8, A9, A11, ARYTM_3:51; then A12: r0 + s = q by ARYTM_3:62; q in B by A7, A11, Lm16, ARYTM_3:77; hence s in DIF by A6, A12; ::_thesis: verum end; consider s1 being Element of RAT+ such that A13: s1 in B and A14: s0 < s1 by A7, Lm7; consider q being Element of RAT+ such that A15: s0 + q = s1 by A14, ARYTM_3:def_13; take t + q ; ::_thesis: ( t + q in DIF & t < t + q ) A16: r0 + (t + q) = s1 by A8, A15, ARYTM_3:51; hence t + q in DIF by A6, A13; ::_thesis: t < t + q ( t <=' t + q & t <> t + q ) by A8, A14, A16, ARYTM_3:77; hence t < t + q by ARYTM_3:68; ::_thesis: verum end; then A17: DIF 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 ) ) } ; B <> RAT+ by ZFMISC_1:56; then consider s2 being Element of RAT+ such that A18: not s2 in B by SUBSET_1:28; now__::_thesis:_not_s2_in_DIF assume s2 in DIF ; ::_thesis: contradiction then ex t being Element of RAT+ st ( t = s2 & ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) ) ; hence contradiction by A18, Lm16, ARYTM_3:77; ::_thesis: verum end; then DIF <> RAT+ ; then reconsider DIF = DIF as Element of DEDEKIND_CUTS by A17, ZFMISC_1:56; take DIF ; ::_thesis: A + DIF = B set C = { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } ; B = { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } proof thus B c= { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } :: according to XBOOLE_0:def_10 ::_thesis: { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } c= B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } ) assume A19: e in B ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } then reconsider y9 = e as Element of RAT+ ; percases ( y9 in A or not y9 in A ) ; supposeA20: y9 in A ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } y9 = y9 + {} by ARYTM_3:84; hence e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } by A5, A20; ::_thesis: verum end; supposeA21: not y9 in A ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } consider s0 being Element of RAT+ such that A22: s0 in B and A23: y9 < s0 by A19, Lm7; set Z = { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } ; A24: not s0 in A by A21, A23, Lm16; A25: s0 + {} = s0 by ARYTM_3:84; for r2 being Element of RAT+ st r2 < s0 holds ex s, t being Element of RAT+ st ( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) proof let r2 be Element of RAT+ ; ::_thesis: ( r2 < s0 implies ex s, t being Element of RAT+ st ( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) ) assume A26: r2 < s0 ; ::_thesis: ex s, t being Element of RAT+ st ( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) then A27: r2 <> s0 ; percases ( r2 in A or not r2 in A ) ; supposeA28: r2 in A ; ::_thesis: ex s, t being Element of RAT+ st ( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) take r2 ; ::_thesis: ex t being Element of RAT+ st ( r2 in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = r2 + t ) take {} ; ::_thesis: ( r2 in A & {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = r2 + {} ) thus r2 in A by A28; ::_thesis: ( {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = r2 + {} ) thus {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } by A24, A25; ::_thesis: r2 = r2 + {} thus r2 = r2 + {} by ARYTM_3:84; ::_thesis: verum end; supposeA29: not r2 in A ; ::_thesis: ex s, t being Element of RAT+ st ( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) consider q being Element of RAT+ such that A30: r2 + q = s0 by A26, ARYTM_3:def_13; defpred S1[ Element of RAT+ ] means $1 *' q in A; {} *' q = {} by ARYTM_3:48; then A31: S1[ {} ] by A1, Lm17; q <> {} by A27, A30, ARYTM_3:84; then consider n being Element of RAT+ such that A32: n in omega and A33: s0 <=' n *' q by ARYTM_3:95; A34: not S1[n] by A24, A33, Lm16; consider n0 being Element of RAT+ such that n0 in omega and A35: S1[n0] and A36: not S1[n0 + one] from ARYTM_3:sch_1(Lm32, Lm33, A32, A31, A34); n0 *' q <=' r2 by A29, A35, Lm16; then (n0 *' q) + q <=' s0 by A30, ARYTM_3:76; then consider t being Element of RAT+ such that A37: ((n0 *' q) + q) + t = s0 by ARYTM_3:def_13; take n0 *' q ; ::_thesis: ex t being Element of RAT+ st ( n0 *' q in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t ) take t ; ::_thesis: ( n0 *' q in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t ) thus n0 *' q in A by A35; ::_thesis: ( t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t ) (n0 + one) *' q = (n0 *' q) + (one *' q) by ARYTM_3:57 .= (n0 *' q) + q by ARYTM_3:53 ; hence t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } by A36, A37; ::_thesis: r2 = (n0 *' q) + t ((n0 *' q) + t) + q = r2 + q by A30, A37, ARYTM_3:51; hence r2 = (n0 *' q) + t by ARYTM_3:62; ::_thesis: verum end; end; end; then consider s, t being Element of RAT+ such that A38: s in A and A39: t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) } and A40: y9 = s + t by A23; ex r being Element of RAT+ st ( t = r & ex x9 being Element of RAT+ st ( not x9 in A & x9 + r = s0 ) ) by A39; then t in DIF by A22; hence e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } by A38, A40; ::_thesis: verum end; end; end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } or e in B ) assume e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } ; ::_thesis: e in B then consider s3, t3 being Element of RAT+ such that A41: e = s3 + t3 and A42: s3 in A and A43: t3 in DIF ; ex t being Element of RAT+ st ( t3 = t & ex r, s being Element of RAT+ st ( not r in A & s in B & r + t = s ) ) by A43; then consider r4, s4 being Element of RAT+ such that A44: not r4 in A and A45: s4 in B and A46: r4 + t3 = s4 ; s3 <=' r4 by A42, A44, Lm16; then s3 + t3 <=' s4 by A46, ARYTM_3:76; hence e in B by A41, A45, Lm16; ::_thesis: verum end; hence A + DIF = B ; ::_thesis: verum end; Lm37: for x, y being Element of REAL+ st x <=' y holds DEDEKIND_CUT x c= DEDEKIND_CUT y proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y ) assume A1: x <=' y ; ::_thesis: DEDEKIND_CUT x c= DEDEKIND_CUT y assume A2: not DEDEKIND_CUT x c= DEDEKIND_CUT y ; ::_thesis: contradiction ( DEDEKIND_CUT 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 ) ) } & DEDEKIND_CUT y 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 ) ) } ) by XBOOLE_0:def_5; then DEDEKIND_CUT y c= DEDEKIND_CUT x by A2, Lm13; then y <=' x by Lm20; hence contradiction by A1, A2, Lm21; ::_thesis: verum end; theorem Th9: :: ARYTM_2:9 for x, y being Element of REAL+ st x <=' y holds ex z being Element of REAL+ st x + z = y proof let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies ex z being Element of REAL+ st x + z = y ) assume A1: x <=' y ; ::_thesis: ex z being Element of REAL+ st x + z = y percases ( x = {} or x = y or ( x <> {} & x <> y ) ) ; supposeA2: x = {} ; ::_thesis: ex z being Element of REAL+ st x + z = y take y ; ::_thesis: x + y = y thus x + y = y by A2, Def8; ::_thesis: verum end; supposeA3: x = y ; ::_thesis: ex z being Element of REAL+ st x + z = y {} in RAT+ ; then reconsider z = {} as Element of REAL+ by Th1; take z ; ::_thesis: x + z = y thus x + z = y by A3, Def8; ::_thesis: verum end; supposethat A4: x <> {} and A5: x <> y ; ::_thesis: ex z being Element of REAL+ st x + z = y A6: DEDEKIND_CUT x <> {} by A4, Lm10; DEDEKIND_CUT x <> DEDEKIND_CUT y by A5, Lm22; then consider C being Element of DEDEKIND_CUTS such that A7: (DEDEKIND_CUT x) + C = DEDEKIND_CUT y by A1, A6, Lm36, Lm37; take GLUED C ; ::_thesis: x + (GLUED C) = y now__::_thesis:_not_C_=_{} assume A8: C = {} ; ::_thesis: contradiction for e being set holds not e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } proof given e being set such that A9: e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } ; ::_thesis: contradiction ex r, s being Element of RAT+ st ( e = r + s & r in C & s in DEDEKIND_CUT x ) by A9; hence contradiction by A8; ::_thesis: verum end; then { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } = {} by XBOOLE_0:def_1; then DEDEKIND_CUT y = {} by A7, Def6; hence contradiction by A1, A6, Lm37, XBOOLE_1:3; ::_thesis: verum end; then GLUED C <> {} by Lm11; hence x + (GLUED C) = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT (GLUED C))) by A4, Def8 .= GLUED (DEDEKIND_CUT y) by A7, Lm12 .= y by Lm23 ; ::_thesis: verum end; end; end; theorem Th10: :: ARYTM_2:10 for x, y being Element of REAL+ ex z being Element of REAL+ st ( x + z = y or y + z = x ) proof let x, y be Element of REAL+ ; ::_thesis: ex z being Element of REAL+ st ( x + z = y or y + z = x ) ( x <=' y or y <=' x ) ; hence ex z being Element of REAL+ st ( x + z = y or y + z = x ) by Th9; ::_thesis: verum end; theorem Th11: :: ARYTM_2:11 for x, y, z being Element of REAL+ st x + y = x + z holds y = z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x + y = x + z implies y = z ) assume A1: x + y = x + z ; ::_thesis: y = z consider q being Element of REAL+ such that A2: ( z + q = y or y + q = z ) by Th10; percases ( z + q = y or y + q = z ) by A2; supposeA3: z + q = y ; ::_thesis: y = z then x + y = (x + y) + q by A1, Th6; then q = {} by Lm35; hence y = z by A3, Def8; ::_thesis: verum end; supposeA4: y + q = z ; ::_thesis: y = z then x + z = (x + z) + q by A1, Th6; then q = {} by Lm35; hence y = z by A4, Def8; ::_thesis: verum end; end; end; Lm38: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) c= (A *' B) *' C proof let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A *' (B *' C) c= (A *' B) *' C let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' (B *' C) or e in (A *' B) *' C ) assume e in A *' (B *' C) ; ::_thesis: e in (A *' B) *' C then consider r0, s0 being Element of RAT+ such that A1: ( e = r0 *' s0 & r0 in A ) and A2: s0 in B *' C ; consider r1, s1 being Element of RAT+ such that A3: ( s0 = r1 *' s1 & r1 in B ) and A4: s1 in C by A2; ( e = (r0 *' r1) *' s1 & r0 *' r1 in A *' B ) by A1, A3, ARYTM_3:52; hence e in (A *' B) *' C by A4; ::_thesis: verum end; Lm39: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) = (A *' B) *' C proof let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A *' (B *' C) = (A *' B) *' C ( A *' (B *' C) c= (A *' B) *' C & (A *' B) *' C c= A *' (B *' C) ) by Lm38; hence A *' (B *' C) = (A *' B) *' C by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: ARYTM_2:12 for x, y, z being Element of REAL+ holds x *' (y *' z) = (x *' y) *' z proof let x, y, z be Element of REAL+ ; ::_thesis: x *' (y *' z) = (x *' y) *' z thus x *' (y *' z) = GLUED ((DEDEKIND_CUT x) *' ((DEDEKIND_CUT y) *' (DEDEKIND_CUT z))) by Lm12 .= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) *' (DEDEKIND_CUT z)) by Lm39 .= (x *' y) *' z by Lm12 ; ::_thesis: verum end; Lm40: for x, y being Element of REAL+ holds ( not x *' y = {} or x = {} or y = {} ) proof let x, y be Element of REAL+ ; ::_thesis: ( not x *' y = {} or x = {} or y = {} ) assume A1: x *' y = {} ; ::_thesis: ( x = {} or y = {} ) ( DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} ) proof assume DEDEKIND_CUT x <> {} ; ::_thesis: DEDEKIND_CUT y = {} then consider r0 being Element of RAT+ such that A2: r0 in DEDEKIND_CUT x by SUBSET_1:4; assume DEDEKIND_CUT y <> {} ; ::_thesis: contradiction then consider s0 being Element of RAT+ such that A3: s0 in DEDEKIND_CUT y by SUBSET_1:4; r0 *' s0 in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } by A2, A3; hence contradiction by A1, Lm11; ::_thesis: verum end; hence ( x = {} or y = {} ) by Lm10; ::_thesis: verum end; Lm41: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B + C) = (A *' B) + (A *' C) proof let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A *' (B + C) = (A *' B) + (A *' C) thus A *' (B + C) c= (A *' B) + (A *' C) :: according to XBOOLE_0:def_10 ::_thesis: (A *' B) + (A *' C) c= A *' (B + C) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' (B + C) or e in (A *' B) + (A *' C) ) assume e in A *' (B + C) ; ::_thesis: e in (A *' B) + (A *' C) then consider r0, v0 being Element of RAT+ such that A1: e = r0 *' v0 and A2: r0 in A and A3: v0 in B + C ; consider s0, t0 being Element of RAT+ such that A4: v0 = s0 + t0 and A5: ( s0 in B & t0 in C ) by A3; A6: e = (r0 *' s0) + (r0 *' t0) by A1, A4, ARYTM_3:57; ( r0 *' s0 in A *' B & r0 *' t0 in A *' C ) by A2, A5; hence e in (A *' B) + (A *' C) by A6; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (A *' B) + (A *' C) or e in A *' (B + C) ) assume e in (A *' B) + (A *' C) ; ::_thesis: e in A *' (B + C) then consider s1, t1 being Element of RAT+ such that A7: e = s1 + t1 and A8: s1 in A *' B and A9: t1 in A *' C ; consider r0, s0 being Element of RAT+ such that A10: s1 = r0 *' s0 and A11: r0 in A and A12: s0 in B by A8; consider r09, t0 being Element of RAT+ such that A13: t1 = r09 *' t0 and A14: r09 in A and A15: t0 in C by A9; percases ( r0 <=' r09 or r09 <=' r0 ) ; suppose r0 <=' r09 ; ::_thesis: e in A *' (B + C) then r0 *' s0 <=' r09 *' s0 by ARYTM_3:82; then consider s09 being Element of RAT+ such that A16: r0 *' s0 = r09 *' s09 and A17: s09 <=' s0 by ARYTM_3:79; s09 in B by A12, A17, Lm16; then A18: s09 + t0 in B + C by A15; e = r09 *' (s09 + t0) by A7, A10, A13, A16, ARYTM_3:57; hence e in A *' (B + C) by A14, A18; ::_thesis: verum end; suppose r09 <=' r0 ; ::_thesis: e in A *' (B + C) then r09 *' t0 <=' r0 *' t0 by ARYTM_3:82; then consider t09 being Element of RAT+ such that A19: r09 *' t0 = r0 *' t09 and A20: t09 <=' t0 by ARYTM_3:79; t09 in C by A15, A20, Lm16; then A21: s0 + t09 in B + C by A12; e = r0 *' (s0 + t09) by A7, A10, A13, A19, ARYTM_3:57; hence e in A *' (B + C) by A11, A21; ::_thesis: verum end; end; end; theorem :: ARYTM_2:13 for x, y, z being Element of REAL+ holds x *' (y + z) = (x *' y) + (x *' z) proof let x, y, z be Element of REAL+ ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) percases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ; supposeA1: x = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) hence x *' (y + z) = x by Th4 .= x + x by A1, Def8 .= x + (x *' z) by A1, Th4 .= (x *' y) + (x *' z) by A1, Th4 ; ::_thesis: verum end; supposeA2: y = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) hence x *' (y + z) = x *' z by Def8 .= y + (x *' z) by A2, Def8 .= (x *' y) + (x *' z) by A2, Th4 ; ::_thesis: verum end; supposeA3: z = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) hence x *' (y + z) = x *' y by Def8 .= (x *' y) + z by A3, Def8 .= (x *' y) + (x *' z) by A3, Th4 ; ::_thesis: verum end; supposethat A4: x <> {} and A5: ( y <> {} & z <> {} ) ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) A6: ( x *' y <> {} & x *' z <> {} ) by A4, A5, Lm40; thus x *' (y + z) = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))))) by A5, Def8 .= GLUED ((DEDEKIND_CUT x) *' ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by Lm12 .= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) + ((DEDEKIND_CUT x) *' (DEDEKIND_CUT z))) by Lm41 .= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) + (DEDEKIND_CUT (x *' z))) by Lm12 .= GLUED ((DEDEKIND_CUT (x *' y)) + (DEDEKIND_CUT (x *' z))) by Lm12 .= (x *' y) + (x *' z) by A6, Def8 ; ::_thesis: verum end; end; end; one in RAT+ ; then reconsider rone = one as Element of REAL+ by Th1; Lm42: for B being set st B 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 ) ) } & B <> {} holds ex r being Element of RAT+ st ( r in B & r <> {} ) proof let B be set ; ::_thesis: ( B 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 ) ) } & B <> {} implies ex r being Element of RAT+ st ( r in B & r <> {} ) ) assume that A1: B 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 ) ) } and A2: B <> {} ; ::_thesis: ex r being Element of RAT+ st ( r in B & r <> {} ) consider A being Subset of RAT+ such that A3: B = A and A4: 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 ) ) by A1; consider r0 being Element of RAT+ such that A5: r0 in A by A2, A3, SUBSET_1:4; consider r1 being Element of RAT+ such that A6: r1 in A and A7: r0 < r1 by A4, A5; A8: ( r1 <> {} or r0 <> {} ) by A7; for r, s being Element of RAT+ st r in A & s <=' r holds s in A by A4; then consider r1, r2, r3 being Element of RAT+ such that A9: ( r1 in A & r2 in A ) and r3 in A and A10: r1 <> r2 and r2 <> r3 and r3 <> r1 by A5, A6, A8, ARYTM_3:75; ( r1 <> {} or r2 <> {} ) by A10; hence ex r being Element of RAT+ st ( r in B & r <> {} ) by A3, A9; ::_thesis: verum end; Lm43: for A being Element of DEDEKIND_CUTS st A <> {} holds ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone proof let A be Element of DEDEKIND_CUTS ; ::_thesis: ( A <> {} implies ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone ) assume A1: A <> {} ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone percases ( A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } or not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ) ; suppose A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone then consider r0 being Element of RAT+ such that A2: A = { s where s is Element of RAT+ : s < r0 } and A3: r0 <> {} ; consider s0 being Element of RAT+ such that A4: r0 *' s0 = one by A3, ARYTM_3:54; set B = { s where s is Element of RAT+ : s < s0 } ; { s where s is Element of RAT+ : s < s0 } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < s0 } or e in RAT+ ) assume e in { s where s is Element of RAT+ : s < s0 } ; ::_thesis: e in RAT+ then ex s being Element of RAT+ st ( s = e & s < s0 ) ; hence e in RAT+ ; ::_thesis: verum end; then reconsider B = { s where s is Element of RAT+ : s < s0 } as Subset of RAT+ ; for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) proof let r be Element of RAT+ ; ::_thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ) assume r in B ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) then A5: ex s being Element of RAT+ st ( s = r & s < s0 ) ; then consider t being Element of RAT+ such that A6: r < t and A7: t < s0 by ARYTM_3:93; thus for s being Element of RAT+ st s <=' r holds s in B ::_thesis: ex s being Element of RAT+ st ( s in B & r < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in B ) assume s <=' r ; ::_thesis: s in B then s < s0 by A5, ARYTM_3:69; hence s in B ; ::_thesis: verum end; take t ; ::_thesis: ( t in B & r < t ) thus t in B by A7; ::_thesis: r < t thus r < t by A6; ::_thesis: verum end; then A8: B 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 ) ) } ; for s being Element of RAT+ holds ( not s = s0 or not s < s0 ) ; then not s0 in B ; then B <> RAT+ ; then reconsider B = B as Element of DEDEKIND_CUTS by A8, ZFMISC_1:56; A9: A *' B = { s where s is Element of RAT+ : s < r0 *' s0 } proof thus A *' B c= { s where s is Element of RAT+ : s < r0 *' s0 } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < r0 *' s0 } c= A *' B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' B or e in { s where s is Element of RAT+ : s < r0 *' s0 } ) assume e in A *' B ; ::_thesis: e in { s where s is Element of RAT+ : s < r0 *' s0 } then consider r1, s1 being Element of RAT+ such that A10: e = r1 *' s1 and A11: r1 in A and A12: s1 in B ; ex s being Element of RAT+ st ( s = r1 & s < r0 ) by A2, A11; then A13: r1 *' s1 <=' r0 *' s1 by ARYTM_3:82; A14: ex s being Element of RAT+ st ( s = s1 & s < s0 ) by A12; then s1 <> s0 ; then A15: r0 *' s1 <> r0 *' s0 by A3, ARYTM_3:56; r0 *' s1 <=' r0 *' s0 by A14, ARYTM_3:82; then r0 *' s1 < r0 *' s0 by A15, ARYTM_3:68; then r1 *' s1 < r0 *' s0 by A13, ARYTM_3:69; hence e in { s where s is Element of RAT+ : s < r0 *' s0 } by A10; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r0 *' s0 } or e in A *' B ) assume e in { s where s is Element of RAT+ : s < r0 *' s0 } ; ::_thesis: e in A *' B then consider s1 being Element of RAT+ such that A16: e = s1 and A17: s1 < r0 *' s0 ; consider t0 being Element of RAT+ such that A18: s1 = r0 *' t0 and A19: t0 <=' s0 by A17, ARYTM_3:79; t0 <> s0 by A17, A18; then t0 < s0 by A19, ARYTM_3:68; then t0 in B ; then consider t1 being Element of RAT+ such that A20: t1 in B and A21: t0 < t1 by Lm7; r0 *' t0 <=' t1 *' r0 by A21, ARYTM_3:82; then consider r1 being Element of RAT+ such that A22: r0 *' t0 = t1 *' r1 and A23: r1 <=' r0 by ARYTM_3:79; t0 <> t1 by A21; then r1 <> r0 by A3, A22, ARYTM_3:56; then r1 < r0 by A23, ARYTM_3:68; then r1 in A by A2; hence e in A *' B by A16, A18, A20, A22; ::_thesis: verum end; ex t0 being Element of RAT+ st ( t0 = rone & DEDEKIND_CUT rone = { s where s is Element of RAT+ : s < t0 } ) by Def3; hence ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone by A4, A9; ::_thesis: verum end; supposeA24: not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone set B = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } ; A25: { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } or e in RAT+ ) assume e in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } ; ::_thesis: e in RAT+ then ex y9 being Element of RAT+ st ( y9 = e & ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) ) ; hence e in RAT+ ; ::_thesis: verum end; A26: A <> RAT+ by ZFMISC_1:56; then consider x0 being Element of RAT+ such that A27: not x0 in A by SUBSET_1:28; x0 *' {} = {} by ARYTM_3:48; then x0 *' {} <=' one by ARYTM_3:64; then A28: {} in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } by A27; then reconsider B = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) } as non empty Subset of RAT+ by A25; A29: A 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 ) ) } by ZFMISC_1:56; ex x9 being Element of RAT+ st x9 in A by A1, SUBSET_1:4; then A30: {} in A by A29, Lm29, ARYTM_3:64; for r being Element of RAT+ st r in B holds ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) proof let r be Element of RAT+ ; ::_thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) ) assume r in B ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds s in B ) & ex s being Element of RAT+ st ( s in B & r < s ) ) then ex y9 being Element of RAT+ st ( r = y9 & ex x9 being Element of RAT+ st ( not x9 in A & x9 *' y9 <=' one ) ) ; then consider x9 being Element of RAT+ such that A31: not x9 in A and A32: x9 *' r <=' one ; thus for s being Element of RAT+ st s <=' r holds s in B ::_thesis: ex s being Element of RAT+ st ( s in B & r < s ) proof let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in B ) assume s <=' r ; ::_thesis: s in B then x9 *' s <=' x9 *' r by ARYTM_3:82; then x9 *' s <=' one by A32, ARYTM_3:67; hence s in B by A31; ::_thesis: verum end; A in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A24, XBOOLE_0:def_5; then consider x99 being Element of RAT+ such that A33: not x99 in A and A34: x99 < x9 by A1, A31, Lm18; consider s being Element of RAT+ such that A35: one = x99 *' s by A30, A33, ARYTM_3:55; take s ; ::_thesis: ( s in B & r < s ) x99 *' s <=' one by A35; hence s in B by A33; ::_thesis: r < s A36: s <> {} by A35, ARYTM_3:48; x99 *' r <=' x9 *' r by A34, ARYTM_3:82; then x99 *' r <=' x99 *' s by A32, A35, ARYTM_3:67; then A37: r <=' s by A30, A33, ARYTM_3:80; ( x99 <> x9 & x99 *' s <=' x9 *' s ) by A34, ARYTM_3:82; then r <> s by A32, A35, A36, ARYTM_3:56, ARYTM_3:66; hence r < s by A37, ARYTM_3:68; ::_thesis: verum end; then A38: B 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 ) ) } ; consider x9 being Element of RAT+ such that A39: x9 in A and A40: x9 <> {} by A1, A29, Lm42; consider y9 being Element of RAT+ such that A41: x9 *' y9 = one by A40, ARYTM_3:55; now__::_thesis:_not_y9_in_B assume y9 in B ; ::_thesis: contradiction then A42: ex s being Element of RAT+ st ( s = y9 & ex x9 being Element of RAT+ st ( not x9 in A & x9 *' s <=' one ) ) ; y9 <> {} by A41, ARYTM_3:48; hence contradiction by A29, A39, A41, A42, Lm29, ARYTM_3:80; ::_thesis: verum end; then B <> RAT+ ; then not B in {RAT+} by TARSKI:def_1; then reconsider B = B as Element of DEDEKIND_CUTS by A38, XBOOLE_0:def_5; take B ; ::_thesis: A *' B = DEDEKIND_CUT rone for r being Element of RAT+ holds ( r in A *' B iff r < one ) proof let r be Element of RAT+ ; ::_thesis: ( r in A *' B iff r < one ) hereby ::_thesis: ( r < one implies r in A *' B ) assume r in A *' B ; ::_thesis: r < one then consider s, t being Element of RAT+ such that A43: r = s *' t and A44: s in A and A45: t in B ; ex z9 being Element of RAT+ st ( z9 = t & ex x9 being Element of RAT+ st ( not x9 in A & x9 *' z9 <=' one ) ) by A45; then consider x9 being Element of RAT+ such that A46: not x9 in A and A47: x9 *' t <=' one ; s <=' x9 by A29, A44, A46, Lm29; then A48: s *' t <=' x9 *' t by ARYTM_3:82; A49: now__::_thesis:_not_r_=_one assume A50: r = one ; ::_thesis: contradiction then t <> {} by A43, ARYTM_3:48; hence contradiction by A43, A44, A46, A47, A48, A50, ARYTM_3:56, ARYTM_3:66; ::_thesis: verum end; r <=' one by A43, A47, A48, ARYTM_3:67; hence r < one by A49, ARYTM_3:68; ::_thesis: verum end; assume A51: r < one ; ::_thesis: r in A *' B then A52: r <> one ; percases ( r = {} or r <> {} ) ; suppose r = {} ; ::_thesis: r in A *' B then r = {} *' {} by ARYTM_3:48; hence r in A *' B by A28, A30; ::_thesis: verum end; suppose r <> {} ; ::_thesis: r in A *' B then consider r9 being Element of RAT+ such that A53: r *' r9 = one by ARYTM_3:55; { (r *' s) where s is Element of RAT+ : s in A } c= RAT+ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r *' s) where s is Element of RAT+ : s in A } or e in RAT+ ) assume e in { (r *' s) where s is Element of RAT+ : s in A } ; ::_thesis: e in RAT+ then ex s being Element of RAT+ st ( e = r *' s & s in A ) ; hence e in RAT+ ; ::_thesis: verum end; then reconsider rA = { (r *' s) where s is Element of RAT+ : s in A } as Subset of RAT+ ; consider dr being Element of RAT+ such that A54: r + dr = one by A51, ARYTM_3:def_13; consider xx being Element of RAT+ such that A55: not xx in A by A26, SUBSET_1:28; set rr = x9 *' dr; dr <> {} by A52, A54, ARYTM_3:50; then consider n0 being Element of RAT+ such that A56: n0 in omega and A57: xx <=' n0 *' (x9 *' dr) by A40, ARYTM_3:78, ARYTM_3:95; defpred S1[ Element of RAT+ ] means $1 *' (x9 *' dr) in A; A58: S1[ {} ] by A30, ARYTM_3:48; A59: not S1[n0] by A29, A55, A57, Lm29; consider n1 being Element of RAT+ such that n1 in omega and A60: S1[n1] and A61: not S1[n1 + one] from ARYTM_3:sch_1(Lm32, Lm33, A56, A58, A59); set s0 = n1 *' (x9 *' dr); A62: now__::_thesis:_not_n1_*'_(x9_*'_dr)_in_rA assume n1 *' (x9 *' dr) in rA ; ::_thesis: contradiction then consider s0 being Element of RAT+ such that A63: r *' s0 = n1 *' (x9 *' dr) and A64: s0 in A ; A65: (n1 + one) *' (x9 *' dr) = (n1 *' (x9 *' dr)) + (one *' (x9 *' dr)) by ARYTM_3:57 .= (r *' s0) + (dr *' x9) by A63, ARYTM_3:53 ; ( s0 <=' x9 or x9 <=' s0 ) ; then consider s1 being Element of RAT+ such that A66: ( ( s1 = s0 & x9 <=' s1 ) or ( s1 = x9 & s0 <=' s1 ) ) ; dr *' x9 <=' dr *' s1 by A66, ARYTM_3:82; then A67: (r *' s1) + (dr *' x9) <=' (r *' s1) + (dr *' s1) by ARYTM_3:76; r *' s0 <=' r *' s1 by A66, ARYTM_3:82; then A68: (r *' s0) + (dr *' x9) <=' (r *' s1) + (dr *' x9) by ARYTM_3:76; (r *' s1) + (dr *' s1) = (r + dr) *' s1 by ARYTM_3:57 .= s1 by A54, ARYTM_3:53 ; hence contradiction by A29, A39, A61, A64, A65, A66, A68, A67, Lm29; ::_thesis: verum end; A69: now__::_thesis:_not_(n1_*'_(x9_*'_dr))_*'_r9_in_A assume A70: (n1 *' (x9 *' dr)) *' r9 in A ; ::_thesis: contradiction r *' ((n1 *' (x9 *' dr)) *' r9) = one *' (n1 *' (x9 *' dr)) by A53, ARYTM_3:52 .= n1 *' (x9 *' dr) by ARYTM_3:53 ; hence contradiction by A62, A70; ::_thesis: verum end; r *' {} = {} by ARYTM_3:48; then {} in rA by A30; then consider s9 being Element of RAT+ such that A71: (n1 *' (x9 *' dr)) *' s9 = one by A62, ARYTM_3:55; A72: (n1 *' (x9 *' dr)) *' (r *' s9) = ((n1 *' (x9 *' dr)) *' s9) *' r by ARYTM_3:52 .= r by A71, ARYTM_3:53 ; ((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) = (((n1 *' (x9 *' dr)) *' r9) *' r) *' s9 by ARYTM_3:52 .= ((n1 *' (x9 *' dr)) *' one) *' s9 by A53, ARYTM_3:52 .= one by A71, ARYTM_3:53 ; then ((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) <=' one ; then r *' s9 in B by A69; hence r in A *' B by A60, A72; ::_thesis: verum end; end; end; then DEDEKIND_CUT (GLUED (A *' B)) = DEDEKIND_CUT rone by Def4; hence A *' B = DEDEKIND_CUT rone by Lm12; ::_thesis: verum end; end; end; theorem :: ARYTM_2:14 for x being Element of REAL+ st x <> {} holds ex y being Element of REAL+ st x *' y = one proof let x be Element of REAL+ ; ::_thesis: ( x <> {} implies ex y being Element of REAL+ st x *' y = one ) assume x <> {} ; ::_thesis: ex y being Element of REAL+ st x *' y = one then DEDEKIND_CUT x <> {} by Lm10; then consider B being Element of DEDEKIND_CUTS such that A1: (DEDEKIND_CUT x) *' B = DEDEKIND_CUT rone by Lm43; take y = GLUED B; ::_thesis: x *' y = one thus x *' y = GLUED (DEDEKIND_CUT rone) by A1, Lm12 .= one by Lm23 ; ::_thesis: verum end; Lm44: for A, B being Element of DEDEKIND_CUTS st A = { r where r is Element of RAT+ : r < one } holds A *' B = B proof let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( A = { r where r is Element of RAT+ : r < one } implies A *' B = B ) assume A1: A = { r where r is Element of RAT+ : r < one } ; ::_thesis: A *' B = B thus A *' B c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A *' B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' B or e in B ) assume e in A *' B ; ::_thesis: e in B then consider r, s being Element of RAT+ such that A2: e = r *' s and A3: r in A and A4: s in B ; ex t being Element of RAT+ st ( t = r & t < one ) by A1, A3; then r *' s <=' one *' s by ARYTM_3:82; then r *' s <=' s by ARYTM_3:53; hence e in B by A2, A4, Lm16; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in A *' B ) assume A5: e in B ; ::_thesis: e in A *' B then reconsider s = e as Element of RAT+ ; consider s1 being Element of RAT+ such that A6: s1 in B and A7: s < s1 by A5, Lm7; s1 <> {} by A7, ARYTM_3:64; then consider s2 being Element of RAT+ such that A8: s1 *' s2 = s by ARYTM_3:55; A9: now__::_thesis:_not_s2_=_one assume s2 = one ; ::_thesis: contradiction then s = s1 by A8, ARYTM_3:53; hence contradiction by A7; ::_thesis: verum end; one *' s = s2 *' s1 by A8, ARYTM_3:53; then s2 <=' one by A7, ARYTM_3:83; then s2 < one by A9, ARYTM_3:68; then s2 in A by A1; hence e in A *' B by A6, A8; ::_thesis: verum end; theorem :: ARYTM_2:15 for x, y being Element of REAL+ st x = one holds x *' y = y proof let x, y be Element of REAL+ ; ::_thesis: ( x = one implies x *' y = y ) assume A1: x = one ; ::_thesis: x *' y = y then ex r being Element of RAT+ st ( x = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3; hence x *' y = GLUED (DEDEKIND_CUT y) by A1, Lm44 .= y by Lm23 ; ::_thesis: verum end; Lm45: for i, j being Element of omega for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds i +^ j = x9 + y9 proof let i, j be Element of omega ; ::_thesis: for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds i +^ j = x9 + y9 let x9, y9 be Element of RAT+ ; ::_thesis: ( i = x9 & j = y9 implies i +^ j = x9 + y9 ) set a = (denominator x9) *^ (denominator y9); set b = ((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)); assume A1: i = x9 ; ::_thesis: ( not j = y9 or i +^ j = x9 + y9 ) then A2: denominator x9 = one by ARYTM_3:def_9; assume A3: j = y9 ; ::_thesis: i +^ j = x9 + y9 then A4: denominator y9 = one by ARYTM_3:def_9; then A5: (denominator x9) *^ (denominator y9) = one by A2, ORDINAL2:39; then A6: RED (((denominator x9) *^ (denominator y9)),(((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)))) = one by ARYTM_3:24; ((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)) = ((numerator x9) *^ one) +^ (numerator y9) by A2, A4, ORDINAL2:39 .= (numerator x9) +^ (numerator y9) by ORDINAL2:39 .= i +^ (numerator y9) by A1, ARYTM_3:def_8 .= i +^ j by A3, ARYTM_3:def_8 ; hence i +^ j = RED ((((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9))),((denominator x9) *^ (denominator y9))) by A5, ARYTM_3:24 .= x9 + y9 by A6, ARYTM_3:def_10 ; ::_thesis: verum end; Lm46: for z9, x9, y9 being Element of RAT+ st z9 < x9 + y9 & x9 <> {} & y9 <> {} holds ex r, s being Element of RAT+ st ( z9 = r + s & r < x9 & s < y9 ) proof let z9, x9, y9 be Element of RAT+ ; ::_thesis: ( z9 < x9 + y9 & x9 <> {} & y9 <> {} implies ex r, s being Element of RAT+ st ( z9 = r + s & r < x9 & s < y9 ) ) assume that A1: z9 < x9 + y9 and A2: x9 <> {} and A3: y9 <> {} ; ::_thesis: ex r, s being Element of RAT+ st ( z9 = r + s & r < x9 & s < y9 ) consider r0, t0 being Element of RAT+ such that A4: z9 = r0 + t0 and A5: r0 <=' x9 and A6: ( t0 <=' y9 & t0 <> y9 ) by A1, A3, ARYTM_3:90; percases ( r0 = {} or r0 <> {} ) ; supposeA7: r0 = {} ; ::_thesis: ex r, s being Element of RAT+ st ( z9 = r + s & r < x9 & s < y9 ) take {} ; ::_thesis: ex s being Element of RAT+ st ( z9 = {} + s & {} < x9 & s < y9 ) take t0 ; ::_thesis: ( z9 = {} + t0 & {} < x9 & t0 < y9 ) thus z9 = {} + t0 by A4, A7; ::_thesis: ( {} < x9 & t0 < y9 ) {} <=' x9 by ARYTM_3:64; hence {} < x9 by A2, ARYTM_3:68; ::_thesis: t0 < y9 thus t0 < y9 by A6, ARYTM_3:68; ::_thesis: verum end; supposeA8: r0 <> {} ; ::_thesis: ex r, s being Element of RAT+ st ( z9 = r + s & r < x9 & s < y9 ) t0 < y9 by A6, ARYTM_3:68; then consider t1 being Element of RAT+ such that A9: t0 < t1 and A10: t1 < y9 by ARYTM_3:93; z9 < t1 + r0 by A4, A9, ARYTM_3:76; then consider t2, r1 being Element of RAT+ such that A11: z9 = t2 + r1 and A12: t2 <=' t1 and A13: ( r1 <=' r0 & r1 <> r0 ) by A8, ARYTM_3:90; take r1 ; ::_thesis: ex s being Element of RAT+ st ( z9 = r1 + s & r1 < x9 & s < y9 ) take t2 ; ::_thesis: ( z9 = r1 + t2 & r1 < x9 & t2 < y9 ) thus z9 = r1 + t2 by A11; ::_thesis: ( r1 < x9 & t2 < y9 ) r1 < r0 by A13, ARYTM_3:68; hence r1 < x9 by A5, ARYTM_3:69; ::_thesis: t2 < y9 thus t2 < y9 by A10, A12, ARYTM_3:69; ::_thesis: verum end; end; end; Lm47: for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) proof let x, y be Element of REAL+ ; ::_thesis: ( x in RAT+ & y in RAT+ implies ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) ) assume that A1: x in RAT+ and A2: y in RAT+ ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) percases ( x = {} or y = {} or ( y <> {} & x <> {} ) ) ; supposeA3: x = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) reconsider y9 = y as Element of RAT+ by A2; take {} ; ::_thesis: ex y9 being Element of RAT+ st ( x = {} & y = y9 & x + y = {} + y9 ) take y9 ; ::_thesis: ( x = {} & y = y9 & x + y = {} + y9 ) thus x = {} by A3; ::_thesis: ( y = y9 & x + y = {} + y9 ) thus y = y9 ; ::_thesis: x + y = {} + y9 thus x + y = y by A3, Def8 .= {} + y9 by ARYTM_3:50 ; ::_thesis: verum end; supposeA4: y = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) reconsider x9 = x as Element of RAT+ by A1; take x9 ; ::_thesis: ex y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) take {} ; ::_thesis: ( x = x9 & y = {} & x + y = x9 + {} ) thus x = x9 ; ::_thesis: ( y = {} & x + y = x9 + {} ) thus y = {} by A4; ::_thesis: x + y = x9 + {} thus x + y = x by A4, Def8 .= x9 + {} by ARYTM_3:50 ; ::_thesis: verum end; supposeA5: ( y <> {} & x <> {} ) ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) set A = DEDEKIND_CUT x; set B = DEDEKIND_CUT y; consider x9 being Element of RAT+ such that A6: x = x9 and A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x9 } by A1, Def3; consider y9 being Element of RAT+ such that A8: y = y9 and A9: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y9 } by A2, Def3; A10: for s being Element of RAT+ holds ( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x9 + y9 ) proof let s2 be Element of RAT+ ; ::_thesis: ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s2 < x9 + y9 ) thus ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) implies s2 < x9 + y9 ) ::_thesis: ( s2 < x9 + y9 implies s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) ) proof assume s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) ; ::_thesis: s2 < x9 + y9 then consider r1, s1 being Element of RAT+ such that A11: s2 = r1 + s1 and A12: r1 in DEDEKIND_CUT x and A13: s1 in DEDEKIND_CUT y ; ex s being Element of RAT+ st ( s = r1 & s < x9 ) by A7, A12; then A14: r1 + s1 <=' x9 + s1 by ARYTM_3:76; ex s being Element of RAT+ st ( s = s1 & s < y9 ) by A9, A13; then x9 + s1 < x9 + y9 by ARYTM_3:76; hence s2 < x9 + y9 by A11, A14, ARYTM_3:69; ::_thesis: verum end; assume s2 < x9 + y9 ; ::_thesis: s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) then consider t2, t0 being Element of RAT+ such that A15: s2 = t2 + t0 and A16: ( t2 < x9 & t0 < y9 ) by A5, A6, A8, Lm46; ( t0 in DEDEKIND_CUT y & t2 in DEDEKIND_CUT x ) by A7, A9, A16; hence s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) by A15; ::_thesis: verum end; then consider r being Element of RAT+ such that A17: GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = r and A18: for s being Element of RAT+ holds ( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < r ) by Def4; A19: for s being Element of RAT+ holds ( s < x9 + y9 iff s < r ) proof let s be Element of RAT+ ; ::_thesis: ( s < x9 + y9 iff s < r ) ( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x9 + y9 ) by A10; hence ( s < x9 + y9 iff s < r ) by A18; ::_thesis: verum end; take x9 ; ::_thesis: ex y9 being Element of RAT+ st ( x = x9 & y = y9 & x + y = x9 + y9 ) take y9 ; ::_thesis: ( x = x9 & y = y9 & x + y = x9 + y9 ) thus ( x = x9 & y = y9 ) by A6, A8; ::_thesis: x + y = x9 + y9 thus x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) by A5, Def8 .= x9 + y9 by A17, A19, Lm6 ; ::_thesis: verum end; end; end; theorem :: ARYTM_2:16 for x, y being Element of REAL+ st x in omega & y in omega holds y + x in omega proof let x, y be Element of REAL+ ; ::_thesis: ( x in omega & y in omega implies y + x in omega ) assume A1: ( x in omega & y in omega ) ; ::_thesis: y + x in omega then reconsider x0 = x, y0 = y as Element of omega ; consider x9, y9 being Element of RAT+ such that A2: ( x = x9 & y = y9 ) and A3: x + y = x9 + y9 by A1, Lm5, Lm47; x9 + y9 = x0 +^ y0 by A2, Lm45; hence y + x in omega by A3, ORDINAL1:def_12; ::_thesis: verum end; theorem :: ARYTM_2:17 for A being Subset of REAL+ st {} in A & ( for x, y being Element of REAL+ st x in A & y = one holds x + y in A ) holds omega c= A proof let A be Subset of REAL+; ::_thesis: ( {} in A & ( for x, y being Element of REAL+ st x in A & y = one holds x + y in A ) implies omega c= A ) defpred S1[ set ] means $1 in A; assume that A1: S1[ {} ] and A2: for x, y being Element of REAL+ st x in A & y = one holds x + y in A ; ::_thesis: omega c= A let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in omega or e in A ) assume e in omega ; ::_thesis: e in A then reconsider a = e as natural Ordinal ; A3: for a being natural Ordinal st S1[a] holds S1[ succ a] proof one in RAT+ ; then reconsider rone = one as Element of REAL+ by Th1; let a be natural Ordinal; ::_thesis: ( S1[a] implies S1[ succ a] ) assume A4: a in A ; ::_thesis: S1[ succ a] reconsider i = a as Element of omega by ORDINAL1:def_12; A5: a in omega by ORDINAL1:def_12; then a in RAT+ by Lm5; then reconsider x = a as Element of REAL+ by Th1; consider x9, y9 being Element of RAT+ such that A6: ( x = x9 & rone = y9 ) and A7: x + rone = x9 + y9 by A5, Lm5, Lm47; x9 + y9 = i +^ 1 by A6, Lm45 .= succ i by ORDINAL2:31 ; hence S1[ succ a] by A2, A4, A7; ::_thesis: verum end; S1[a] from ORDINAL2:sch_17(A1, A3); hence e in A ; ::_thesis: verum end; theorem :: ARYTM_2:18 for x being Element of REAL+ st x in omega holds for y being Element of REAL+ holds ( y in x iff ( y in omega & y <> x & y <=' x ) ) proof let x be Element of REAL+ ; ::_thesis: ( x in omega implies for y being Element of REAL+ holds ( y in x iff ( y in omega & y <> x & y <=' x ) ) ) assume A1: x in omega ; ::_thesis: for y being Element of REAL+ holds ( y in x iff ( y in omega & y <> x & y <=' x ) ) then reconsider m = x as Element of omega ; reconsider x9 = x as Element of RAT+ by A1, Lm5; let y be Element of REAL+ ; ::_thesis: ( y in x iff ( y in omega & y <> x & y <=' x ) ) A2: x c= omega by A1, ORDINAL1:def_2; hereby ::_thesis: ( y in omega & y <> x & y <=' x implies y in x ) assume A3: y in x ; ::_thesis: ( y in omega & y <> x & y <=' x ) then reconsider n = y as Element of omega by A2; thus y in omega by A2, A3; ::_thesis: ( y <> x & y <=' x ) then reconsider y9 = y as Element of RAT+ by Lm5; thus y <> x by A3; ::_thesis: y <=' x n c= m by A3, ORDINAL1:def_2; then consider C being Ordinal such that A4: m = n +^ C by ORDINAL3:27; C c= m by A4, ORDINAL3:24; then reconsider C = C as Element of omega by ORDINAL1:12; C in omega ; then reconsider z9 = C as Element of RAT+ by Lm5; x9 = y9 + z9 by A4, Lm45; then y9 <=' x9 by ARYTM_3:def_13; hence y <=' x by Lm14; ::_thesis: verum end; assume A5: y in omega ; ::_thesis: ( not y <> x or not y <=' x or y in x ) then reconsider y9 = y as Element of RAT+ by Lm5; reconsider n = y as Element of omega by A5; assume A6: y <> x ; ::_thesis: ( not y <=' x or y in x ) assume y <=' x ; ::_thesis: y in x then y9 <=' x9 by Lm14; then consider z9 being Element of RAT+ such that A7: y9 + z9 = x9 by ARYTM_3:def_13; reconsider k = z9 as Element of omega by A1, A5, A7, ARYTM_3:71; n +^ k = m by A7, Lm45; then n c= m by ORDINAL3:24; then n c< m by A6, XBOOLE_0:def_8; hence y in x by ORDINAL1:11; ::_thesis: verum end; theorem :: ARYTM_2:19 for x, y, z being Element of REAL+ st x = y + z holds z <=' x proof let x, y, z be Element of REAL+ ; ::_thesis: ( x = y + z implies z <=' x ) {} in RAT+ ; then reconsider zz = {} as Element of REAL+ by Th1; assume A1: x = y + z ; ::_thesis: z <=' x assume A2: not z <=' x ; ::_thesis: contradiction then consider y0 being Element of REAL+ such that A3: x + y0 = z by Th9; x = x + (y + y0) by A1, A3, Th6; then x + zz = x + (y + y0) by Def8; then y0 = {} by Th5, Th11; then z = x by A3, Def8; hence contradiction by A2; ::_thesis: verum end; theorem :: ARYTM_2:20 ( {} in REAL+ & one in REAL+ ) proof ( {} in RAT+ & one in RAT+ ) ; hence ( {} in REAL+ & one in REAL+ ) by Th1; ::_thesis: verum end; theorem :: ARYTM_2:21 for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) proof let x, y be Element of REAL+ ; ::_thesis: ( x in RAT+ & y in RAT+ implies ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) ) assume that A1: x in RAT+ and A2: y in RAT+ ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) percases ( x = {} or y = {} or ( y <> {} & x <> {} ) ) ; supposeA3: x = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) reconsider y9 = y as Element of RAT+ by A2; take {} ; ::_thesis: ex y9 being Element of RAT+ st ( x = {} & y = y9 & x *' y = {} *' y9 ) take y9 ; ::_thesis: ( x = {} & y = y9 & x *' y = {} *' y9 ) thus x = {} by A3; ::_thesis: ( y = y9 & x *' y = {} *' y9 ) thus y = y9 ; ::_thesis: x *' y = {} *' y9 thus x *' y = {} by A3, Th4 .= {} *' y9 by ARYTM_3:48 ; ::_thesis: verum end; supposeA4: y = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) reconsider x9 = x as Element of RAT+ by A1; take x9 ; ::_thesis: ex y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) take {} ; ::_thesis: ( x = x9 & y = {} & x *' y = x9 *' {} ) thus x = x9 ; ::_thesis: ( y = {} & x *' y = x9 *' {} ) thus y = {} by A4; ::_thesis: x *' y = x9 *' {} thus x *' y = {} by A4, Th4 .= x9 *' {} by ARYTM_3:48 ; ::_thesis: verum end; supposethat y <> {} and A5: x <> {} ; ::_thesis: ex x9, y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) consider y9 being Element of RAT+ such that A6: y = y9 and A7: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y9 } by A2, Def3; set A = DEDEKIND_CUT x; set B = DEDEKIND_CUT y; consider x9 being Element of RAT+ such that A8: x = x9 and A9: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x9 } by A1, Def3; A10: for s being Element of RAT+ holds ( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < x9 *' y9 ) proof let s2 be Element of RAT+ ; ::_thesis: ( s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s2 < x9 *' y9 ) thus ( s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) implies s2 < x9 *' y9 ) ::_thesis: ( s2 < x9 *' y9 implies s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) ) proof assume s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) ; ::_thesis: s2 < x9 *' y9 then consider r1, s1 being Element of RAT+ such that A11: s2 = r1 *' s1 and A12: r1 in DEDEKIND_CUT x and A13: s1 in DEDEKIND_CUT y ; ex s being Element of RAT+ st ( s = r1 & s < x9 ) by A9, A12; then A14: r1 *' s1 <=' x9 *' s1 by ARYTM_3:82; A15: ex s being Element of RAT+ st ( s = s1 & s < y9 ) by A7, A13; then s1 <> y9 ; then A16: x9 *' s1 <> x9 *' y9 by A5, A8, ARYTM_3:56; x9 *' s1 <=' x9 *' y9 by A15, ARYTM_3:82; then x9 *' s1 < x9 *' y9 by A16, ARYTM_3:68; hence s2 < x9 *' y9 by A11, A14, ARYTM_3:69; ::_thesis: verum end; assume A17: s2 < x9 *' y9 ; ::_thesis: s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) then consider t0 being Element of RAT+ such that A18: s2 = x9 *' t0 and A19: t0 <=' y9 by ARYTM_3:79; t0 <> y9 by A17, A18; then t0 < y9 by A19, ARYTM_3:68; then consider t1 being Element of RAT+ such that A20: t0 < t1 and A21: t1 < y9 by ARYTM_3:93; s2 <=' t1 *' x9 by A18, A20, ARYTM_3:82; then consider t2 being Element of RAT+ such that A22: s2 = t1 *' t2 and A23: t2 <=' x9 by ARYTM_3:79; now__::_thesis:_not_t2_=_x9 assume t2 = x9 ; ::_thesis: contradiction then t0 = t1 by A5, A8, A18, A22, ARYTM_3:56; hence contradiction by A20; ::_thesis: verum end; then t2 < x9 by A23, ARYTM_3:68; then A24: t2 in DEDEKIND_CUT x by A9; t1 in DEDEKIND_CUT y by A7, A21; hence s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) by A22, A24; ::_thesis: verum end; then consider r being Element of RAT+ such that A25: GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) = r and A26: for s being Element of RAT+ holds ( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < r ) by Def4; take x9 ; ::_thesis: ex y9 being Element of RAT+ st ( x = x9 & y = y9 & x *' y = x9 *' y9 ) take y9 ; ::_thesis: ( x = x9 & y = y9 & x *' y = x9 *' y9 ) thus ( x = x9 & y = y9 ) by A8, A6; ::_thesis: x *' y = x9 *' y9 for s being Element of RAT+ holds ( s < x9 *' y9 iff s < r ) proof let s be Element of RAT+ ; ::_thesis: ( s < x9 *' y9 iff s < r ) ( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < x9 *' y9 ) by A10; hence ( s < x9 *' y9 iff s < r ) by A26; ::_thesis: verum end; hence x *' y = x9 *' y9 by A25, Lm6; ::_thesis: verum end; end; end;