The Theory %real%
 Parents
 Children
 analysis
 Constants
 Is_ℝ_Rep DYADIC SET → BOOL \$R ℝ → ℝ → BOOL \$≥R ℝ → ℝ → BOOL Sup ℝ SET → ℝ 1R ℝ 0R ℝ \$+R ℝ → ℝ → ℝ ~R ℝ → ℝ \$-R ℝ → ℝ → ℝ ℕℝ ℕ → ℝ AbsR ℝ → ℝ \$*R ℝ → ℝ → ℝ \$/R ℝ → ℝ → ℝ \$/N ℕ → ℕ → ℝ \$-1 ℝ → ℝ \$^N ℝ → ℕ → ℝ ℤℝ ℤ → ℝ \$^Z ℝ → ℤ → ℝ Float ℕ → ℤ → ℤ → ℝ MaxR ℝ LIST → ℝ MinR ℝ LIST → ℝ
 Aliases
 < \$ \$>R : ℝ → ℝ → BOOL ≥ \$≥R : ℝ → ℝ → BOOL + \$+R : ℝ → ℝ → ℝ ~ ~R : ℝ → ℝ - \$-R : ℝ → ℝ → ℝ Abs AbsR : ℝ → ℝ * \$*R : ℝ → ℝ → ℝ / \$/R : ℝ → ℝ → ℝ / \$/N : ℕ → ℕ → ℝ ^ \$^N : ℝ → ℕ → ℝ ^ \$^Z : ℝ → ℤ → ℝ
 Types
 ℝ
 Fixity
 Left Infix 305: -R Left Infix 315: / /N /R Right Infix 210: R ≤R ≥R Right Infix 300: +R Right Infix 310: *R Right Infix 320: ^N ^Z Postfix 320: -1
 Definitions
 Is_ℝ_Rep ⊢ ∀ a• Is_ℝ_Rep a ⇔ a ∈ Cuts (Universe, \$dy_less) ℝ ℝ_def ⊢ ∃ f• TypeDefn Is_ℝ_Rep f R ⊢ ∀ x y• x > y ⇔ y < x ≥R ⊢ ∀ x y• x ≥ y ⇔ y ≤ x Sup ⊢ ConstSpec (λ Sup' • ∀ A • ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b) ⇒ (∀ x• x ∈ A ⇒ x ≤ Sup' A) ∧ (∀ b • (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup' A ≤ b)) Sup +R 0R 1R ⊢ ConstSpec (λ (+R', 0R', 1R') • (∀ x y z • +R' (+R' x y) z = +R' x (+R' y z)) ∧ (∀ x y• +R' x y = +R' y x) ∧ (∀ x• +R' x 0R' = x) ∧ (∀ x• ∃ y• +R' x y = 0R') ∧ (∀ x y z• y < z ⇒ +R' x y < +R' x z) ∧ 0R' < 1R') (\$+, 0R, 1R) ~R ⊢ ConstSpec (λ ~R'• ∀ x• x + ~R' x = 0R) ~ -R ⊢ ∀ x y• x - y = x + ~ y ℕℝ ⊢ 0. = 0R ∧ (∀ m• ℕℝ (m + 1) = ℕℝ m + 1R) AbsR ⊢ ∀ x• Abs x = (if 0. ≤ x then x else ~ x) *R ⊢ ConstSpec (λ *R' • (∀ x y z • *R' (*R' x y) z = *R' x (*R' y z)) ∧ (∀ x• *R' x 1. = x) ∧ (∀ x y z • *R' x (y + z) = *R' x y + *R' x z) ∧ (∀ x y• *R' x y = *R' y x) ∧ (∀ x y• 0. < x ∧ 0. < y ⇒ 0. < *R' x y)) \$* /R ⊢ ConstSpec (λ /R' • (∀ y z• ¬ z = 0. ⇒ /R' (y * z) z = y) ∧ (∀ x y z • ¬ z = 0. ⇒ /R' (x * y) z = x * /R' y z)) \$/ /N ⊢ ∀ m n• m / n = ℕℝ m / ℕℝ n -1 ⊢ ∀ x• x -1 = 1. / x ^N ⊢ (∀ x• x ^ 0 = 1.) ∧ (∀ x m• x ^ (m + 1) = x * x ^ m) ℤℝ ⊢ ConstSpec (λ \$"ℤℝ'" • \$"ℤℝ'" (ℕℤ 0) = 0. ∧ \$"ℤℝ'" (ℕℤ 1) = 1. ∧ (∀ i j • \$"ℤℝ'" (i + j) = \$"ℤℝ'" i + \$"ℤℝ'" j)) ℤℝ ^Z ⊢ ConstSpec (λ ^Z' • ∀ x m • ^Z' x (ℕℤ m) = x ^ m ∧ ^Z' x (~ (ℕℤ (m + 1))) = (x ^ (m + 1)) -1) \$^ Float ⊢ ∀ m p e• Float m p e = ℕℝ m * 10. ^ (e + ~ p) MaxR ⊢ ConstSpec (λ MaxR' • (∀ x• MaxR' [x] = x) ∧ (∀ x y L • MaxR' (Cons x (Cons y L)) = (if x < MaxR' (Cons y L) then MaxR' (Cons y L) else x))) MaxR MinR ⊢ ConstSpec (λ MinR' • (∀ x• MinR' [x] = x) ∧ (∀ x y L • MinR' (Cons x (Cons y L)) = (if x > MinR' (Cons y L) then MinR' (Cons y L) else x))) MinR
 Theorems
 dy_less_order_lemmas_thm ⊢ StrictLinearOrder (Universe, \$dy_less) ∧ UnboundedBelow (Universe, \$dy_less) ∧ UnboundedAbove (Universe, \$dy_less) ∧ Universe DenseIn (Universe, \$dy_less) is_ℝ_rep_consistent_thm ⊢ ∃ a• Is_ℝ_Rep a MinR' (Cons y L) then MinR' (Cons y L) else x))) ℝ_max_cons_thm ⊢ ∀ x L • MaxR (Cons x L) = (if L = [] then x else if x < MaxR L then MaxR L else x) ℝ_max_conv_thm ⊢ ∀ x y L • MaxR (Cons x (Cons y L)) = (if x < y then MaxR (Cons y L) else MaxR (Cons x L)) ℝ_min_cons_thm ⊢ ∀ x L • MinR (Cons x L) = (if L = [] then x else if MinR L < x then MinR L else x) ℝ_min_conv_thm ⊢ ∀ x y L • MinR (Cons x (Cons y L)) = (if x < y then MinR (Cons x L) else MinR (Cons y L)) ^Z_consistent ⊢ Consistent (λ ^Z' • ∀ x m • ^Z' x (ℕℤ m) = x ^ m ∧ ^Z' x (~ (ℕℤ (m + 1))) = (x ^ (m + 1)) -1) ℤℝ_consistent ⊢ Consistent (λ \$"ℤℝ'" • \$"ℤℝ'" (ℕℤ 0) = 0. ∧ \$"ℤℝ'" (ℕℤ 1) = 1. ∧ (∀ i j • \$"ℤℝ'" (i + j) = \$"ℤℝ'" i + \$"ℤℝ'" j)) ℤℝ_plus_homomorphism_thm ⊢ ∀ i j• ℤℝ (i + j) = ℤℝ i + ℤℝ j ℤℝ_minus_thm ⊢ ∀ i• ℤℝ (~ i) = ~ (ℤℝ i) ℤℝ_ℕℤ_thm ⊢ ∀ m• ℤℝ (ℕℤ m) = ℕℝ m ∧ ℤℝ (~ (ℕℤ m)) = ~ (ℕℝ m) ℤℝ_times_homomorphism_thm ⊢ ∀ i j• ℤℝ (i * j) = ℤℝ i * ℤℝ j