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