:: AXIOMS semantic presentation
E1:
for b1, b2 being real number holds
( b1 <= b2 implies ( not ( b1 in REAL+ & b2 in REAL+ & ( for b3, b4 being Element of REAL+ holds
not ( b1 = b3 & b2 = b4 & b3 <=' b4 ) ) ) & not ( b1 in [:{0},REAL+ :] & b2 in [:{0},REAL+ :] & ( for b3, b4 being Element of REAL+ holds
not ( b1 = [0,b3] & b2 = [0,b4] & b4 <=' b3 ) ) ) & ( ( ) implies ( ( b1 in REAL+ & b2 in REAL+ ) or ( b1 in [:{0},REAL+ :] & b2 in [:{0},REAL+ :] ) or ( b2 in REAL+ & b1 in [:{0},REAL+ :] ) ) ) ) )
by XXREAL_0:def 5;
E2:
for b1, b2 being real number holds
( not ( not ( b1 in REAL+ & b2 in REAL+ & ex b3, b4 being Element of REAL+ st
( b1 = b3 & b2 = b4 & b3 <=' b4 ) ) & not ( b1 in [:{0},REAL+ :] & b2 in [:{0},REAL+ :] & ex b3, b4 being Element of REAL+ st
( b1 = [0,b3] & b2 = [0,b4] & b4 <=' b3 ) ) & not ( b2 in REAL+ & b1 in [:{0},REAL+ :] ) ) implies b1 <= b2 )
theorem :: AXIOMS:1
canceled;
theorem :: AXIOMS:2
canceled;
theorem :: AXIOMS:3
canceled;
theorem :: AXIOMS:4
canceled;
theorem :: AXIOMS:5
canceled;
theorem :: AXIOMS:6
canceled;
theorem :: AXIOMS:7
canceled;
theorem :: AXIOMS:8
canceled;
theorem :: AXIOMS:9
canceled;
theorem :: AXIOMS:10
canceled;
theorem :: AXIOMS:11
canceled;
theorem :: AXIOMS:12
canceled;
theorem :: AXIOMS:13
canceled;
theorem :: AXIOMS:14
canceled;
theorem :: AXIOMS:15
canceled;
theorem :: AXIOMS:16
canceled;
theorem :: AXIOMS:17
canceled;
theorem :: AXIOMS:18
canceled;
theorem :: AXIOMS:19
theorem :: AXIOMS:20
E3:
for b1, b2 being real number holds
( ( b1 <= b2 & b2 <= b1 ) implies ( b1 = b2 ) )
by XXREAL_0:1;
E4:
for b1 being real number
for b2, b3 being Element of REAL holds
( b1 = [*b2,b3*] implies ( b3 = 0 & b1 = b2 ) )
E5:
for b1, b2 being Element of REAL
for b3, b4 being real number holds
( ( b1 = b3 & b2 = b4 ) implies ( + b1,b2 = b3 + b4 ) )
proof
let c
1, c
2 be
Element of
REAL ;
let c
3, c
4 be
real number ;
assume E6:
( c
1 = c
3 & c
2 = c
4 )
;
consider c
5, c
6, c
7, c
8 being
Element of
REAL such that E7:
c
3 = [*c5,c6*]
and E8:
c
4 = [*c7,c8*]
and E9:
c
3 + c
4 = [*(+ c5,c7),(+ c6,c8)*]
by XCMPLX_0:def 4;
E10:
( c
3 = c
5 & c
4 = c
7 )
by E7, E8, E4;
( c
6 = 0 & c
8 = 0 )
by E7, E8, E4;
then
+ c
6,c
8 = 0
by ARYTM_0:13;
hence
+ c
1,c
2 = c
3 + c
4
by E6, E9, E10, ARYTM_0:def 7;
end;
E6:
{} in {{} }
by TARSKI:def 1;
reconsider c1 = 0 as Element of REAL+ by ARYTM_2:21;
theorem :: AXIOMS:21
canceled;
theorem :: AXIOMS:22
canceled;
theorem :: AXIOMS:23
canceled;
theorem :: AXIOMS:24
canceled;
theorem :: AXIOMS:25
canceled;
theorem :: AXIOMS:26
proof
let c
2, c
3 be
Subset of
REAL ;
assume E7:
for b
1, b
2 being
real number holds
( ( b
1 in c
2 & b
2 in c
3 ) implies ( b
1 <= b
2 ) )
;
per cases
not ( not c
2 = 0 & not c
3 = 0 & not ( c
2 <> 0 & c
3 <> 0 ) )
;
suppose E8:
( c
2 = 0 or c
3 = 0 )
;
take
1
;
thus
for b
1, b
2 being
real number holds
( ( b
1 in c
2 & b
2 in c
3 ) implies ( ( b
1 <= 1 & 1
<= b
2 ) ) )
by E8;
end;
suppose that E8:
c
2 <> 0
and E9:
c
3 <> 0
;
consider c
4 being
Element of
REAL such that E10:
c
4 in c
2
by E8, SUBSET_1:10;
consider c
5 being
Element of
REAL such that E11:
c
5 in c
3
by E9, SUBSET_1:10;
E12:
REAL c= REAL+ \/ [:{0},REAL+ :]
by NUMBERS:def 1, XBOOLE_1:36;
then E13:
c
2 c= REAL+ \/ [:{0},REAL+ :]
by XBOOLE_1:1;
E14:
c
3 c= REAL+ \/ [:{0},REAL+ :]
by E12, XBOOLE_1:1;
thus
ex b
1 being
real number st
for b
2, b
3 being
real number holds
( ( b
2 in c
2 & b
3 in c
3 ) implies ( ( b
2 <= b
1 & b
1 <= b
3 ) ) )
proof
per cases
not ( not ( c
2 misses REAL+ & c
3 misses [:{0},REAL+ :] ) & not c
3 meets [:{0},REAL+ :] & not c
2 meets REAL+ )
;
suppose
c
3 meets [:{0},REAL+ :]
;
then consider c
6 being
set such that E15:
c
6 in c
3
and E16:
c
6 in [:{0},REAL+ :]
by XBOOLE_0:3;
consider c
7, c
8 being
set such that E17:
c
7 in {0}
and E18:
c
8 in REAL+
and E19:
c
6 = [c7,c8]
by E16, ZFMISC_1:103;
reconsider c
9 = c
8 as
Element of
REAL+ by E18;
c
6 in REAL
by E15;
then E20:
[0,c9] in REAL
by E17, E19, TARSKI:def 1;
then reconsider c
10 =
[0,c9] as
real number by XREAL_0:def 1;
{ b1 where B is Element of REAL+ : [0,b1] in c3 } c= REAL+
then reconsider c
11 =
{ b1 where B is Element of REAL+ : [0,b1] in c3 } as
Subset of
REAL+ ;
E21:
c
10 in [:{0},REAL+ :]
by E6, ZFMISC_1:106;
E22:
c
10 in c
3
by E15, E17, E19, TARSKI:def 1;
then E23:
c
9 in c
11
;
E24:
c
2 c= [:{0},REAL+ :]
then consider c
12, c
13 being
set such that E25:
c
12 in {0}
and E26:
c
13 in REAL+
and E27:
c
4 = [c12,c13]
by E10, ZFMISC_1:103;
reconsider c
14 = c
13 as
Element of
REAL+ by E26;
E28:
c
4 = [0,c14]
by E25, E27, TARSKI:def 1;
{ b1 where B is Element of REAL+ : [0,b1] in c2 } c= REAL+
then reconsider c
15 =
{ b1 where B is Element of REAL+ : [0,b1] in c2 } as
Subset of
REAL+ ;
E29:
c
14 in c
15
by E10, E28;
for b
1, b
2 being
Element of
REAL+ holds
( ( b
1 in c
11 & b
2 in c
15 ) implies ( b
1 <=' b
2 ) )
proof
let c
16, c
17 be
Element of
REAL+ ;
assume
c
16 in c
11
;
then consider c
18 being
Element of
REAL+ such that E30:
c
16 = c
18
and E31:
[0,c18] in c
3
;
assume
c
17 in c
15
;
then consider c
19 being
Element of
REAL+ such that E32:
c
17 = c
19
and E33:
[0,c19] in c
2
;
reconsider c
20 =
[0,c17], c
21 =
[0,c16] as
real number by E30, E31, E32, E33, XREAL_0:def 1;
E34:
( c
20 in [:{0},REAL+ :] & c
21 in [:{0},REAL+ :] )
by E6, ZFMISC_1:106;
c
20 <= c
21
by E7, E30, E31, E32, E33;
then consider c
22, c
23 being
Element of
REAL+ such that E35:
c
20 = [0,c22]
and E36:
c
21 = [0,c23]
and E37:
c
23 <=' c
22
by E34, E1;
( c
17 = c
22 & c
16 = c
23 )
by E35, E36, ZFMISC_1:33;
hence
c
16 <=' c
17
by E37;
end;
then consider c
16 being
Element of
REAL+ such that E30:
for b
1, b
2 being
Element of
REAL+ holds
( ( b
1 in c
11 & b
2 in c
15 ) implies ( ( b
1 <=' c
16 & c
16 <=' b
2 ) ) )
by E23, E29, ARYTM_2:9;
E31:
c
9 <> 0
by E20, ARYTM_0:3;
c
9 <=' c
16
by E23, E29, E30;
then
c
16 <> 0
by E31, ARYTM_1:5;
then
[0,c16] in REAL
by ARYTM_0:2;
then reconsider c
17 =
[0,c16] as
real number by XREAL_0:def 1;
take
c
17
;
E32:
c
17 in [:{0},REAL+ :]
by E6, ZFMISC_1:106;
let c
18, c
19 be
real number ;
assume that E33:
c
18 in c
2
and E34:
c
19 in c
3
;
consider c
20, c
21 being
set such that E35:
c
20 in {0}
and E36:
c
21 in REAL+
and E37:
c
18 = [c20,c21]
by E24, E33, ZFMISC_1:103;
reconsider c
22 = c
21 as
Element of
REAL+ by E36;
E38:
c
18 = [0,c22]
by E35, E37, TARSKI:def 1;
then E39:
c
22 in c
15
by E33;
now
per cases
( c
19 in REAL+ or c
19 in [:{0},REAL+ :] )
by E14, E34, XBOOLE_0:def 2;
suppose E40:
c
19 in REAL+
;
( c
9 <=' c
16 & c
16 <=' c
22 )
by E23, E30, E39;
hence
c
18 <= c
17
by E24, E32, E33, E38, E2;
( not c
17 in REAL+ & not c
19 in [:{0},REAL+ :] )
by E32, E40, ARYTM_0:5, XBOOLE_0:3;
hence
c
17 <= c
19
by E1;
suppose E40:
c
19 in [:{0},REAL+ :]
;
then consider c
23, c
24 being
set such that E41:
c
23 in {0}
and E42:
c
24 in REAL+
and E43:
c
19 = [c23,c24]
by ZFMISC_1:103;
reconsider c
25 = c
24 as
Element of
REAL+ by E42;
E44:
c
19 = [0,c25]
by E41, E43, TARSKI:def 1;
then
c
25 in c
11
by E34;
then
( c
25 <=' c
16 & c
16 <=' c
22 )
by E30, E39;
hence
( c
18 <= c
17 & c
17 <= c
19 )
by E24, E32, E33, E38, E40, E44, E2;
end;
end;
hence
( c
18 <= c
17 & c
17 <= c
19 )
;
end;
end;
end;
end;
end;
end;
theorem :: AXIOMS:27
canceled;
theorem :: AXIOMS:28
E7: one =
succ 0
by ORDINAL2:def 4
.=
1
;
theorem :: AXIOMS:29
proof
let c
2 be
Subset of
REAL ;
assume that E8:
0
in c
2
and E9:
for b
1 being
real number holds
( b
1 in c
2 implies b
1 + 1
in c
2 )
;
reconsider c
3 = c
2 /\ REAL+ as
Subset of
REAL+ by XBOOLE_1:17;
E10:
0
in c
3
by E8, ARYTM_2:21, XBOOLE_0:def 3;
E11:
c
3 c= c
2
by XBOOLE_1:17;
for b
1, b
2 being
Element of
REAL+ holds
( ( b
1 in c
3 & b
2 = 1 ) implies ( b
1 + b
2 in c
3 ) )
proof
let c
4, c
5 be
Element of
REAL+ ;
assume that E12:
c
4 in c
3
and E13:
c
5 = 1
;
c
4 in REAL+
;
then reconsider c
6 = c
4 as
Element of
REAL by ARYTM_0:1;
reconsider c
7 = c
6 as
real number by XREAL_0:def 1;
consider c
8, c
9 being
Element of
REAL+ such that E14:
c
6 = c
8
and E15:
1
= c
9
and E16:
+ c
6,1
= c
8 + c
9
by E7, ARYTM_0:def 2, ARYTM_2:21;
c
7 + 1
in c
2
by E9, E11, E12;
then
+ c
6,1
in c
2
by E5;
hence
c
4 + c
5 in c
3
by E13, E14, E15, E16, XBOOLE_0:def 3;
end;
then
NAT c= c
3
by E10, E7, ARYTM_2:18;
hence
NAT c= c
2
by E11, XBOOLE_1:1;
end;
theorem :: AXIOMS:30