THEOREM
*******
Suppose s is a non-empty subset of the reals that is bounded from above, and that lub is the least upper bound of s. Then we have:
ALL(a):[a e r => [a<lub => EXIST(b):[b e s & [a<b & b<=lub]]]]]]
where r is the set of real numbers.
OUTLINE
*******
Line No. Description
1-4 Properties of < and <= on r
5 Suppose s is a non-empty subset of r that is bounded from above
9 Suppose lub is the least upper bound of s
13 Suppose x e r
14 Suppose x < lub
17-22 Case 1: Prove lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
23-65 Case 2: Prove ~lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
This formal proof was written and machine-verified with the aid the author's DC Proof 2.0 software available at http://www.dcproof.com
PROPERTIES OF < AND <= ON R
***************************
1 ALL(a):[a e r => a<=a]
Axiom
2 ALL(a):ALL(b):[a e r & b e r => [~a<b => b<=a]]
Axiom
3 ALL(a):ALL(b):[a e r & b e r => [~a<=b => b<a]]
Axiom
4 ALL(a):ALL(b):[a e r & b e r => [a<=b => ~b<a]]
Axiom
PROOF
*****
Suppose s is a non-empty subset of the reals that is bounded from above
5 ALL(a):[a e s => a e r]
& EXIST(a):a e s
& EXIST(a):[a e r & ALL(b):[b e s => b<=a]]
Premise
Splitting this premise...
s is a subset of r
6 ALL(a):[a e s => a e r]
Split, 5
s is non-empty
7 EXIST(a):a e s
Split, 5
s is bounded from above
8 EXIST(a):[a e r & ALL(b):[b e s => b<=a]]
Split, 5
Suppose lub is the least upper bound of s
9 lub e r
& ALL(a):[a e s => a<=lub]
& ALL(a):[a e r & ALL(b):[b e s => b<=a] => lub<=a]
Premise
Splitting this premise...
10 lub e r
Split, 9
11 ALL(a):[a e s => a<=lub]
Split, 9
12 ALL(a):[a e r & ALL(b):[b e s => b<=a] => lub<=a]
Split, 9
Prove: ALL(a):[a e r => [a<lub => EXIST(b):[b e s & [a<b & b<=lub]]]]
Suppose...
13 x e r
Premise
Prove: x<lub => EXIST(b):[b e s & [x<b & b<=lub]]
Suppose...
14 x<lub
Premise
Two cases to consider:
15 lub e s | ~lub e s
Or Not
Case 1
Prove: lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
Suppose...
16 lub e s
Premise
Apply property of <= on r
17 lub e r => lub<=lub
U Spec, 1
18 lub<=lub
Detach, 17, 10
19 x<lub & lub<=lub
Join, 14, 18
20 lub e s & [x<lub & lub<=lub]
Join, 16, 19
21 EXIST(b):[b e s & [x<b & b<=lub]]
E Gen, 20
Case 1
As Required:
22 lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
4 Conclusion, 16
Case 2
Prove: ~lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
Suppose...
23 ~lub e s
Premise
Prove: EXIST(b):[b e s & [x<b & b<=lub]]
Suppose to the contrary...
24 ~EXIST(b):[b e s & [x<b & b<=lub]]
Premise
25 ~~ALL(b):~[b e s & [x<b & b<=lub]]
Quant, 24
26 ALL(b):~[b e s & [x<b & b<=lub]]
Rem DNeg, 25
27 ALL(b):~~[b e s => ~[x<b & b<=lub]]
Imply-And, 26
28 ALL(b):[b e s => ~[x<b & b<=lub]]
Rem DNeg, 27
29 ALL(b):[b e s => ~~[~x<b | ~b<=lub]]
DeMorgan, 28
30 ALL(b):[b e s => ~x<b | ~b<=lub]
Rem DNeg, 29
Prove: ALL(a):[a e s => a<=x] i.e. x is an upper bound
of s (to obtain a contradiction)
Suppose...
31 y e s
Premise
Apply premise...
32 y e s => ~x<y | ~y<=lub
U Spec, 30
Two sub-cases to consider:
33 ~x<y | ~y<=lub
Detach, 32, 31
Sub-case 1
Prove: ~x<y => y<=x
Apply property of < and <=
34 ALL(b):[x e r & b e r => [~x<b => b<=x]]
U Spec, 2
35 x e r & y e r => [~x<y => y<=x]
U Spec, 34
36 y e s => y e r
U Spec, 6
37 y e r
Detach, 36, 31
38 x e r & y e r
Join, 13, 37
Sub-case 1
As Required:
39 ~x<y => y<=x
Detach, 35, 38
Sub-case 2
Prove: ~y<=lub => y<=x
Suppose...
40 ~y<=lub
Premise
Apply property of < and <= on r
41 ALL(b):[y e r & b e r => [~y<=b => b<y]]
U Spec, 3
42 y e r & lub e r => [~y<=lub => lub<y]
U Spec, 41
43 y e r & lub e r
Join, 37, 10
44 ~y<=lub => lub<y
Detach, 42, 43
45 lub<y
Detach, 44, 40
Apply definition of lub
46 y e s => y<=lub
U Spec, 11
47 y<=lub
Detach, 46, 31
Apply Arbitrary Consequent Rule
48 ~y<=lub => y<=x
Arb Cons, 47
49 y<=x
Detach, 48, 40
Sub-case 2
As Required:
50 ~y<=lub => y<=x
4 Conclusion, 40
Joining results...
51 [~x<y => y<=x] & [~y<=lub => y<=x]
Join, 39, 50
52 y<=x
Cases, 33, 51
x is an upper bound of s (to obtain a contradiction)
As Required:
53 ALL(a):[a e s => a<=x]
4 Conclusion, 31
Apply defintion of lub to obtain a contradiction
54 x e r & ALL(b):[b e s => b<=x] => lub<=x
U Spec, 12
55 x e r & ALL(a):[a e s => a<=x]
Join, 13, 53
56 lub<=x
Detach, 54, 55
Apply property of < and <= on r
57 ALL(b):[lub e r & b e r => [lub<=b => ~b<lub]]
U Spec, 4
58 lub e r & x e r => [lub<=x => ~x<lub]
U Spec, 57
59 lub e r & x e r
Join, 10, 13
60 lub<=x => ~x<lub
Detach, 58, 59
61 ~x<lub
Detach, 60, 56
Obtain the contradiction...
62 x<lub & ~x<lub
Join, 14, 61
As Required:
63 ~~EXIST(b):[b e s & [x<b & b<=lub]]
4 Conclusion, 24
As Required:
64 EXIST(b):[b e s & [x<b & b<=lub]]
Rem DNeg, 63
Case 2
As Required:
65 ~lub e s => EXIST(b):[b e s & [x<b & b<=lub]]
4 Conclusion, 23
Joining results...
66 [lub e s => EXIST(b):[b e s & [x<b & b<=lub]]]
& [~lub e s => EXIST(b):[b e s & [x<b & b<=lub]]]
Join, 22, 65
67 EXIST(b):[b e s & [x<b & b<=lub]]
Cases, 15, 66
As Required:
68 x<lub => EXIST(b):[b e s & [x<b & b<=lub]]
4 Conclusion, 14
As Required:
69 ALL(a):[a e r => [a<lub => EXIST(b):[b e s & [a<b & b<=lub]]]]
4 Conclusion, 13
As Required:
70 ALL(lub):[lub e r
& ALL(a):[a e s => a<=lub]
& ALL(a):[a e r & ALL(b):[b e s => b<=a] => lub<=a]
=> ALL(a):[a e r => [a<lub => EXIST(b):[b e s & [a<b & b<=lub]]]]]
4 Conclusion, 9
As Required:
71 ALL(s):[ALL(a):[a e s => a e r]
& EXIST(a):a e s
& EXIST(a):[a e r & ALL(b):[b e s => b<=a]]
=> ALL(lub):[lub e r
& ALL(a):[a e s => a<=lub]
& ALL(a):[a e r & ALL(b):[b e s => b<=a] => lub<=a]
=> ALL(a):[a e r => [a<lub => EXIST(b):[b e s & [a<b & b<=lub]]]]]]
4 Conclusion, 5