Apostol.Chapter_I_03

A Set of Axioms for the Real-Number System

The least-upper-bound axiom (completeness axiom)

theorem Apostol.Chapter_I_03.set_neg_prop_iff_neg_set_prop (S : Set ℝ) (p : ℝ → Prop) : (∀ y ∈ S, p (-y)) ↔ ∀ y ∈ -S, p y

A property holds for the negation of elements in set S iff it also holds for the elements of the negation of S.

theorem Apostol.Chapter_I_03.upper_bounds_neg_eq_neg_lower_bounds (S : Set ℝ) : upperBounds (-S) = -lowerBounds S

The upper bounds of the negation of a set is the negation of the lower bounds of the set.

theorem Apostol.Chapter_I_03.neg_upper_bounds_eq_lower_bounds_neg (S : Set ℝ) : -upperBounds S = lowerBounds (-S)

The negation of the upper bounds of a set is the lower bounds of the negation of the set.

theorem Apostol.Chapter_I_03.is_least_neg_set_eq_is_greatest_set_neq {x : ℝ} (S : Set ℝ) : IsLeast (-S) x = IsGreatest S (-x)

An element x is the least element of the negation of a set iff -x is the greatest element of the set.

theorem Apostol.Chapter_I_03.is_lub_neg_set_iff_is_glb_set_neg {x : ℝ} (S : Set ℝ) : IsLUB (-S) x = IsGLB S (-x)

At least with respect to ℝ, x is the least upper bound of set -S iff -x is the greatest lower bound of S.

theorem Apostol.Chapter_I_03.exists_isGLB (S : Set ℝ) (hne : Set.Nonempty S) (hbdd : BddBelow S) : ∃ (x : ℝ), IsGLB S x

Theorem I.27

Every nonempty set S that is bounded below has a greatest lower bound; that is, there is a real number L such that L = inf S.

theorem Apostol.Chapter_I_03.leq_nat_abs_ceil_self (x : ℝ) : x ≤ ↑(Int.natAbs ⌈x⌉)

Every real should be less than or equal to the absolute value of its ceiling.

The Archimedean property of the real-number system

theorem Apostol.Chapter_I_03.exists_pnat_geq_self (x : ℝ) : ∃ (n : ℕ+), ↑↑n > x

Theorem I.29

For every real x there exists a positive integer n such that n > x.

theorem Apostol.Chapter_I_03.exists_pnat_mul_self_geq_of_pos {x : ℝ} {y : ℝ} : x > 0 → ∃ (n : ℕ+), ↑↑n * x > y

Theorem I.30

If x > 0 and if y is an arbitrary real number, there exists a positive integer n such that nx > y.

This is known as the Archimedean Property of the Reals.

theorem Apostol.Chapter_I_03.forall_pnat_leq_self_leq_frac_imp_eq {x : ℝ} {y : ℝ} {a : ℝ} : (∀ (n : ℕ+), a ≤ x ∧ x ≤ a + y / ↑↑n) → x = a

Theorem I.31

If three real numbers a, x, and y satisfy the inequalities a ≤ x ≤ a + y / n for every integer n ≥ 1, then x = a.

theorem Apostol.Chapter_I_03.forall_pnat_frac_leq_self_leq_imp_eq {x : ℝ} {y : ℝ} {a : ℝ} : (∀ (n : ℕ+), a - y / ↑↑n ≤ x ∧ x ≤ a) → x = a

If three real numbers a, x, and y satisfy the inequalities a - y / n ≤ x ≤ a for every integer n ≥ 1, then x = a.

Fundamental properties of the supremum and infimum

theorem Apostol.Chapter_I_03.mem_upper_bounds_iff_forall_le {ub : ℝ} {S : Set ℝ} : ub ∈ upperBounds S ↔ ∀ x ∈ S, x ≤ ub

Every member of a set S is less than or equal to some value ub if and only if ub is an upper bound of S.

