:: AXIOMS semantic presentation begin Lm1: for r, s being real number st ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st ( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) holds r <= s proof let r, s be real number ; ::_thesis: ( ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st ( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) implies r <= s ) assume A1: ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st ( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) ; ::_thesis: r <= s percases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) or ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ) ; :: according to XXREAL_0:def_5 case ( r in REAL+ & s in REAL+ ) ; ::_thesis: ex b1, b2 being Element of REAL+ st ( r = b1 & s = b2 & b1 <=' b2 ) hence ex b1, b2 being Element of REAL+ st ( r = b1 & s = b2 & b1 <=' b2 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum end; case ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ; ::_thesis: ex b1, b2 being Element of REAL+ st ( r = [0,b1] & s = [0,b2] & b2 <=' b1 ) hence ex b1, b2 being Element of REAL+ st ( r = [0,b1] & s = [0,b2] & b2 <=' b1 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum end; case ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ; ::_thesis: ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty ) hence ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty ) by A1; ::_thesis: verum end; end; end; Lm2: for x being real number for x1, x2 being Element of REAL st x = [*x1,x2*] holds ( x2 = 0 & x = x1 ) proof let x be real number ; ::_thesis: for x1, x2 being Element of REAL st x = [*x1,x2*] holds ( x2 = 0 & x = x1 ) let x1, x2 be Element of REAL ; ::_thesis: ( x = [*x1,x2*] implies ( x2 = 0 & x = x1 ) ) assume A1: x = [*x1,x2*] ; ::_thesis: ( x2 = 0 & x = x1 ) A2: x in REAL by XREAL_0:def_1; hereby ::_thesis: x = x1 assume x2 <> 0 ; ::_thesis: contradiction then x = (0,1) --> (x1,x2) by A1, ARYTM_0:def_5; hence contradiction by A2, ARYTM_0:8; ::_thesis: verum end; hence x = x1 by A1, ARYTM_0:def_5; ::_thesis: verum end; Lm3: for x9, y9 being Element of REAL for x, y being real number st x9 = x & y9 = y holds + (x9,y9) = x + y proof let x9, y9 be Element of REAL ; ::_thesis: for x, y being real number st x9 = x & y9 = y holds + (x9,y9) = x + y let x, y be real number ; ::_thesis: ( x9 = x & y9 = y implies + (x9,y9) = x + y ) assume A1: ( x9 = x & y9 = y ) ; ::_thesis: + (x9,y9) = x + y consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4; ( x2 = 0 & y2 = 0 ) by A2, Lm2; then A4: + (x2,y2) = 0 by ARYTM_0:11; ( x = x1 & y = y1 ) by A2, Lm2; hence + (x9,y9) = x + y by A1, A3, A4, ARYTM_0:def_5; ::_thesis: verum end; Lm4: {} in {{}} by TARSKI:def_1; reconsider o = 0 as Element of REAL+ by ARYTM_2:20; theorem :: AXIOMS:1 for X, Y being Subset of REAL st ( for x, y being real number st x in X & y in Y holds x <= y ) holds ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) proof let X, Y be Subset of REAL; ::_thesis: ( ( for x, y being real number st x in X & y in Y holds x <= y ) implies ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) ) assume A1: for x, y being real number st x in X & y in Y holds x <= y ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) percases ( X = 0 or Y = 0 or ( X <> 0 & Y <> 0 ) ) ; supposeA2: ( X = 0 or Y = 0 ) ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) take 1 ; ::_thesis: for x, y being real number st x in X & y in Y holds ( x <= 1 & 1 <= y ) thus for x, y being real number st x in X & y in Y holds ( x <= 1 & 1 <= y ) by A2; ::_thesis: verum end; supposethat A3: X <> 0 and A4: Y <> 0 ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) consider x1 being Element of REAL such that A5: x1 in X by A3, SUBSET_1:4; A6: X c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_1:1; A7: Y c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_1:1; A8: ex x2 being Element of REAL st x2 in Y by A4, SUBSET_1:4; thus ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) ::_thesis: verum proof percases ( ( X misses REAL+ & Y misses [:{0},REAL+:] ) or Y meets [:{0},REAL+:] or X meets REAL+ ) ; supposethat A9: X misses REAL+ and A10: Y misses [:{0},REAL+:] ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) take z = 0 ; ::_thesis: for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) let x, y be real number ; ::_thesis: ( x in X & y in Y implies ( x <= z & z <= y ) ) assume that A11: x in X and A12: y in Y ; ::_thesis: ( x <= z & z <= y ) ( not z in [:{0},REAL+:] & not x in REAL+ ) by A9, A11, ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3; hence x <= z by XXREAL_0:def_5; ::_thesis: z <= y Y c= REAL+ by A7, A10, XBOOLE_1:73; then reconsider y9 = y as Element of REAL+ by A12; o <=' y9 by ARYTM_1:6; hence z <= y by Lm1; ::_thesis: verum end; supposeA13: Y meets [:{0},REAL+:] ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) { r where r is Element of REAL+ : [0,r] in X } c= REAL+ proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { r where r is Element of REAL+ : [0,r] in X } or u in REAL+ ) assume u in { r where r is Element of REAL+ : [0,r] in X } ; ::_thesis: u in REAL+ then ex r being Element of REAL+ st ( u = r & [0,r] in X ) ; hence u in REAL+ ; ::_thesis: verum end; then reconsider X9 = { r where r is Element of REAL+ : [0,r] in X } as Subset of REAL+ ; { r where r is Element of REAL+ : [0,r] in Y } c= REAL+ proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { r where r is Element of REAL+ : [0,r] in Y } or u in REAL+ ) assume u in { r where r is Element of REAL+ : [0,r] in Y } ; ::_thesis: u in REAL+ then ex r being Element of REAL+ st ( u = r & [0,r] in Y ) ; hence u in REAL+ ; ::_thesis: verum end; then reconsider Y9 = { r where r is Element of REAL+ : [0,r] in Y } as Subset of REAL+ ; consider e being set such that A14: e in Y and A15: e in [:{0},REAL+:] by A13, XBOOLE_0:3; consider u, y1 being set such that A16: u in {0} and A17: y1 in REAL+ and A18: e = [u,y1] by A15, ZFMISC_1:84; reconsider y1 = y1 as Element of REAL+ by A17; e in REAL by A14; then A19: [0,y1] in REAL by A16, A18, TARSKI:def_1; then reconsider y0 = [0,y1] as real number ; A20: y0 in Y by A14, A16, A18, TARSKI:def_1; then A21: y1 in Y9 ; A22: y0 in [:{0},REAL+:] by Lm4, ZFMISC_1:87; A23: X c= [:{0},REAL+:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in X or u in [:{0},REAL+:] ) assume A24: u in X ; ::_thesis: u in [:{0},REAL+:] then reconsider x = u as real number ; now__::_thesis:_not_x_in_REAL+ assume x in REAL+ ; ::_thesis: contradiction then A25: not x in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3; ( x <= y0 & not y0 in REAL+ ) by A1, A22, A20, A24, ARYTM_0:5, XBOOLE_0:3; hence contradiction by A25, XXREAL_0:def_5; ::_thesis: verum end; hence u in [:{0},REAL+:] by A6, A24, XBOOLE_0:def_3; ::_thesis: verum end; then consider e, x3 being set such that A26: e in {0} and A27: x3 in REAL+ and A28: x1 = [e,x3] by A5, ZFMISC_1:84; reconsider x3 = x3 as Element of REAL+ by A27; x1 = [0,x3] by A26, A28, TARSKI:def_1; then A29: x3 in X9 by A5; for y9, x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds y9 <=' x9 proof let y9, x9 be Element of REAL+ ; ::_thesis: ( y9 in Y9 & x9 in X9 implies y9 <=' x9 ) assume y9 in Y9 ; ::_thesis: ( not x9 in X9 or y9 <=' x9 ) then A30: ex r1 being Element of REAL+ st ( y9 = r1 & [0,r1] in Y ) ; assume x9 in X9 ; ::_thesis: y9 <=' x9 then A31: ex r2 being Element of REAL+ st ( x9 = r2 & [0,r2] in X ) ; then reconsider x = [0,x9], y = [0,y9] as real number by A30; A32: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) by Lm4, ZFMISC_1:87; x <= y by A1, A30, A31; then consider x99, y99 being Element of REAL+ such that A33: x = [0,x99] and A34: ( y = [0,y99] & y99 <=' x99 ) by A32, XXREAL_0:def_5; x9 = x99 by A33, XTUPLE_0:1; hence y9 <=' x9 by A34, XTUPLE_0:1; ::_thesis: verum end; then consider z9 being Element of REAL+ such that A35: for y9, x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds ( y9 <=' z9 & z9 <=' x9 ) by A29, ARYTM_2:8; A36: y1 <> 0 by A19, ARYTM_0:3; y1 <=' z9 by A21, A29, A35; then [0,z9] in REAL by A36, ARYTM_0:2, ARYTM_1:5; then reconsider z = [0,z9] as real number ; take z ; ::_thesis: for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) let x, y be real number ; ::_thesis: ( x in X & y in Y implies ( x <= z & z <= y ) ) assume that A37: x in X and A38: y in Y ; ::_thesis: ( x <= z & z <= y ) consider e, x9 being set such that A39: e in {0} and A40: x9 in REAL+ and A41: x = [e,x9] by A23, A37, ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A40; A42: z in [:{0},REAL+:] by Lm4, ZFMISC_1:87; A43: x = [0,x9] by A39, A41, TARSKI:def_1; then A44: x9 in X9 by A37; now__::_thesis:_(_x_<=_z_&_z_<=_y_) percases ( y in REAL+ or y in [:{0},REAL+:] ) by A7, A38, XBOOLE_0:def_3; supposeA45: y in REAL+ ; ::_thesis: ( x <= z & z <= y ) z9 <=' x9 by A21, A35, A44; hence x <= z by A23, A42, A37, A43, Lm1; ::_thesis: z <= y A46: not y in [:{0},REAL+:] by A45, ARYTM_0:5, XBOOLE_0:3; not z in REAL+ by A42, ARYTM_0:5, XBOOLE_0:3; hence z <= y by A46, XXREAL_0:def_5; ::_thesis: verum end; supposeA47: y in [:{0},REAL+:] ; ::_thesis: ( x <= z & z <= y ) then consider e, y9 being set such that A48: e in {0} and A49: y9 in REAL+ and A50: y = [e,y9] by ZFMISC_1:84; reconsider y9 = y9 as Element of REAL+ by A49; A51: y = [0,y9] by A48, A50, TARSKI:def_1; then y9 in Y9 by A38; then ( y9 <=' z9 & z9 <=' x9 ) by A35, A44; hence ( x <= z & z <= y ) by A23, A42, A37, A43, A47, A51, Lm1; ::_thesis: verum end; end; end; hence ( x <= z & z <= y ) ; ::_thesis: verum end; supposeA52: X meets REAL+ ; ::_thesis: ex z being real number st for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) reconsider X9 = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17; consider x1 being set such that A53: x1 in X and A54: x1 in REAL+ by A52, XBOOLE_0:3; reconsider x1 = x1 as Element of REAL+ by A54; x1 in REAL+ ; then reconsider x0 = x1 as real number by ARYTM_0:1; A55: Y c= REAL+ proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Y or u in REAL+ ) assume A56: u in Y ; ::_thesis: u in REAL+ then reconsider y = u as real number ; now__::_thesis:_not_y_in_[:{0},REAL+:] assume y in [:{0},REAL+:] ; ::_thesis: contradiction then A57: not y in REAL+ by ARYTM_0:5, XBOOLE_0:3; ( x0 <= y & not x0 in [:{0},REAL+:] ) by A1, A53, A56, ARYTM_0:5, XBOOLE_0:3; hence contradiction by A57, XXREAL_0:def_5; ::_thesis: verum end; hence u in REAL+ by A7, A56, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider Y9 = Y as Subset of REAL+ ; for x9, y9 being Element of REAL+ st x9 in X9 & y9 in Y9 holds x9 <=' y9 proof let x9, y9 be Element of REAL+ ; ::_thesis: ( x9 in X9 & y9 in Y9 implies x9 <=' y9 ) A58: X9 c= X by XBOOLE_1:17; ( x9 in REAL+ & y9 in REAL+ ) ; then reconsider x = x9, y = y9 as real number by ARYTM_0:1; assume ( x9 in X9 & y9 in Y9 ) ; ::_thesis: x9 <=' y9 then x <= y by A1, A58; then ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & x9 <=' y9 ) by XXREAL_0:def_5; hence x9 <=' y9 ; ::_thesis: verum end; then consider z9 being Element of REAL+ such that A59: for x9, y9 being Element of REAL+ st x9 in X9 & y9 in Y9 holds ( x9 <=' z9 & z9 <=' y9 ) by A8, ARYTM_2:8; z9 in REAL+ ; then reconsider z = z9 as real number by ARYTM_0:1; take z ; ::_thesis: for x, y being real number st x in X & y in Y holds ( x <= z & z <= y ) let x, y be real number ; ::_thesis: ( x in X & y in Y implies ( x <= z & z <= y ) ) assume that A60: x in X and A61: y in Y ; ::_thesis: ( x <= z & z <= y ) reconsider y9 = y as Element of REAL+ by A55, A61; A62: x0 in X9 by A53, XBOOLE_0:def_4; now__::_thesis:_(_x_<=_z_&_z_<=_y_) percases ( x in REAL+ or x in [:{0},REAL+:] ) by A6, A60, XBOOLE_0:def_3; suppose x in REAL+ ; ::_thesis: ( x <= z & z <= y ) then reconsider x9 = x as Element of REAL+ ; x9 in X9 by A60, XBOOLE_0:def_4; then ( x9 <=' z9 & z9 <=' y9 ) by A59, A61; hence ( x <= z & z <= y ) by Lm1; ::_thesis: verum end; supposeA63: x in [:{0},REAL+:] ; ::_thesis: ( x <= z & z <= y ) A64: not z in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3; not x in REAL+ by A63, ARYTM_0:5, XBOOLE_0:3; hence x <= z by A64, XXREAL_0:def_5; ::_thesis: z <= y z9 <=' y9 by A62, A59, A61; hence z <= y by Lm1; ::_thesis: verum end; end; end; hence ( x <= z & z <= y ) ; ::_thesis: verum end; end; end; end; end; end; theorem :: AXIOMS:2 for x, y being real number st x in NAT & y in NAT holds x + y in NAT proof let x, y be real number ; ::_thesis: ( x in NAT & y in NAT implies x + y in NAT ) reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def_1; A1: + (x1,y1) = x + y by Lm3; assume A2: ( x in NAT & y in NAT ) ; ::_thesis: x + y in NAT then ex x9, y9 being Element of REAL+ st ( x1 = x9 & y1 = y9 & + (x1,y1) = x9 + y9 ) by ARYTM_0:def_1, ARYTM_2:2; hence x + y in NAT by A1, A2, ARYTM_2:16; ::_thesis: verum end; theorem :: AXIOMS:3 for A being Subset of REAL st 0 in A & ( for x being real number st x in A holds x + 1 in A ) holds NAT c= A proof let A be Subset of REAL; ::_thesis: ( 0 in A & ( for x being real number st x in A holds x + 1 in A ) implies NAT c= A ) assume that A1: 0 in A and A2: for x being real number st x in A holds x + 1 in A ; ::_thesis: NAT c= A reconsider B = A /\ REAL+ as Subset of REAL+ by XBOOLE_1:17; A3: B c= A by XBOOLE_1:17; A4: for x9, y9 being Element of REAL+ st x9 in B & y9 = 1 holds x9 + y9 in B proof let x9, y9 be Element of REAL+ ; ::_thesis: ( x9 in B & y9 = 1 implies x9 + y9 in B ) assume that A5: x9 in B and A6: y9 = 1 ; ::_thesis: x9 + y9 in B x9 in REAL+ ; then reconsider x = x9 as Element of REAL by ARYTM_0:1; reconsider xx = x as real number ; xx + 1 in A by A2, A3, A5; then ( ex x99, y99 being Element of REAL+ st ( x = x99 & 1 = y99 & + (x,1) = x99 + y99 ) & + (x,1) in A ) by Lm3, ARYTM_0:def_1, ARYTM_2:20; hence x9 + y9 in B by A6, XBOOLE_0:def_4; ::_thesis: verum end; 0 in B by A1, ARYTM_2:20, XBOOLE_0:def_4; then NAT c= B by A4, ARYTM_2:17; hence NAT c= A by A3, XBOOLE_1:1; ::_thesis: verum end; theorem :: AXIOMS:4 for k being Nat holds k = { i where i is Element of NAT : i < k } proof let k be Nat; ::_thesis: k = { i where i is Element of NAT : i < k } A1: k in NAT by ORDINAL1:def_12; thus k c= { i where i is Element of NAT : i < k } :: according to XBOOLE_0:def_10 ::_thesis: { i where i is Element of NAT : i < k } c= k proof reconsider k9 = k as Element of NAT by ORDINAL1:def_12; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k or e in { i where i is Element of NAT : i < k } ) assume A2: e in k ; ::_thesis: e in { i where i is Element of NAT : i < k } A3: k9 c= NAT by ORDINAL1:def_2; then reconsider j = e as Element of NAT by A2; e in NAT by A3, A2; then reconsider y9 = e as Element of REAL+ by ARYTM_2:2; k9 in NAT ; then reconsider x9 = k9 as Element of REAL+ by ARYTM_2:2; y9 <=' x9 by A2, ARYTM_2:18; then A4: j <= k by Lm1; y9 <> x9 by A2; then j < k by A4, XXREAL_0:1; hence e in { i where i is Element of NAT : i < k } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { i where i is Element of NAT : i < k } or e in k ) assume e in { i where i is Element of NAT : i < k } ; ::_thesis: e in k then consider i being Element of NAT such that A5: e = i and A6: not k <= i ; i in NAT ; then reconsider x9 = e, y9 = k as Element of REAL+ by A5, A1, ARYTM_2:2; not y9 <=' x9 by A5, A6, Lm1; hence e in k by A5, A6, A1, ARYTM_2:18; ::_thesis: verum end;