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