Theory realax

⊢ ∀x. clg x = LEAST n. x ≤ &n

⊢ ∀x. flr x = LEAST n. &(n + 1) > x

⊢ ∀T1. hreal_of_real T1 = hreal_of_treal (real_REP T1)

⊢ real_0 = real_ABS treal_0

⊢ real_1 = real_ABS treal_1

⊢ ∀r. real_ABS r = real_ABS_CLASS (treal_eq r)

⊢ ∀a. real_REP a = $@ (real_REP_CLASS a)

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. treal_eq r r ∧ (c = treal_eq r)) rep

⊢ ∀x. abs x = if 0 ≤ x then x else -x

⊢ ∀T1 T2. T1 + T2 = real_ABS (real_REP T1 treal_add real_REP T2)

⊢ (∀a. real_ABS_CLASS (real_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. treal_eq r r ∧ (c = treal_eq r)) r ⇔
      (real_REP_CLASS (real_ABS_CLASS r) = r)

⊢ ∀x y. x / y = x * y⁻¹

⊢ ∀x y. x ≥ y ⇔ y ≤ x

⊢ ∀x y. x > y ⇔ y < x

⊢ ∀T1. T1⁻¹ = real_ABS (treal_inv (real_REP T1))

⊢ ∀x y. x ≤ y ⇔ ¬(y < x)

⊢ ∀x y. max x y = if x ≤ y then y else x

⊢ ∀x y. min x y = if x ≤ y then x else y

⊢ ∀T1 T2. T1 * T2 = real_ABS (real_REP T1 treal_mul real_REP T2)

⊢ ∀T1. -T1 = real_ABS (treal_neg (real_REP T1))

⊢ ∀T1. real_of_hreal T1 = real_ABS (treal_of_hreal T1)

⊢ (0 = real_0) ∧ ∀n. &SUC n = &n + real_1

⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n

⊢ ∀x y. x − y = x + -y

⊢ ∀n. &SUC n = &n + 1

⊢ real_0 = 0

⊢ real_1 = 1

⊢ real_1 ≠ real_0

⊢ 1 ≠ 0

⊢ ∀x. abs (-x) = abs x

⊢ ∀n. abs (&n) = &n

⊢ ∀m n. &m + &n = &(m + n)

⊢ (m + n = n + m) ∧ (m + n + p = m + (n + p)) ∧ (m + (n + p) = n + (m + p))

⊢ ∀x y z. x + (y + z) = x + y + z

⊢ ∀x y z. x * (y + z) = x * y + x * z

⊢ ∀x. real_0 + x = x

⊢ ∀x. 0 + x = x

⊢ ∀x. -x + x = real_0

⊢ ∀x. -x + x = 0

⊢ ∀x y z. (x + y) * z = x * z + y * z

⊢ ∀x. x + 0 = x

⊢ ∀x. x + -x = 0

⊢ ∀x y. x + y = y + x

⊢ (∀h. hreal_of_real (real_of_hreal h) = h) ∧
  ∀r. real_0 < r ⇔ (real_of_hreal (hreal_of_real r) = r)

⊢ ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)

⊢ ∀x y z. (x + y = x + z) ⇔ (y = z)

⊢ ∀x y z. (x + z = y + z) ⇔ (x = y)

⊢ ∀m n. (&m = &n) ⇔ (m = n)

⊢ real_0⁻¹ = real_0

⊢ 0⁻¹ = 0

⊢ ∀h i. h hreal_lt i ⇒ real_of_hreal h < real_of_hreal i

⊢ ∀h i. h hreal_lt i ⇔ real_of_hreal h < real_of_hreal i

⊢ ∀x y z. x * (y + z) = x * y + x * z

⊢ ∀m n. &m ≤ &n ⇔ m ≤ n

⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y

⊢ ∀x y. x ≤ y ∨ y < x

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

⊢ 0 ≤ 1

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y

⊢ ∀x y. x ≤ x + y ⇔ 0 ≤ y

⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ (x = y)

⊢ ∀x y z. x + y ≤ x + z ⇔ y ≤ z

⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z

⊢ ∀x y. -x ≤ y ⇔ 0 ≤ x + y

⊢ ∀x y. x ≤ y ⇔ x < y ∨ (x = y)

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y

⊢ ∀x y. -x ≤ -y ⇔ y ≤ x

⊢ ∀x. 0 ≤ x ∨ 0 ≤ -x

⊢ ∀x y z. x + z ≤ y + z ⇔ x ≤ y

⊢ ∀x. x ≤ x

⊢ ∀x y. x ≤ -y ⇔ x + y ≤ 0

⊢ ∀x. 0 ≤ x * x

⊢ ∀x y. x ≤ y ∨ y ≤ x

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

⊢ ∀x y. (x + y = 0) ⇔ (x = -y)

⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y

⊢ ∀x y. ¬(x ≤ y ∧ y < x)

⊢ ∀x y. x < y ∨ y ≤ x

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

⊢ 0 < 1

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y

⊢ ∀x y. x < x + y ⇔ 0 < y

⊢ ∀x y. ¬(x < y ∧ y < x)

⊢ ∀x y. x < y ⇒ ¬(y < x)

⊢ ∀x y z. y < z ⇒ x + y < x + z

⊢ ∀x y. x < y ⇒ x ≤ y

⊢ ∀x y z. x + y < x + z ⇔ y < z

⊢ ∀x y z. y < z ⇒ x + y < x + z

⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y

⊢ ∀x y. real_0 < x ∧ real_0 < y ⇒ real_0 < x * y

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y

⊢ ∀x. (x = 0) ∨ 0 < x ∨ 0 < -x

⊢ ∀n. &n ≠ 0 ⇔ 0 < &n

⊢ ∀x y z. x + z < y + z ⇔ x < y

⊢ ∀x. ¬(x < x)

⊢ ∀x y. (x = y) ∨ x < y ∨ y < x

⊢ ∀x y z. x < y ∧ y < z ⇒ x < z

⊢ ∀m n. &m * &n = &(m * n)

⊢ (m * n = n * m) ∧ (m * n * p = m * (n * p)) ∧ (m * (n * p) = n * (m * p))

⊢ ∀x y z. x * (y * z) = x * y * z

⊢ ∀x. real_1 * x = x

⊢ ∀x. 1 * x = x

⊢ ∀x. x ≠ real_0 ⇒ (x⁻¹ * x = real_1)

⊢ ∀x. x ≠ 0 ⇒ (x⁻¹ * x = 1)

⊢ ∀x y. -x * y = -(x * y)

⊢ ∀x. 0 * x = 0

⊢ ∀x. x * 1 = x

⊢ ∀x y. x * -y = -(x * y)

⊢ ∀x. x * 0 = 0

⊢ ∀x y. x * y = y * x

⊢ -0 = 0

⊢ ∀x y. -(x + y) = -x + -y

⊢ ∀x y. -(x * y) = -x * y

⊢ ∀x. -x < 0 ⇔ 0 < x

⊢ ∀x. --x = x

⊢ ∀x y. -(x * y) = x * -y

⊢ ∀x y. -(x − y) = y − x

⊢ ∀x y. ¬(x ≤ y) ⇔ y < x

⊢ ∀x y. ¬(x < y) ⇔ y ≤ x

⊢ ∀m n. &m + &n = &(m + n)

⊢ ∀m n. (&m = &n) ⇔ (m = n)

⊢ ∀m n. &m ≤ &n ⇔ m ≤ n

⊢ ∀m n. &m * &n = &(m * n)

⊢ ∀x n. &x pow n = &(x ** n)

⊢ ∀m n. m ≤ n ⇒ (&(n − m) = &n − &m)

⊢ (1 * x = x) ∧ (a * m + b * m = (a + b) * m) ∧ (a * m + m = (a + 1) * m) ∧
  (m + a * m = (a + 1) * m) ∧ (m + m = (1 + 1) * m) ∧ (0 * m = 0) ∧
  (0 + a = a) ∧ (a + 0 = a) ∧ (a * b = b * a) ∧
  ((a + b) * c = a * c + b * c) ∧ (0 * a = 0) ∧ (a * 0 = 0) ∧ (1 * a = a) ∧
  (a * 1 = a) ∧ (lx * ly * (rx * ry) = lx * rx * (ly * ry)) ∧
  (lx * ly * (rx * ry) = lx * (ly * (rx * ry))) ∧
  (lx * ly * (rx * ry) = rx * (lx * ly * ry)) ∧
  (lx * ly * rx = lx * rx * ly) ∧ (lx * ly * rx = lx * (ly * rx)) ∧
  (lx * rx = rx * lx) ∧ (lx * (rx * ry) = lx * rx * ry) ∧
  (lx * (rx * ry) = rx * (lx * ry)) ∧ (a + b + (c + d) = a + c + (b + d)) ∧
  (a + b + c = a + (b + c)) ∧ (a + (c + d) = c + (a + d)) ∧
  (a + b + c = a + c + b) ∧ (a + c = c + a) ∧ (a + (c + d) = a + c + d) ∧
  (x pow p * x pow q = x pow (p + q)) ∧ (x * x pow q = x pow SUC q) ∧
  (x pow q * x = x pow SUC q) ∧ (x * x = x pow 2) ∧
  ((x * y) pow q = x pow q * y pow q) ∧ ((x pow p) pow q = x pow (p * q)) ∧
  (x pow 0 = 1) ∧ (x pow 1 = x) ∧ (x * (y + z) = x * y + x * z) ∧
  (x pow SUC q = x * x pow q)

⊢ (∀x. -x = -1 * x) ∧ ∀x y. x − y = x + -1 * y

⊢ ∀n. 0 ≤ &n

⊢ ∀n. 0 < &SUC n

⊢ ∀x. x pow 2 = x * x

⊢ ∀x n. -x pow n = if EVEN n then x pow n else -(x pow n)

⊢ ∀x y z. (x + y) * z = x * z + y * z

⊢ ∀x y. (x + y = 0) ⇔ (y = -x)

⊢ ∀x y. (x − y = 0) ⇔ (x = y)

⊢ ∀x y. 0 ≤ x − y ⇔ y ≤ x

⊢ ∀x y. 0 < x − y ⇔ y < x

⊢ ∀P. (∀x. P x ⇒ real_0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
      ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

⊢ ∀P. (∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
      ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

⊢ (∀a. real_ABS_CLASS (real_REP_CLASS a) = a) ∧
  ∀c. (∃r. treal_eq r r ∧ (c = treal_eq r)) ⇔
      (real_REP_CLASS (real_ABS_CLASS c) = c)

⊢ QUOTIENT treal_eq real_ABS real_REP

⊢ ∀y x. x < y ⇔ ¬(y ≤ x)