theorem Apostol.Chapter_I_03.forall_lub_imp_forall_le {ub : ℝ} {S : Set ℝ} : IsLUB S ub → ∀ x ∈ S, x ≤ ub

If a set S has a least upper bound, it follows every member of S is less than or equal to that value.

theorem Apostol.Chapter_I_03.mem_imp_ge_lub {S : Set ℝ} {s : ℝ} {x : ℝ} (h : IsLUB S s) : x ∈ upperBounds S → x ≥ s

Any member of the upper bounds of a set must be greater than or equal to the least member of that set.

theorem Apostol.Chapter_I_03.sup_imp_exists_gt_sup_sub_delta {S : Set ℝ} {s : ℝ} {h : ℝ} (hp : h > 0) : IsLUB S s → ∃ x ∈ S, x > s - h

Theorem I.32a

Let h be a given positive number and let S be a set of real numbers. If S has a supremum, then for some x in S we have x > sup S - h.

theorem Apostol.Chapter_I_03.mem_lower_bounds_iff_forall_ge {lb : ℝ} {S : Set ℝ} : lb ∈ lowerBounds S ↔ ∀ x ∈ S, x ≥ lb

Every member of a set S is greater than or equal to some value lb if and only if lb is a lower bound of S.

theorem Apostol.Chapter_I_03.forall_glb_imp_forall_ge {lb : ℝ} {S : Set ℝ} : IsGLB S lb → ∀ x ∈ S, x ≥ lb

If a set S has a greatest lower bound, it follows every member of S is greater than or equal to that value.

theorem Apostol.Chapter_I_03.mem_imp_le_glb {S : Set ℝ} {s : ℝ} {x : ℝ} (h : IsGLB S s) : x ∈ lowerBounds S → x ≤ s

Any member of the lower bounds of a set must be less than or equal to the greatest member of that set.

theorem Apostol.Chapter_I_03.inf_imp_exists_lt_inf_add_delta {S : Set ℝ} {s : ℝ} {h : ℝ} (hp : h > 0) : IsGLB S s → ∃ x ∈ S, x < s + h

Theorem I.32b

Let h be a given positive number and let S be a set of real numbers. If S has an infimum, then for some x in S we have x < inf S + h.

theorem Apostol.Chapter_I_03.sup_minkowski_sum_eq_sup_add_sup (A : Set ℝ) (B : Set ℝ) (a : ℝ) (b : ℝ) (hA : Set.Nonempty A) (hB : Set.Nonempty B) (ha : IsLUB A a) (hb : IsLUB B b) : IsLUB (Set.minkowskiSum A B) (a + b)

Theorem I.33a (Additive Property)

Given nonempty subsets A and B of ℝ, let C denote the set C = {a + b : a ∈ A, b ∈ B}. If each of A and B has a supremum, then C has a supremum, and sup C = sup A + sup B.

theorem Apostol.Chapter_I_03.inf_minkowski_sum_eq_inf_add_inf {a : ℝ} {b : ℝ} (A : Set ℝ) (B : Set ℝ) (hA : Set.Nonempty A) (hB : Set.Nonempty B) (ha : IsGLB A a) (hb : IsGLB B b) : IsGLB (Set.minkowskiSum A B) (a + b)

Theorem I.33b (Additive Property)

Given nonempty subsets A and B of ℝ, let C denote the set C = {a + b : a ∈ A, b ∈ B}. If each of A and B has an infimum, then C has an infimum, and inf C = inf A + inf B.

theorem Apostol.Chapter_I_03.forall_mem_le_forall_mem_imp_sup_le_inf (S : Set ℝ) (T : Set ℝ) (hS : Set.Nonempty S) (hT : Set.Nonempty T) (p : ∀ s ∈ S, ∀ t ∈ T, s ≤ t) : ∃ (s : ℝ), IsLUB S s ∧ ∃ (t : ℝ), IsGLB T t ∧ s ≤ t

Theorem I.34

Given two nonempty subsets S and T of ℝ such that s ≤ t for every s in S and every t in T. Then S has a supremum, and T has an infimum, and they satisfy the inequality sup S ≤ inf T.

theorem Apostol.Chapter_I_03.exercise_1 (x : ℝ) (y : ℝ) (h : x < y) : ∃ (z : ℝ), x < z ∧ z < y

Exercise 1

If x and y are arbitrary real numbers with x < y, prove that there is at least one real z satisfying x < z < y.

theorem Apostol.Chapter_I_03.exercise_2 (x : ℝ) : ∃ (m : ℝ) (n : ℝ), m < x ∧ x < n

Exercise 2

If x is an arbitrary real number, prove that there are integers m and n such that m < x < n.

theorem Apostol.Chapter_I_03.exercise_3 (x : ℝ) (h : x > 0) : ∃ (n : ℕ+), 1 / ↑↑n < x

Exercise 3

If x > 0, prove that there is a positive integer n such that 1 / n < x.

theorem Apostol.Chapter_I_03.exercise_4 (x : ℝ) : ∃! (n : ℤ), ↑n ≤ x ∧ x < ↑n + 1

Exercise 4

If x is an arbitrary real number, prove that there is exactly one integer n which satisfies the inequalities n ≤ x < n + 1. This n is called the greatest integer in x and is denoted by ⌊x⌋. For example, ⌊5⌋ = 5, ⌊5 / 2⌋ = 2, ⌊-8/3⌋ = -3.

theorem Apostol.Chapter_I_03.exercise_5 (x : ℝ) : ∃! (n : ℤ), x ≤ ↑n ∧ ↑n < x + 1

Exercise 5

If x is an arbitrary real number, prove that there is exactly one integer n which satisfies x ≤ n < x + 1.

Exercise 6

If x and y are arbitrary real numbers, x < y, prove that there exists at least one rational number r satisfying x < r < y, and hence infinitely many. This property is often described by saying that the rational numbers are dense in the real-number system.

TODO

Exercise 7

If x is rational, x ≠ 0, and y irrational, prove that x + y, x - y, xy, x / y, and y / x are all irrational.

TODO

Exercise 8

Is the sum or product of two irrational numbers always irrational?

TODO

Exercise 9

If x and y are arbitrary real numbers, x < y, prove that there exists at least one irrational number z satisfying x < z < y, and hence infinitely many.

TODO

Exercise 10

An integer n is called even if n = 2m for some integer m, and odd if n + 1 is even. Prove the following statements:

(a) An integer cannot be both even and odd.

(b) Every integer is either even or odd.

(c) The sum or product of two even integers is even. What can you say about the sum or product of two odd integers?

(d) If n² is even, so is n. If a² = 2b², where a and b are integers, then both a and b are even.

(e) Every rational number can be expressed in the form a / b, where a and b are integers, at least one of which is odd.

TODO

def Apostol.Chapter_I_03.isEven (n : ℤ) : Prop

Equations

• Apostol.Chapter_I_03.isEven n = ∃ (m : ℤ), n = 2 * m

def Apostol.Chapter_I_03.isOdd (n : ℤ) : Prop

Equations

• Apostol.Chapter_I_03.isOdd n = Apostol.Chapter_I_03.isEven (n + 1)

Exercise 11

Prove that there is no rational number whose square is 2.

[Hint: Argue by contradiction. Assume (a / b)² = 2, where a and b are integers, at least one of which is odd. Use parts of Exercise 10 to deduce a contradiction.]

TODO

Exercise 12

The Archimedean property of the real-number system was deduced as a consequence of the least-upper-bound axiom. Prove that the set of rational numbers satisfies the Archimedean property but not the least-upper-bound property. This shows that the Archimedean property does not imply the least-upper-bound axiom.

TODO