The Theory analysis

Parents

fin_set

ℝ

Children

group_egs

ℂ

metric_spaces

fincomb

Constants

PolyFunc	(ℝ → ℝ) ℘
PolyEval	ℝ LIST → ℝ → ℝ
PlusCoeffs	ℝ LIST → ℝ LIST → ℝ LIST
TimesCoeffs	ℝ LIST → ℝ LIST → ℝ LIST
$To	(ℕ → 'a) → ℕ → 'a LIST
Roots	('a → ℝ) → 'a ℘
$->	(ℕ → ℝ) → ℝ → BOOL
ClosedInterval	ℝ → ℝ → ℝ ℘
OpenInterval	ℝ → ℝ → ℝ ℘
$Cts	(ℝ → ℝ) → ℝ → BOOL
$Deriv	(ℝ → ℝ) → ℝ → ℝ → BOOL
DerivCoeffs	ℝ LIST → ℝ LIST
Open_R	ℝ ℘ ℘
Closed_R	ℝ ℘ ℘
Compact_R	ℝ ℘ ℘
$-->	(ℝ → ℝ) → ℝ → ℝ → BOOL
$--->	(ℕ → ℝ → ℝ) → (ℝ → ℝ) → ℝ ℘ → BOOL
Series	(ℕ → ℝ) → ℕ → ℝ
PowerSeries	(ℕ → ℝ) → ℕ → ℝ → ℝ
$!	ℕ → ℕ
Exp	ℝ → ℝ
Log	ℝ → ℝ
Cos	ℝ → ℝ
Sin	ℝ → ℝ
ArchimedesConstant	ℝ
$+#->	(ℝ → ℝ) → ℝ → ℝ → BOOL
$-+#>	(ℝ → ℝ) → ℝ → BOOL
$-+#>+#	(ℝ → ℝ) → BOOL
Sqrt	ℝ → ℝ
Tan	ℝ → ℝ
Cotan	ℝ → ℝ
Sec	ℝ → ℝ
Cosec	ℝ → ℝ
ArcSin	ℝ → ℝ
ArcCos	ℝ → ℝ
Sinh	ℝ → ℝ
Cosh	ℝ → ℝ
Tanh	ℝ → ℝ
Cotanh	ℝ → ℝ
Sech	ℝ → ℝ
Cosech	ℝ → ℝ
ArcSinh	ℝ → ℝ
TaggedPartition	(ℕ → ℝ) ↔ ((ℕ → ℝ) × ℕ)
RiemannSum	(ℝ → ℝ) → (ℕ → ℝ) × (ℕ → ℝ) × ℕ → ℝ
Gauge	(ℝ → ℝ ℘) ℘
$Fine	(ℝ → ℝ ℘) → (ℕ → ℝ) ↔ ((ℕ → ℝ) × ℕ)
$Int_R	(ℝ → ℝ) → ℝ → BOOL
CharFun	'a ℘ → 'a → ℝ
$Int	(ℝ → ℝ) → ℝ → ℝ ℘ → BOOL
$Area	ℝ ↔ ℝ → ℝ → BOOL

Aliases

π	ArchimedesConstant : ℝ
χ	CharFun : 'a ℘ → 'a → ℝ

Fixity

Right Infix 200:

Area

Cts

Deriv

Int

Int_R

Right Infix 205:

+#->

-+#>

--->

-->

Right Infix 310:

Postfix 200:

-+#>+#

Postfix 330:

Fine

Definitions

PolyFunc	⊢ PolyFunc = ⋂ {A \|(∀ c• (λ x• c) ∈ A) ∧ (λ x• x) ∈ A ∧ (∀ f g • f ∈ A ∧ g ∈ A ⇒ (λ x• f x + g x) ∈ A) ∧ (∀ f g • f ∈ A ∧ g ∈ A ⇒ (λ x• f x * g x) ∈ A)}
PolyEval	⊢ (∀ x• PolyEval [] x = 0.) ∧ (∀ c l x • PolyEval (Cons c l) x = c + x * PolyEval l x)
PlusCoeffs	⊢ ConstSpec (λ PlusCoeffs' • (∀ l• PlusCoeffs' [] l = l) ∧ (∀ l• PlusCoeffs' l [] = l) ∧ (∀ c1 l1 c2 l2 • PlusCoeffs' (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs' l1 l2))) PlusCoeffs
TimesCoeffs	⊢ (∀ l• TimesCoeffs [] l = []) ∧ (∀ c l1 l2 • TimesCoeffs (Cons c l1) l2 = PlusCoeffs (Cons 0. (TimesCoeffs l1 l2)) (Map (λ x• c * x) l2))
To	⊢ (∀ f• f To 0 = []) ∧ (∀ f n• f To (n + 1) = f To n ⁀ [f n])
Roots	⊢ ∀ f• Roots f = {x\|f x = 0.}
->	⊢ ∀ s x • s -> x ⇔ (∀ e • 0. < e ⇒ (∃ n• ∀ m• n ≤ m ⇒ Abs (s m - x) < e))
ClosedInterval	⊢ ∀ x y• ClosedInterval x y = {t\|x ≤ t ∧ t ≤ y}
OpenInterval	⊢ ∀ x y• OpenInterval x y = {t\|x < t ∧ t < y}
Cts	⊢ ∀ f x • f Cts x ⇔ (∀ e • 0. < e ⇒ (∃ d • 0. < d ∧ (∀ y • Abs (y - x) < d ⇒ Abs (f y - f x) < e)))
Deriv	⊢ ∀ f c x • (f Deriv c) x ⇔ (∀ e • 0. < e ⇒ (∃ d • 0. < d ∧ (∀ y • Abs (y - x) < d ∧ ¬ y = x ⇒ Abs ((f y - f x) / (y - x) - c) < e)))
DerivCoeffs	⊢ DerivCoeffs [] = [] ∧ (∀ c l • DerivCoeffs (Cons c l) = PlusCoeffs l (Cons 0. (DerivCoeffs l)))
Open_R	⊢ Open_R = {A \|∀ t • t ∈ A ⇒ (∃ x y • t ∈ OpenInterval x y ∧ OpenInterval x y ⊆ A)}
Closed_R	⊢ Closed_R = {A\|~ A ∈ Open_R}
Compact_R	⊢ Compact_R = {A \|∀ V • V ⊆ Open_R ∧ A ⊆ ⋃ V ⇒ (∃ W• W ⊆ V ∧ W ∈ Finite ∧ A ⊆ ⋃ W)}
-->	⊢ ∀ f c x • (f --> c) x ⇔ (∀ e • 0. < e ⇒ (∃ d • 0. < d ∧ (∀ y • Abs (y - x) < d ∧ ¬ y = x ⇒ Abs (f y - c) < e)))
--->	⊢ ∀ u h X • (u ---> h) X ⇔ (∀ e • 0. < e ⇒ (∃ n • ∀ m y • n ≤ m ∧ y ∈ X ⇒ Abs (u m y - h y) < e))
Series	⊢ (∀ s• Series s 0 = 0.) ∧ (∀ s n• Series s (n + 1) = Series s n + s n)
PowerSeries	⊢ ∀ s n• PowerSeries s n = PolyEval (s To n)
!	⊢ 0 ! = 1 ∧ (∀ m• (m + 1) ! = (m + 1) * m !)
Exp	⊢ ConstSpec (λ Exp' • Exp' 0. = 1. ∧ (∀ x• (Exp' Deriv Exp' x) x)) Exp
Log	⊢ ConstSpec (λ Log'• ∀ x• Log' (Exp x) = x) Log
Sin Cos	⊢ ConstSpec (λ (Sin', Cos') • Sin' 0. = 0. ∧ Cos' 0. = 1. ∧ (∀ x• (Sin' Deriv Cos' x) x) ∧ (∀ x• (Cos' Deriv ~ (Sin' x)) x)) (Sin, Cos)
ArchimedesConstant	⊢ ConstSpec (λ ArchimedesConstant' • 0. < ArchimedesConstant' ∧ (∀ x • Sin x = 0. ⇔ (∃ m• x = ℕℝ m * ArchimedesConstant') ∨ (∃ m • x = ~ (ℕℝ m * ArchimedesConstant')))) π
+#->	⊢ ∀ f c a • (f +#-> c) a ⇔ (∀ e • 0. < e ⇒ (∃ b • a < b ∧ (∀ x • a < x ∧ x < b ⇒ Abs (f x - c) < e)))
-+#>	⊢ ∀ f c • f -+#> c ⇔ (∀ e • 0. < e ⇒ (∃ b• ∀ x• b < x ⇒ Abs (f x - c) < e))
-+#>+#	⊢ ∀ f• f -+#>+# ⇔ (∀ x• ∃ b• ∀ y• b < y ⇒ x < f y)
Sqrt	⊢ ConstSpec (λ Sqrt' • ∀ x • 0. ≤ x ⇒ 0. ≤ Sqrt' x ∧ Sqrt' x ^ 2 = x ∧ Sqrt' Cts x) Sqrt
Tan	⊢ ∀ x• Tan x = Sin x * Cos x ^-¹
Cotan	⊢ ∀ x• Cotan x = Cos x * Sin x ^-¹
Sec	⊢ ∀ x• Sec x = Cos x ^-¹
Cosec	⊢ ∀ x• Cosec x = Sin x ^-¹
ArcSin	⊢ ConstSpec (λ ArcSin' • (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin' (Sin x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Sin (ArcSin' x) = x ∧ ArcSin' Cts x)) ArcSin
ArcCos	⊢ ConstSpec (λ ArcCos' • (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos' (Cos x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Cos (ArcCos' x) = x ∧ ArcCos' Cts x)) ArcCos
Sinh	⊢ ∀ x• Sinh x = 1 / 2 * (Exp x - Exp (~ x))
Cosh	⊢ ∀ x• Cosh x = 1 / 2 * (Exp x + Exp (~ x))
Tanh	⊢ ∀ x• Tanh x = Sinh x * Cosh x ^-¹
Cotanh	⊢ ∀ x• Cotanh x = Cosh x * Sinh x ^-¹
Sech	⊢ ∀ x• Sech x = Cosh x ^-¹
Cosech	⊢ ∀ x• Cosech x = Sinh x ^-¹
ArcSinh	⊢ ConstSpec (λ ArcSinh' • ∀ x • ArcSinh' (Sinh x) = x ∧ Sinh (ArcSinh' x) = x ∧ ArcSinh' Cts x) ArcSinh
TaggedPartition	⊢ ∀ t I n • (t, I, n) ∈ TaggedPartition ⇔ (∀ m• m < n ⇒ I m < I (m + 1)) ∧ (∀ m • m < n ⇒ t m ∈ ClosedInterval (I m) (I (m + 1)))
RiemannSum	⊢ ∀ f t I n • RiemannSum f (t, I, n) = Series (λ m• f (t m) * (I (m + 1) - I m)) n
Gauge	⊢ ∀ G• G ∈ Gauge ⇔ (∀ x• G x ∈ Open_R ∧ x ∈ G x)
Fine	⊢ ∀ t I n G • (t, I, n) ∈ G Fine ⇔ (∀ m • m < n ⇒ ClosedInterval (I m) (I (m + 1)) ⊆ G (t m))
Int_R	⊢ ∀ f c • f Int_R c ⇔ (∀ e • 0. < e ⇒ (∃ G a b • G ∈ Gauge ∧ a < b ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 < a ∧ b < I n ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e)))
CharFun	⊢ ∀ A x• χ A x = (if x ∈ A then 1. else 0.)
Int	⊢ ∀ f c A• (f Int c) A ⇔ (λ x• χ A x * f x) Int_R c
Area	⊢ ∀ A c • A Area c ⇔ (∃ sf • sf Int_R c ∧ (∀ x• χ {y\|(x, y) ∈ A} Int_R sf x))

Theorems

PlusCoeffs_consistent	⊢ Consistent (λ PlusCoeffs' • (∀ l• PlusCoeffs' [] l = l) ∧ (∀ l• PlusCoeffs' l [] = l) ∧ (∀ c1 l1 c2 l2 • PlusCoeffs' (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs' l1 l2)))
plus_coeffs_def	⊢ (∀ l• PlusCoeffs [] l = l) ∧ (∀ l• PlusCoeffs l [] = l) ∧ (∀ c1 l1 c2 l2 • PlusCoeffs (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs l1 l2))
const_eval_thm	⊢ ∀ c• (λ x• c) = PolyEval [c]
id_eval_thm	⊢ (λ x• x) = PolyEval [0.; 1.]
plus_eval_thm	⊢ ∀ l1 l2 • (λ x• PolyEval l1 x + PolyEval l2 x) = PolyEval (PlusCoeffs l1 l2)
const_times_eval_thm	⊢ ∀ c l • (λ x• c * PolyEval l x) = PolyEval (Map (λ y• c * y) l)
times_eval_thm	⊢ ∀ l1 l2 • (λ x• PolyEval l1 x * PolyEval l2 x) = PolyEval (TimesCoeffs l1 l2)
poly_induction_thm	⊢ ∀ p • (∀ c• p (λ x• c)) ∧ p (λ x• x) ∧ (∀ f g• p f ∧ p g ⇒ p (λ x• f x + g x)) ∧ (∀ f g• p f ∧ p g ⇒ p (λ x• f x * g x)) ⇒ (∀ h• h ∈ PolyFunc ⇒ p h)
poly_func_eq_poly_eval_thm	⊢ PolyFunc = {f\|∃ l• f = PolyEval l}
const_poly_func_thm	⊢ ∀ c• (λ x• c) ∈ PolyFunc
id_poly_func_thm	⊢ (λ x• x) ∈ PolyFunc
plus_poly_func_thm	⊢ ∀ f g • f ∈ PolyFunc ∧ g ∈ PolyFunc ⇒ (λ x• f x + g x) ∈ PolyFunc
times_poly_func_thm	⊢ ∀ f g • f ∈ PolyFunc ∧ g ∈ PolyFunc ⇒ (λ x• f x * g x) ∈ PolyFunc
comp_poly_func_thm	⊢ ∀ f g • f ∈ PolyFunc ∧ g ∈ PolyFunc ⇒ (λ x• f (g x)) ∈ PolyFunc
poly_eval_append_thm	⊢ ∀ l1 l2 x • PolyEval (l1 ⁀ l2) x = PolyEval l1 x + x ^ # l1 * PolyEval l2 x
poly_eval_rev_thm	⊢ (∀ x• PolyEval (Rev []) x = 0.) ∧ (∀ c l x • PolyEval (Rev (Cons c l)) x = c * x ^ # l + PolyEval (Rev l) x)
poly_diff_powers_thm	⊢ ∀ n x y • (x - y) * PolyEval (Rev ((λ m• y ^ m) To (n + 1))) x = x ^ (n + 1) - y ^ (n + 1)
length_plus_coeffs_thm	⊢ ∀ l1 l2 • # (PlusCoeffs l1 l2) = (if # l2 < # l1 then # l1 else # l2)
poly_linear_div_thm	⊢ ∀ l1 c • ¬ l1 = [] ⇒ (∃ l2 r • # l2 < # l1 ∧ (λ x• PolyEval l1 x) = (λ x• (x - c) * PolyEval l2 x + r))
poly_remainder_thm	⊢ ∀ l1 c • ¬ l1 = [] ⇒ (∃ l2 • # l2 < # l1 ∧ (λ x• PolyEval l1 x) = (λ x • (x - c) * PolyEval l2 x + PolyEval l1 c))
poly_factor_thm	⊢ ∀ l1 c • ¬ l1 = [] ∧ PolyEval l1 c = 0. ⇒ (∃ l2 • # l2 < # l1 ∧ (λ x• PolyEval l1 x) = (λ x• (x - c) * PolyEval l2 x))
poly_roots_finite_thm	⊢ ∀ f c• f ∈ PolyFunc ∧ ¬ f c = 0. ⇒ Roots f ∈ Finite
ℝ_0_≤_abs_thm	⊢ ∀ x• 0. ≤ Abs x
ℝ_abs_plus_thm	⊢ ∀ x y• Abs (x + y) ≤ Abs x + Abs y
ℝ_abs_subtract_thm	⊢ ∀ x y• Abs (x - y) ≤ Abs x + Abs y
ℝ_abs_plus_minus_thm	⊢ ∀ x y• Abs (x + ~ y) ≤ Abs x + Abs y
ℝ_abs_diff_bounded_thm	⊢ ∀ x y z • 0. < z ⇒ (Abs (x + ~ y) < z ⇔ y + ~ z < x ∧ x < y + z)
ℝ_abs_plus_bc_thm	⊢ ∀ x y z• Abs x ≤ Abs (y + z) ⇒ Abs x ≤ Abs y + Abs z
ℝ_abs_abs_minus_thm	⊢ ∀ x y• Abs (Abs x - Abs y) ≤ Abs (x - y)
ℝ_abs_abs_thm	⊢ ∀ x• Abs (Abs x) = Abs x
ℝ_abs_times_thm	⊢ ∀ x y• Abs (x * y) = Abs x * Abs y
ℝ_abs_ℝ_ℕ_exp_thm	⊢ ∀ x m• Abs (x ^ m) = Abs x ^ m
ℝ_abs_eq_0_thm	⊢ ∀ x• Abs x = 0. ⇔ x = 0.
ℝ_abs_≤_0_thm	⊢ ∀ x• Abs x ≤ 0. ⇔ x = 0.
ℝ_abs_0_thm	⊢ Abs 0. = 0.
ℝ_abs_recip_thm	⊢ ∀ x• ¬ x = 0. ⇒ Abs (x ^-¹) = Abs x ^-¹
ℝ_abs_squared_thm	⊢ ∀ x• Abs x ^ 2 = x ^ 2
ℝ_abs_less_times_thm	⊢ ∀ x t y u • Abs x < t ∧ Abs y < u ⇒ Abs x * Abs y < t * u
ℝ_¬_0_abs_thm	⊢ ∀ x• ¬ x = 0. ⇔ 0. < Abs x
ℝ_less_recip_less_thm	⊢ ∀ x y• 0. < x ∧ x < y ⇒ y ^-¹ < x ^-¹
ℝ_abs_≤_less_interval_thm	⊢ ∀ x y • (Abs x ≤ y ⇔ x ∈ ClosedInterval (~ y) y) ∧ (Abs x < y ⇔ x ∈ OpenInterval (~ y) y)
ℝ_plus_recip_thm	⊢ ∀ x y • ¬ x = 0. ∧ ¬ y = 0. ⇒ x ^-¹ + y ^-¹ = (x + y) * x ^-¹ * y ^-¹
ℕℝ_recip_thm	⊢ ∀ m• ℕℝ (m + 1) ^-¹ ^-¹ = ℕℝ (m + 1)
ℕℝ_0_less_recip_thm	⊢ ∀ m• 0. < ℕℝ (m + 1) ^-¹
ℕℝ_recip_not_eq_0_thm	⊢ ∀ m• ¬ ℕℝ (m + 1) ^-¹ = 0.
ℝ_ℕ_exp_0_1_thm	⊢ ∀ m• 0. ^ (m + 1) = 0. ∧ 1. ^ m = 1.
ℝ_ℕ_exp_square_thm	⊢ ∀ x• x ^ 2 = x * x
ℝ_ℕ_exp_0_less_thm	⊢ ∀ m x• 0. < x ⇒ 0. < x ^ m
ℝ_ℕ_exp_1_less_mono_thm	⊢ ∀ x m• 1. < x ⇒ x ^ m < x ^ (m + 1)
ℝ_ℕ_exp_1_less_mono_thm1	⊢ ∀ x m n• 1. < x ∧ m < n ⇒ x ^ m < x ^ n
ℝ_≤_times_mono_thm	⊢ ∀ x y z• 0. ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
ℝ_ℕ_exp_¬_eq_0_thm	⊢ ∀ m x• ¬ x = 0. ⇒ ¬ x ^ m = 0.
ℝ_ℕ_exp_plus_thm	⊢ ∀ x m n• x ^ (m + n) = x ^ m * x ^ n
ℝ_ℕ_exp_times_thm	⊢ ∀ x y m• (x * y) ^ m = x ^ m * y ^ m
ℝ_ℕ_exp_recip_thm	⊢ ∀ m x• ¬ x = 0. ⇒ (x ^ m) ^-¹ = (x ^-¹) ^ m
ℝ_ℕ_exp_recip_thm1	⊢ ∀ m x• ¬ x = 0. ⇒ (x ^-¹) ^ m = (x ^ m) ^-¹
ℝ_ℕ_exp_1_≤_thm	⊢ ∀ m x• 1. ≤ x ⇒ 1. ≤ x ^ m
ℝ_ℕ_exp_less_1_mono_thm	⊢ ∀ x m• 0. < x ∧ x < 1. ⇒ x ^ (m + 1) < x ^ m
ℝ_ℕ_exp_less_mono_thm	⊢ ∀ x m• 0. < x ⇒ 0. < x ^ m
ℝ_ℕ_exp_less_1_mono_thm1	⊢ ∀ x m n• 0. < x ∧ x < 1. ∧ m < n ⇒ x ^ n < x ^ m
ℝ_ℕ_exp_linear_estimate_thm	⊢ ∀ x m• 0. < x ⇒ 1. + ℕℝ m * x ≤ (1. + x) ^ m
ℝ_0_≤_square_thm	⊢ ∀ x• 0. ≤ x ^ 2
ℝ_square_eq_0_thm	⊢ ∀ x• x ^ 2 = 0. ⇔ x = 0.
ℝ_bound_below_2_thm	⊢ ∀ x y • 0. < x ∧ 0. < y ⇒ (∃ d• 0. < d ∧ d < x ∧ d < y)
ℝ_bound_below_3_thm	⊢ ∀ x y z • 0. < x ∧ 0. < y ∧ 0. < z ⇒ (∃ d• 0. < d ∧ d < x ∧ d < y ∧ d < z)
ℝ_max_2_thm	⊢ ∀ x y• ∃ z• x < z ∧ y < z
ℝ_max_3_thm	⊢ ∀ x y z• ∃ t• x < t ∧ y < t ∧ z < t
ℝ_min_2_thm	⊢ ∀ x y• ∃ z• z < x ∧ z < y
ℝ_min_3_thm	⊢ ∀ x y z• ∃ t• t < x ∧ t < y ∧ t < z
ℝ_archimedean_thm	⊢ ∀ x• ∃ m• x < ℕℝ m
ℝ_archimedean_recip_thm	⊢ ∀ x• 0. < x ⇒ (∃ m• ℕℝ (m + 1) ^-¹ < x)
ℝ_archimedean_times_thm	⊢ ∀ x y• 0. < x ⇒ (∃ m• y < ℕℝ m * x)
ℝ_archimedean_division_thm	⊢ ∀ d y • 0. < d ∧ 0. ≤ y ⇒ (∃ q r• y = ℕℝ q * d + r ∧ 0. ≤ r ∧ r < d)
ℝ_ℕ_exp_tends_to_infinity_thm	⊢ ∀ x y• 1. < x ⇒ (∃ m• y < x ^ m)
ℝ_ℕ_exp_tends_to_0_thm	⊢ ∀ x y• 0. < x ∧ x < 1. ∧ 0. < y ⇒ (∃ m• x ^ m < y)
const_lim_seq_thm	⊢ ∀ c• (λ m• c) -> c
plus_lim_seq_thm	⊢ ∀ s1 c1 s2 c2 • s1 -> c1 ∧ s2 -> c2 ⇒ (λ m• s1 m + s2 m) -> c1 + c2
lim_seq_bounded_thm	⊢ ∀ s c• s -> c ⇒ (∃ b• 0. < b ∧ (∀ m• Abs (s m) < b))
times_lim_seq_thm	⊢ ∀ s1 c1 s2 c2 • s1 -> c1 ∧ s2 -> c2 ⇒ (λ m• s1 m * s2 m) -> c1 * c2
minus_lim_seq_thm	⊢ ∀ s c• s -> c ⇔ (λ m• ~ (s m)) -> ~ c
poly_lim_seq_thm	⊢ ∀ f s t • f ∈ PolyFunc ∧ s -> t ⇒ (λ x• f (s x)) -> f t
recip_lim_seq_thm	⊢ ∀ s t• s -> t ∧ ¬ t = 0. ⇒ (λ m• s m ^-¹) -> t ^-¹
lim_seq_choice_thm	⊢ ∀ p s1 s2 x • s1 -> x ∧ s2 -> x ⇒ (λ m• if p m then s1 m else s2 m) -> x
abs_lim_seq_thm	⊢ ∀ s x• s -> x ⇒ (λ m• Abs (s m)) -> Abs x
lim_seq_recip_ℕ_thm	⊢ ∀ x• (λ m• x + ℕℝ (m + 1) ^-¹) -> x
lim_seq_¬_eq_thm	⊢ ∀ x• ∃ s• s -> x ∧ (∀ m• ¬ s m = x)
lim_seq_shift_thm	⊢ ∀ m s x• s -> x ⇔ (λ n• s (n + m)) -> x
lim_seq_¬_eq_thm1	⊢ ∀ x d • 0. < d ⇒ (∃ s • s -> x ∧ (∀ m• Abs (s m - x) < d ∧ ¬ s m = x))
lim_seq_¬_0_thm	⊢ ∀ s x • s -> x ∧ ¬ x = 0. ⇒ (∃ n• ∀ m• n ≤ m ⇒ ¬ s m = 0.)
lim_seq_upper_bound_thm	⊢ ∀ s b c• (∀ m• s m ≤ b) ∧ s -> c ⇒ c ≤ b
lim_seq_unique_thm	⊢ ∀ s b c• s -> b ∧ s -> c ⇒ b = c
lim_seq_diffs_tend_to_0_thm	⊢ ∀ s c• s -> c ⇒ (λ m• s (m + 1) - s m) -> 0.
cts_lim_seq_thm	⊢ ∀ f x • f Cts x ⇔ (∀ s• s -> x ⇒ (λ m• f (s m)) -> f x)
cts_lim_seq_thm1	⊢ ∀ f x • f Cts x ⇔ (∀ s • s -> x ∧ (∀ m• ¬ s m = x) ⇒ (λ m• f (s m)) -> f x)
cts_lim_seq_thm2	⊢ ∀ f x • f Cts x ⇔ (∃ a b • a < x ∧ x < b ∧ (∀ s • s -> x ∧ (∀ m• ¬ s m = x ∧ a < s m ∧ s m < b) ⇒ (λ m• f (s m)) -> f x))
cts_local_thm	⊢ ∀ f g x a b • a < x ∧ x < b ∧ (∀ y• a < y ∧ y < b ⇒ f y = g y) ∧ g Cts x ⇒ f Cts x
const_cts_thm	⊢ ∀ c t• (λ x• c) Cts t
id_cts_thm	⊢ ∀ t• (λ x• x) Cts t
plus_cts_thm	⊢ ∀ f g t• f Cts t ∧ g Cts t ⇒ (λ x• f x + g x) Cts t
times_cts_thm	⊢ ∀ f g t• f Cts t ∧ g Cts t ⇒ (λ x• f x * g x) Cts t
poly_cts_thm	⊢ ∀ f t• f ∈ PolyFunc ⇒ f Cts t
comp_cts_thm	⊢ ∀ f g t• f Cts g t ∧ g Cts t ⇒ (λ x• f (g x)) Cts t
minus_cts_thm	⊢ ∀ t• ~ Cts t
minus_comp_cts_thm	⊢ ∀ f t• f Cts t ⇒ (λ x• ~ (f x)) Cts t
recip_cts_thm	⊢ ∀ t• ¬ t = 0. ⇒ $^-¹ Cts t
recip_comp_cts_thm	⊢ ∀ f t• f Cts t ∧ ¬ f t = 0. ⇒ (λ x• f x ^-¹) Cts t
ℝ_ℕ_exp_cts_thm	⊢ ∀ m t• (λ x• x ^ m) Cts t
ℝ_ℕ_exp_comp_cts_thm	⊢ ∀ f m t• f Cts t ⇒ (λ x• f x ^ m) Cts t
abs_cts_thm	⊢ ∀ t• Abs Cts t
abs_comp_cts_thm	⊢ ∀ f m t• f Cts t ⇒ (λ x• Abs (f x)) Cts t
cts_extension_thm1	⊢ ∀ a b f • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ⇒ (∃ g • (∀ x• a ≤ x ∧ x ≤ b ⇒ g x = f x) ∧ (∀ x• x < a ⇒ g x = f a) ∧ (∀ x• b < x ⇒ g x = f b) ∧ (∀ x• g Cts x))
cts_extension_thm	⊢ ∀ a b f • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ⇒ (∃ g • (∀ x• a ≤ x ∧ x ≤ b ⇒ g x = f x) ∧ (∀ x• g Cts x))
open_ℝ_delta_thm	⊢ ∀ A • A ∈ Open_R ⇔ (∀ t • t ∈ A ⇒ (∃ d • 0. < d ∧ (∀ y• Abs (y - t) < d ⇒ y ∈ A)))
lim_seq_open_ℝ_thm	⊢ ∀ s x • s -> x ⇔ (∀ A • A ∈ Open_R ∧ x ∈ A ⇒ (∃ n• ∀ m• n ≤ m ⇒ s m ∈ A))
cts_open_ℝ_thm	⊢ ∀ f • (∀ x• f Cts x) ⇔ (∀ A• A ∈ Open_R ⇒ {x\|f x ∈ A} ∈ Open_R)
closed_interval_closed_thm	⊢ ∀ x y• ClosedInterval x y ∈ Closed_R
cts_estimate_thm	⊢ ∀ f x lb ub • f Cts x ∧ (∀ d • 0. < d ⇒ (∃ z• Abs (z - x) < d ∧ lb ≤ f z) ∧ (∃ z• Abs (z - x) < d ∧ f z ≤ ub)) ⇒ lb ≤ f x ∧ f x ≤ ub
cts_estimate_0_thm	⊢ ∀ f x • f Cts x ∧ (∀ d • 0. < d ⇒ (∃ z• Abs (z - x) < d ∧ 0. ≤ f z) ∧ (∃ z• Abs (z - x) < d ∧ f z ≤ 0.)) ⇒ f x = 0.
cts_limit_unique_thm	⊢ ∀ f g x a b • a < x ∧ x < b ∧ f Cts x ∧ g Cts x ∧ (∀ y• a < y ∧ y < b ∧ ¬ y = x ⇒ f y = g y) ⇒ f x = g x
cts_open_interval_thm	⊢ ∀ f a b x • f x ∈ OpenInterval a b ∧ (∀ c d • f x ∈ OpenInterval c d ∧ ClosedInterval c d ⊆ OpenInterval a b ⇒ (∃ s t • x ∈ OpenInterval s t ∧ (∀ y • y ∈ OpenInterval s t ⇒ f y ∈ OpenInterval c d))) ⇒ f Cts x
darboux_cts_mono_thm	⊢ ∀ f a b x • (∀ x y • x ∈ ClosedInterval a b ∧ y ∈ ClosedInterval a b ∧ x < y ⇒ f x < f y) ∧ (∀ y • y ∈ OpenInterval (f a) (f b) ⇒ (∃ x• a < x ∧ x < b ∧ f x = y)) ∧ x ∈ OpenInterval a b ⇒ f Cts x
darboux_cts_mono_thm1	⊢ ∀ f a b x • (∀ x y • x ∈ OpenInterval a b ∧ y ∈ OpenInterval a b ∧ x < y ⇒ f x < f y) ∧ (∀ x y z • x ∈ OpenInterval a b ∧ y ∈ OpenInterval a b ∧ z ∈ OpenInterval (f x) (f y) ⇒ (∃ t• t ∈ OpenInterval a b ∧ f t = z)) ∧ x ∈ OpenInterval a b ⇒ f Cts x
caratheodory_deriv_thm	⊢ ∀ f c x • (f Deriv c) x ⇔ (∃ g • (∀ y• f y - f x = g y * (y - x)) ∧ g Cts x ∧ g x = c)
deriv_cts_thm	⊢ ∀ f c x• (f Deriv c) x ⇒ f Cts x
const_deriv_thm	⊢ ∀ c t• ((λ x• c) Deriv 0.) t
id_deriv_thm	⊢ ∀ t• ((λ x• x) Deriv 1.) t
plus_deriv_thm	⊢ ∀ f1 c1 x f2 c2 • (f1 Deriv c1) x ∧ (f2 Deriv c2) x ⇒ ((λ y• f1 y + f2 y) Deriv c1 + c2) x
plus_const_deriv_thm	⊢ ∀ c x• ($+ c Deriv 1.) x
times_deriv_thm	⊢ ∀ f1 c1 x f2 c2 • (f1 Deriv c1) x ∧ (f2 Deriv c2) x ⇒ ((λ y• f1 y * f2 y) Deriv c1 * f2 x + f1 x * c2) x
times_const_deriv_thm	⊢ ∀ c x• ($* c Deriv c) x
comp_deriv_thm	⊢ ∀ f1 c1 f2 c2 x • (f1 Deriv c1) (f2 x) ∧ (f2 Deriv c2) x ⇒ ((λ y• f1 (f2 y)) Deriv c1 * c2) x
minus_deriv_thm	⊢ ∀ c t• (~ Deriv ~ 1.) t
minus_comp_deriv_thm	⊢ ∀ f c t• (f Deriv c) t ⇒ ((λ x• ~ (f x)) Deriv ~ c) t
ℝ_ℕ_exp_deriv_thm	⊢ ∀ n t • ((λ x• x ^ (n + 1)) Deriv (ℕℝ n + 1.) * t ^ n) t
recip_deriv_thm	⊢ ∀ t• ¬ t = 0. ⇒ ($^-¹ Deriv ~ (t ^-¹ * t ^-¹)) t
recip_comp_deriv_thm	⊢ ∀ f c t • (f Deriv c) t ∧ ¬ f t = 0. ⇒ ((λ x• f x ^-¹) Deriv ~ (f t ^-¹ * f t ^-¹) * c) t
poly_deriv_thm	⊢ ∀ l x • (PolyEval l Deriv PolyEval (DerivCoeffs l) x) x
deriv_local_thm	⊢ ∀ f g x a b c • a < x ∧ x < b ∧ (∀ y• a < y ∧ y < b ⇒ f y = g y) ∧ (g Deriv c) x ⇒ (f Deriv c) x
deriv_lim_fun_thm	⊢ ∀ f c x • (f Deriv c) x ⇔ ((λ y• (f y - f x) / (y - x)) --> c) x
deriv_unique_thm	⊢ ∀ f x c d• (f Deriv c) x ∧ (f Deriv d) x ⇒ c = d
curtain_induction_thm	⊢ ∀ p • (∃ x• p x) ∧ (∀ x• p x ⇒ (∀ y• y < x ⇒ p y)) ∧ (∀ x• ∃ y z• y < x ∧ x < z ∧ (p y ⇒ p z)) ⇒ (∀ x• p x)
bisection_thm	⊢ ∀ p a b • (∀ x y z• x ≤ y ∧ y ≤ z ∧ p x y ∧ p y z ⇒ p x z) ∧ (∀ y • ∃ d • 0. < d ∧ (∀ x z • x ≤ y ∧ y ≤ z ∧ z - x < d ⇒ p x z)) ∧ a ≤ b ⇒ p a b
closed_interval_compact_thm	⊢ ∀ x y• ClosedInterval x y ∈ Compact_R
finite_chain_thm	⊢ ∀ V • V ∈ Finite ∧ ¬ V = {} ∧ (∀ A B• A ∈ V ∧ B ∈ V ⇒ A ⊆ B ∨ B ⊆ A) ⇒ (∃ A• A ∈ V ∧ ⋃ V = A)
cts_compact_maximum_thm	⊢ ∀ X f • ¬ X = {} ∧ X ∈ Compact_R ∧ (∀ x• f Cts x) ⇒ (∃ x• x ∈ X ∧ (∀ z• z ∈ X ⇒ f z ≤ f x))
cts_maximum_thm	⊢ ∀ f a b • a ≤ b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ⇒ (∃ x • a ≤ x ∧ x ≤ b ∧ (∀ z• a ≤ z ∧ z ≤ b ⇒ f z ≤ f x))
cts_abs_bounded_thm	⊢ ∀ f a b • a ≤ b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ⇒ (∃ c• ∀ z• a ≤ z ∧ z ≤ b ⇒ Abs (f z) ≤ c)
intermediate_value_thm	⊢ ∀ f a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ⇒ (∀ y • f a < y ∧ y < f b ∨ f b < y ∧ y < f a ⇒ (∃ x• a < x ∧ x < b ∧ f x = y))
local_min_thm	⊢ ∀ f x a b c • a < x ∧ x < b ∧ (∀ y• a < y ∧ y < b ⇒ f x ≤ f y) ∧ (f Deriv c) x ⇒ c = 0.
local_max_thm	⊢ ∀ f x a b c • a < x ∧ x < b ∧ (∀ y• a < y ∧ y < b ⇒ f y ≤ f x) ∧ (f Deriv c) x ⇒ c = 0.
rolle_thm	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ∧ f a = f b ⇒ (∃ x• a < x ∧ x < b ∧ (f Deriv 0.) x)
cauchy_mean_value_thm	⊢ ∀ f df g dg a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ g Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (g Deriv dg x) x) ⇒ (∃ x • a < x ∧ x < b ∧ dg x * (f b - f a) = df x * (g b - g a))
mean_value_thm	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ⇒ (∃ x • a < x ∧ x < b ∧ f b - f a = (b - a) * df x)
mean_value_thm1	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ (f Deriv df x) x) ⇒ (∃ x • a < x ∧ x < b ∧ f b - f a = (b - a) * df x)
deriv_0_thm1	⊢ ∀ f a b • (∀ x• a < x ∧ x < b ⇒ (f Deriv 0.) x) ⇒ (∀ x y• a < x ∧ x < y ∧ y < b ⇒ f x = f y)
deriv_0_thm	⊢ ∀ f a b • (∀ x• a < x ∧ x < b ⇒ (f Deriv 0.) x) ⇒ (∃ c• ∀ x• a < x ∧ x < b ⇒ f x = c)
deriv_0_thm2	⊢ ∀ f x y• (∀ x• (f Deriv 0.) x) ⇒ f x = f y
deriv_0_less_thm	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ∧ (∀ x• a < x ∧ x < b ⇒ 0. < df x) ⇒ f a < f b
deriv_linear_estimate_thm	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ (f Deriv df x) x) ∧ (∀ x• a < x ∧ x < b ⇒ Abs (df x) ≤ 1.) ⇒ Abs (f b - f a) ≤ b - a
ℝ_mono_inc_seq_thm	⊢ ∀ f • (∀ m• f m ≤ f (m + 1)) ⇒ (∀ m n• f m ≤ f (m + n))
ℝ_mono_dec_seq_thm	⊢ ∀ f • (∀ m• f (m + 1) ≤ f m) ⇒ (∀ m n• f (m + n) ≤ f m)
nested_interval_bounds_thm	⊢ ∀ L U • (∀ m • L m ≤ L (m + 1) ∧ U (m + 1) ≤ U m ∧ L m ≤ U m) ⇒ (∀ m n• L m ≤ U n)
nested_interval_diag_thm	⊢ ∀ X • ∃ L U • ∀ m • L m ≤ L (m + 1) ∧ U (m + 1) ≤ U m ∧ L m < U m ∧ (X m < L m ∨ U m < X m)
nested_interval_intersection_thm	⊢ ∀ L U • (∀ m • L m ≤ L (m + 1) ∧ U (m + 1) ≤ U m ∧ L m ≤ U m) ⇒ (∃ x• ∀ m• L m ≤ x ∧ x ≤ U m)
ℝ_uncountable_thm	⊢ ∀ X• ∃ x• ∀ m• ¬ x = X m
∩_open_interval_thm	⊢ ∀ x1 y1 x2 y2 • ∃ x y • OpenInterval x1 y1 ∩ OpenInterval x2 y2 = OpenInterval x y
∩_closed_interval_thm	⊢ ∀ x1 y1 x2 y2 • ∃ x y • ClosedInterval x1 y1 ∩ ClosedInterval x2 y2 = ClosedInterval x y
⋃_open_ℝ_thm	⊢ ∀ V• V ⊆ Open_R ⇒ ⋃ V ∈ Open_R
∪_open_ℝ_thm	⊢ ∀ X Y• X ∈ Open_R ∧ Y ∈ Open_R ⇒ X ∪ Y ∈ Open_R
∩_open_ℝ_thm	⊢ ∀ X Y• X ∈ Open_R ∧ Y ∈ Open_R ⇒ X ∩ Y ∈ Open_R
⋂_closed_ℝ_thm	⊢ ∀ V• V ⊆ Closed_R ⇒ ⋂ V ∈ Closed_R
∩_closed_ℝ_thm	⊢ ∀ X Y• X ∈ Closed_R ∧ Y ∈ Closed_R ⇒ X ∩ Y ∈ Closed_R
∪_closed_ℝ_thm	⊢ ∀ X Y• X ∈ Closed_R ∧ Y ∈ Closed_R ⇒ X ∪ Y ∈ Closed_R
open_interval_open_thm	⊢ ∀ x y• OpenInterval x y ∈ Open_R
complement_open_interval_thm	⊢ ∀ x y• ~ (OpenInterval x y) = {t\|t ≤ x} ∪ {t\|y ≤ t}
complement_closed_interval_thm	⊢ ∀ x y• ~ (ClosedInterval x y) = {t\|t < x} ∪ {t\|y < t}
half_infinite_intervals_open_thm	⊢ ∀ x• {t\|t < x} ∈ Open_R ∧ {t\|x < t} ∈ Open_R
half_infinite_intervals_closed_thm	⊢ ∀ x• {t\|t ≤ x} ∈ Closed_R ∧ {t\|x ≤ t} ∈ Closed_R
empty_universe_open_closed_thm	⊢ {} ∈ Open_R ∧ Universe ∈ Open_R ∧ {} ∈ Closed_R ∧ Universe ∈ Closed_R
compact_closed_thm	⊢ Compact_R ⊆ Closed_R
compact_min_max_thm	⊢ ∀ X • ¬ X = {} ∧ X ∈ Compact_R ⇒ (∃ L U • L ∈ X ∧ U ∈ X ∧ (∀ x• x ∈ X ⇒ L ≤ x ∧ x ≤ U))
closed_⊆_compact_thm	⊢ ∀ X Y • Y ∈ Closed_R ∧ Y ⊆ X ∧ X ∈ Compact_R ⇒ Y ∈ Compact_R
empty_universe_compact_thm	⊢ {} ∈ Compact_R ∧ ¬ Universe ∈ Compact_R
heine_borel_thm	⊢ ∀ X • X ∈ Compact_R ⇔ X ∈ Closed_R ∧ (∃ L U• ∀ x• x ∈ X ⇒ L ≤ x ∧ x ≤ U)
ℝ_connected_thm	⊢ ∀ X Y • ¬ X = {} ∧ X ∈ Open_R ∧ ¬ Y = {} ∧ Y ∈ Open_R ∧ (∀ x• x ∈ X ∪ Y) ⇒ (∃ x• x ∈ X ∩ Y)
lim_seq_cauchy_seq_thm	⊢ ∀ s x • s -> x ⇒ (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
fin_seq_bounded_thm	⊢ ∀ s n• ∃ b• ∀ m• m ≤ n ⇒ s m < b
cauchy_seq_bounded_above_thm	⊢ ∀ s • (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e)) ⇒ (∃ b• ∀ m• s m < b)
cauchy_seq_bounded_below_thm	⊢ ∀ s • (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e)) ⇒ (∃ b• ∀ m• b < s m)
lim_seq_mono_inc_sup_thm	⊢ ∀ s ub • (∀ m• s m ≤ ub ∧ s m ≤ s (m + 1)) ⇒ s -> Sup {t\|∃ m• t = s m} ∧ (∀ m• s m ≤ Sup {t\|∃ m• t = s m})
lim_seq_mono_inc_thm	⊢ ∀ s ub • (∀ m• s m ≤ ub ∧ s m ≤ s (m + 1)) ⇒ (∃ x• s -> x ∧ (∀ m• s m ≤ x))
lim_seq_mono_dec_thm	⊢ ∀ s lb • (∀ m• lb ≤ s m ∧ s (m + 1) ≤ s m) ⇒ (∃ x• s -> x ∧ (∀ m• x ≤ s m))
lim_sup_thm	⊢ ∀ s lb ub • (∀ m• lb ≤ s m ∧ s m ≤ ub) ⇒ (∃ lim_sup • ∀ e • 0. < e ⇒ (∃ n• ∀ m• n ≤ m ⇒ s m < lim_sup + e) ∧ (∀ n• ∃ m• n ≤ m ∧ lim_sup < s m + e))
lim_inf_thm	⊢ ∀ s lb ub • (∀ m• lb ≤ s m ∧ s m ≤ ub) ⇒ (∃ lim_inf • ∀ e • 0. < e ⇒ (∃ n• ∀ m• n ≤ m ⇒ lim_inf - e < s m) ∧ (∀ n• ∃ m• n ≤ m ∧ s m - e < lim_inf))
cauchy_seq_lim_seq_thm	⊢ ∀ s • (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e)) ⇒ (∃ x• s -> x)
lim_seq_⇔_cauchy_seq_thm	⊢ ∀ s • (∃ x• s -> x) ⇔ (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
lim_fun_lim_seq_thm	⊢ ∀ f c x • (f --> c) x ⇔ (∀ s • s -> x ∧ (∀ m• ¬ s m = x) ⇒ (λ m• f (s m)) -> c)
const_lim_fun_thm	⊢ ∀ c t• ((λ x• c) --> c) t
id_lim_fun_thm	⊢ ∀ t• ((λ x• x) --> t) t
plus_lim_fun_thm	⊢ ∀ f1 t1 x f2 t2 • (f1 --> t1) x ∧ (f2 --> t2) x ⇒ ((λ x• f1 x + f2 x) --> t1 + t2) x
times_lim_fun_thm	⊢ ∀ f1 t1 x f2 t2 • (f1 --> t1) x ∧ (f2 --> t2) x ⇒ ((λ x• f1 x * f2 x) --> t1 * t2) x
recip_lim_fun_thm	⊢ ∀ f t x • (f --> t) x ∧ ¬ t = 0. ⇒ ((λ x• f x ^-¹) --> t ^-¹) x
comp_lim_fun_thm	⊢ ∀ f t x g • (f --> t) x ∧ g Cts t ⇒ ((λ x• g (f x)) --> g t) x
cts_lim_fun_thm	⊢ ∀ f x• f Cts x ⇒ (f --> f x) x
comp_lim_fun_thm1	⊢ ∀ f t x g • (g --> t) (f x) ∧ f Cts x ∧ (∀ y• f y = f x ⇔ y = x) ⇒ ((λ x• g (f x)) --> t) x
poly_lim_fun_thm	⊢ ∀ f x• f ∈ PolyFunc ⇒ (f --> f x) x
lim_fun_upper_bound_thm	⊢ ∀ u d c t x • 0. < d ∧ (∀ y• Abs (y - x) < d ∧ ¬ y = x ⇒ u y ≤ c) ∧ (u --> t) x ⇒ t ≤ c
lim_fun_unique_thm	⊢ ∀ u s t x• (u --> s) x ∧ (u --> t) x ⇒ s = t
lim_fun_local_thm	⊢ ∀ u v s t x a b • (u --> s) x ∧ a < x ∧ x < b ∧ (∀ t• a < t ∧ t < b ∧ ¬ t = x ⇒ u t = v t) ⇒ (v --> s) x
deriv_lim_fun_thm1	⊢ ∀ f c x • (f Deriv c) x ⇔ ((λ y• (f y - f x) * (y - x) ^-¹) --> c) x
comp_lim_fun_thm2	⊢ ∀ f a b t x g • x ∈ OpenInterval a b ∧ (g --> t) (f x) ∧ f Cts x ∧ (∀ y • y ∈ OpenInterval a b ⇒ (f y = f x ⇔ y = x)) ⇒ ((λ x• g (f x)) --> t) x
inverse_deriv_thm	⊢ ∀ f g a b x c • x ∈ OpenInterval a b ∧ (∀ y• y ∈ OpenInterval a b ⇒ f (g y) = y) ∧ (f Deriv c) (g x) ∧ g Cts x ∧ ¬ c = 0. ⇒ (g Deriv c ^-¹) x
const_unif_lim_seq_thm	⊢ ∀ h X• ((λ m• h) ---> h) X
plus_unif_lim_seq_thm	⊢ ∀ u1 h1 X u2 h2 • (u1 ---> h1) X ∧ (u2 ---> h2) X ⇒ ((λ m y• u1 m y + u2 m y) ---> (λ y• h1 y + h2 y)) X
bounded_unif_limit_thm	⊢ ∀ u g X c • (u ---> g) X ∧ (∀ y m• y ∈ X ⇒ Abs (u m y) < c) ⇒ (∃ d• ∀ y• y ∈ X ⇒ Abs (g y) < d)
times_unif_lim_seq_thm	⊢ ∀ u g v h X c d • (u ---> g) X ∧ (v ---> h) X ∧ (∀ y m• y ∈ X ⇒ Abs (u m y) < c) ∧ (∀ y m• y ∈ X ⇒ Abs (v m y) < d) ⇒ ((λ m y• u m y * v m y) ---> (λ y• g y * h y)) X
unif_lim_seq_bounded_thm	⊢ ∀ u h a b • a < b ∧ (u ---> h) (ClosedInterval a b) ∧ (∀ y• a ≤ y ∧ y ≤ b ⇒ h Cts y) ⇒ (∃ c n • ∀ m y• n ≤ m ∧ a ≤ y ∧ y ≤ b ⇒ Abs (u m y) < c)
unif_lim_seq_⊆_thm	⊢ ∀ u h X Y• (u ---> h) X ∧ Y ⊆ X ⇒ (u ---> h) Y
unif_lim_seq_shift_thm	⊢ ∀ m u h X• (u ---> h) X ⇔ ((λ n• u (n + m)) ---> h) X
unif_lim_seq_cts_thm	⊢ ∀ u h x a b • (u ---> h) (OpenInterval a b) ∧ a < x ∧ x < b ∧ (∀ m• u m Cts x) ⇒ h Cts x
unif_lim_seq_cauchy_seq_thm	⊢ ∀ u f X • (u ---> f) X ⇒ (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ (∀ y • y ∈ X ⇒ Abs (u k y - u m y) < e)))
cauchy_seq_unif_lim_seq_thm	⊢ ∀ u X • (∀ e • 0. < e ⇒ (∃ n • ∀ k m • n ≤ k ∧ n ≤ m ⇒ (∀ y • y ∈ X ⇒ Abs (u k y - u m y) < e))) ⇒ (∃ f• (u ---> f) X)
unif_lim_seq_pointwise_lim_seq_thm	⊢ ∀ u f X x• (u ---> f) X ∧ x ∈ X ⇒ (λ m• u m x) -> f x
unif_lim_seq_pointwise_unique_thm	⊢ ∀ u f g X x c • (u ---> f) X ∧ x ∈ X ∧ (λ m• u m x) -> c ⇒ f x = c
unif_lim_seq_unique_thm	⊢ ∀ u f g X x • (u ---> f) X ∧ (u ---> g) X ∧ x ∈ X ⇒ f x = g x
lim_fun_lim_seq_interchange_thm	⊢ ∀ u f a b x s • (u ---> f) (OpenInterval a b \ {x}) ∧ a < x ∧ x < b ∧ (∀ m• (u m --> s m) x) ⇒ (∃ c• (f --> c) x ∧ s -> c)
unif_lim_seq_deriv_estimate_thm	⊢ ∀ du df x0 y0 A B u e • (du ---> df) (OpenInterval A B) ∧ (∀ y m• A < y ∧ y < B ⇒ (u m Deriv du m y) y) ∧ A < x0 ∧ x0 < B ∧ (λ m• u m x0) -> y0 ∧ 0. < e ⇒ (∃ N • ∀ n m x t • N ≤ n ∧ N ≤ m ∧ A < x ∧ x < B ∧ A < t ∧ t < B ⇒ Abs (u n t + ~ (u m t) + ~ (u n x) + u m x) ≤ Abs (t + ~ x) * e)
unif_lim_seq_deriv_thm	⊢ ∀ u du df A B x0 y0 • (du ---> df) (OpenInterval A B) ∧ (∀ y m • y ∈ OpenInterval A B ⇒ (u m Deriv du m y) y) ∧ x0 ∈ OpenInterval A B ∧ (λ m• u m x0) -> y0 ⇒ (∃ f • (u ---> f) (OpenInterval A B) ∧ (∀ y • y ∈ OpenInterval A B ⇒ (f Deriv df y) y))
power_series_series_thm	⊢ ∀ s • PowerSeries s = (λ n x• Series (λ m• s m * x ^ m) n)
series_power_series_thm	⊢ ∀ s• Series s = (λ n• PowerSeries s n 1.)
power_series_0_arg_thm	⊢ (∀ s• PowerSeries s 0 0. = 0.) ∧ (∀ s m• PowerSeries s (m + 1) 0. = s 0)
power_series_limit_0_thm	⊢ ∀ s• (λ m• PowerSeries s m 0.) -> s 0
plus_series_thm	⊢ ∀ s1 s2 • Series (λ m• s1 m + s2 m) = (λ n• Series s1 n + Series s2 n)
series_0_thm	⊢ Series (λ m• 0.) = (λ m• 0.)
const_times_series_thm	⊢ ∀ s c• Series (λ m• c * s m) = (λ n• c * Series s n)
lim_seq_ℕℝ_recip_eq_0_thm	⊢ (λ m• ℕℝ m ^-¹) -> 0.
lim_seq_ℝ_ℕ_exp_eq_0_thm	⊢ ∀ x• ~ 1. < x ∧ x < 1. ⇒ (λ m• x ^ m) -> 0.
series_shift_thm	⊢ ∀ n s • Series (λ m• s (m + n)) = (λ m• Series s (m + n) - Series s n)
lim_series_shift_thm	⊢ ∀ n s x • Series s -> x ⇔ Series (λ m• s (m + n)) -> x - Series s n
lim_series_shift_∃_thm	⊢ ∀ n s • (∃ x• Series s -> x) ⇔ (∃ x• Series (λ m• s (m + n)) -> x)
lim_series_bounded_thm	⊢ ∀ e s c • 0. < e ∧ Series s -> c ⇒ (∃ m• ∀ n• m ≤ n ⇒ Abs (s n) < e)
geometric_sum_thm1	⊢ ∀ n x • ¬ x = 1. ⇒ PolyEval ((λ m• 1.) To (n + 1)) x = (1. - x ^ (n + 1)) / (1. - x)
geometric_sum_thm	⊢ ∀ n x • ¬ x = 1. ⇒ Series (λ m• x ^ m) (n + 1) = (1. - x ^ (n + 1)) / (1. - x)
geometric_series_thm	⊢ ∀ x • ~ 1. < x ∧ x < 1. ⇒ (λ n• PowerSeries (λ m• 1.) n x) -> 1. / (1. - x)
geometric_series_series_thm	⊢ ∀ x • (λ n• PowerSeries (λ m• 1.) n x) = Series (λ m• x ^ m)
geometric_series_thm1	⊢ ∀ x • ~ 1. < x ∧ x < 1. ⇒ Series (λ m• x ^ m) -> 1. / (1. - x)
weierstrass_test_thm	⊢ ∀ u X s c • (∀ m x• x ∈ X ⇒ Abs (u m x) ≤ s m) ∧ Series s -> c ⇒ (∃ f • ((λ m x• Series (λ m• u m x) m) ---> f) X)
comparison_test_thm	⊢ ∀ s1 s2 c2 • (∀ m• Abs (s1 m) ≤ s2 m) ∧ Series s2 -> c2 ⇒ (∃ c1• Series s1 -> c1)
simple_root_test_thm	⊢ ∀ s b m • 0. < b ∧ b < 1. ∧ (∀ n• m ≤ n ⇒ Abs (s n) ≤ b ^ n) ⇒ (∃ c• Series s -> c)
root_test_thm	⊢ ∀ s b d m • b < 1. ∧ (∀ n• m ≤ n ⇒ Abs (s n) ≤ d * b ^ n) ⇒ (∃ c• Series s -> c)
ratio_test_thm1	⊢ ∀ s b m • (∀ m• ¬ s m = 0.) ∧ 0. < b ∧ b < 1. ∧ (∀ n• m ≤ n ⇒ Abs (s (n + 1) / s n) < b) ⇒ (∃ c• Series s -> c)
ratio_test_thm	⊢ ∀ s b • (∀ m• ¬ s m = 0.) ∧ 0. ≤ b ∧ b < 1. ∧ (λ n• Abs (s (n + 1) / s n)) -> b ⇒ (∃ c• Series s -> c)
power_series_convergence_thm	⊢ ∀ s B C b • 0. < B ∧ 0. < b ∧ b < B ∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C ⇒ (∃ f • (PowerSeries s ---> f) (OpenInterval (~ b) b))
power_series_deriv_coeffs_thm	⊢ ∀ s n x • (PowerSeries s (n + 1) Deriv PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) n x) x
power_series_deriv_lemma1	⊢ ∀ b • 0. < b ∧ b < 1. ⇒ (∃ c• Series (λ m• ℕℝ (m + 1) * b ^ m) -> c)
power_series_deriv_lemma2	⊢ ∀ s C b • 0. < b ∧ b < 1. ∧ (λ m• PowerSeries (λ m• Abs (s m)) m 1.) -> C ⇒ (∃ D • (λ m • PowerSeries (λ m• Abs (ℕℝ (m + 1) * s (m + 1))) m b) -> D)
power_series_scale_arg_thm	⊢ ∀ c s m y • PowerSeries s m (c * y) = PowerSeries (λ m• s m * c ^ m) m y
power_series_scale_coeffs_thm	⊢ ∀ c s m y • PowerSeries (λ m• c * s m) m y = c * PowerSeries s m y
power_series_deriv_lim_seq_convergence_thm	⊢ ∀ s B C b • 0. < b ∧ b < B ∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C ⇒ (∃ D • (λ m • PowerSeries (λ m• Abs (ℕℝ (m + 1) * s (m + 1))) m b) -> D)
power_series_deriv_convergence_thm	⊢ ∀ s B C b • 0. < B ∧ 0. < b ∧ b < B ∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C ⇒ (∃ df • (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) ---> df) (OpenInterval (~ b) b))
power_series_main_thm	⊢ ∀ s B C b • 0. < b ∧ b < B ∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C ⇒ (∃ f df • (PowerSeries s ---> f) (OpenInterval (~ b) b) ∧ (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) ---> df) (OpenInterval (~ b) b) ∧ (∀ y • y ∈ OpenInterval (~ b) b ⇒ (f Deriv df y) y))
power_series_main_thm1	⊢ ∀ s b • 0. < b ∧ (∀ x • 0. < x ⇒ (∃ c • (λ m• PowerSeries (λ m• Abs (s m)) m x) -> c)) ⇒ (∃ f df • (PowerSeries s ---> f) (OpenInterval (~ b) b) ∧ (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) ---> df) (OpenInterval (~ b) b) ∧ (∀ y • y ∈ OpenInterval (~ b) b ⇒ (f Deriv df y) y))
power_series_main_thm2	⊢ ∀ s • (∀ x • 0. < x ⇒ (∃ c • (λ m• PowerSeries (λ m• Abs (s m)) m x) -> c)) ⇒ (∃ f df • (∀ x• (λ m• PowerSeries s m x) -> f x) ∧ (∀ x • (λ m • PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) m x) -> df x) ∧ (∀ x• (f Deriv df x) x) ∧ f 0. = s 0)
power_series_main_thm3	⊢ ∀ s • (∀ x • 0. < x ⇒ (∃ c • (λ m• PowerSeries (λ m• Abs (s m)) m x) -> c)) ⇒ (∃ f d1f d2f • (∀ x• (λ m• PowerSeries s m x) -> f x) ∧ (∀ x • (λ m • PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1)) m x) -> d1f x) ∧ (∀ x • (λ m • PowerSeries (λ m • ℕℝ (m + 1) * ℕℝ (m + 2) * s (m + 2)) m x) -> d2f x) ∧ (∀ x• (f Deriv d1f x) x) ∧ (∀ x• (d1f Deriv d2f x) x) ∧ f 0. = s 0 ∧ d1f 0. = s 1)
factorial_linear_estimate_thm	⊢ ∀ m• 1. ≤ ℕℝ (m !) ∧ ℕℝ m ≤ ℕℝ (m !)
factorial_0_less_thm	⊢ ∀ m• 0. < ℕℝ (m !)
factorial_times_recip_thm	⊢ ∀ m• ℕℝ (m + 1) * ℕℝ ((m + 1) !) ^-¹ = ℕℝ (m !) ^-¹
gen_rolle_thm	⊢ ∀ n D a b • a < b ∧ (∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x) ∧ (∀ m x • m ≤ n ∧ a < x ∧ x < b ⇒ (D m Deriv D (m + 1) x) x) ∧ (∀ m• m ≤ n ⇒ D m a = 0.) ∧ D 0 b = 0. ⇒ (∃ x• a < x ∧ x < b ∧ D (n + 1) x = 0.)
taylor_thm	⊢ ∀ n f D a b • a < b ∧ D 0 = f ∧ (∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x) ∧ (∀ m x • m ≤ n ∧ a < x ∧ x < b ⇒ (D m Deriv D (m + 1) x) x) ⇒ (∃ x • a < x ∧ x < b ∧ f b = PowerSeries (λ m• D m a * ℕℝ (m !) ^-¹) (n + 1) (b - a) + D (n + 1) x * (b - a) ^ (n + 1) * ℕℝ ((n + 1) !) ^-¹)
exp_series_convergence_thm	⊢ ∀ x • 0. < x ⇒ (∃ c • (λ m • PowerSeries (λ m• Abs (ℕℝ (m !) ^-¹)) m x) -> c)
exp_consistency_thm	⊢ ∃ f • (∀ y• (f Deriv f y) y) ∧ f 0. = 1. ∧ (∀ x • (λ m• PowerSeries (λ m• ℕℝ (m !) ^-¹) m x) -> f x)
Exp_consistent	⊢ Consistent (λ Exp' • Exp' 0. = 1. ∧ (∀ x• (Exp' Deriv Exp' x) x))
exp_def	⊢ Exp 0. = 1. ∧ (∀ x• (Exp Deriv Exp x) x)
exp_unique_thm	⊢ ∀ f g a b t • (∀ x• x ∈ OpenInterval a b ⇒ ¬ f x = 0.) ∧ (∀ x• x ∈ OpenInterval a b ⇒ (f Deriv f x) x) ∧ (∀ x• x ∈ OpenInterval a b ⇒ (g Deriv g x) x) ∧ t ∈ OpenInterval a b ⇒ (∀ x • x ∈ OpenInterval a b ⇒ g x = g t * f t ^-¹ * f x)
exp_cts_thm	⊢ ∀ x• Exp Cts x
exp_¬_eq_0_thm	⊢ ∀ x• ¬ Exp x = 0.
exp_minus_thm	⊢ ∀ x• Exp (~ x) = Exp x ^-¹
exp_0_less_thm	⊢ ∀ x• 0. < Exp x
exp_plus_thm	⊢ ∀ x y• Exp (x + y) = Exp x * Exp y
exp_clauses	⊢ Exp 0. = 1. ∧ (∀ x• Exp (~ x) = Exp x ^-¹) ∧ (∀ x y• Exp (x + y) = Exp x * Exp y) ∧ (∀ x• 0. < Exp x) ∧ (∀ x• 0. ≤ Exp x)
exp_less_mono_thm	⊢ ∀ x y• x < y ⇔ Exp x < Exp y
exp_power_series_thm	⊢ ∀ x • (λ m• PowerSeries (λ m• ℕℝ (m !) ^-¹) m x) -> Exp x
Log_consistent	⊢ Consistent (λ Log'• ∀ x• Log' (Exp x) = x)
log_def	⊢ ∀ x• Log (Exp x) = x
exp_one_one_thm	⊢ OneOne Exp
exp_ℝ_ℕ_exp_thm	⊢ ∀ m x• Exp (ℕℝ m * x) = Exp x ^ m
exp_0_less_onto_thm	⊢ ∀ x• 0. < x ⇒ (∃ y• x = Exp y)
exp_log_thm	⊢ ∀ x• 0. < x ⇒ Exp (Log x) = x
log_less_mono_thm	⊢ ∀ x y• 0. < x ∧ x < y ⇒ Log x < Log y
log_cts_thm	⊢ ∀ x• 0. < x ⇒ Log Cts x
log_deriv_thm	⊢ ∀ x• 0. < x ⇒ (Log Deriv x ^-¹) x
log_clauses	⊢ Log 1. = 0. ∧ (∀ x• 0. < x ⇒ Log (x ^-¹) = ~ (Log x)) ∧ (∀ x y • 0. < x ∧ 0. < y ⇒ Log (x * y) = Log x + Log y)
ℝ_ℕ_exp_exp_log_thm	⊢ ∀ m x• 0. < x ⇒ x ^ m = Exp (ℕℝ m * Log x)
positive_root_thm	⊢ ∀ m x• ¬ m = 0 ∧ 0. < x ⇒ (∃ y• 0. < y ∧ y ^ m = x)
square_root_thm	⊢ ∀ x• 0. < x ⇔ (∃ y• 0. < y ∧ y ^ 2 = x)
square_root_thm1	⊢ ∀ x• 0. ≤ x ⇔ (∃ y• 0. ≤ y ∧ y ^ 2 = x)
square_root_unique_thm	⊢ ∀ x y• x ^ 2 = y ^ 2 ⇔ x = y ∨ x = ~ y
square_square_root_mono_thm	⊢ ∀ x y• 0. < x ∧ 0. < y ⇒ (x ^ 2 < y ^ 2 ⇔ x < y)
sin_series_convergence_thm	⊢ ∀ x • 0. < x ⇒ (∃ c • (λ m • PowerSeries (λ m • Abs (if m Mod 2 = 0 then 0. else ~ 1. ^ (m Div 2) * ℕℝ (m !) ^-¹)) m x) -> c)
even_odd_thm	⊢ ∀ m• ∃ n• m = 2 * n ∨ m = 2 * n + 1
mod_2_div_2_thm	⊢ ∀ n • (2 * n) Mod 2 = 0 ∧ (2 * n + 1) Mod 2 = 1 ∧ (2 * n) Div 2 = n ∧ (2 * n + 1) Div 2 = n
mod_2_cases_thm	⊢ ∀ m• m Mod 2 = 0 ∨ m Mod 2 = 1
mod_2_0_ℝ_ℕ_exp_thm	⊢ ∀ m x• m Mod 2 = 0 ⇒ ~ x ^ m = x ^ m
mod_2_1_ℝ_ℕ_exp_thm	⊢ ∀ m x• m Mod 2 = 1 ⇒ ~ x ^ m = ~ (x ^ m)
power_series_even_thm	⊢ ∀ s n x • (∀ m• m Mod 2 = 1 ⇒ s m = 0.) ⇒ PowerSeries s n (~ x) = PowerSeries s n x
power_series_odd_thm	⊢ ∀ s n x • (∀ m• m Mod 2 = 0 ⇒ s m = 0.) ⇒ PowerSeries s n (~ x) = ~ (PowerSeries s n x)
sin_deriv_coeffs_thm	⊢ ∀ m • ℕℝ (m + 1) * ℕℝ (m + 2) * (if (m + 2) Mod 2 = 0 then 0. else ~ 1. ^ ((m + 2) Div 2) * ℕℝ ((m + 2) !) ^-¹) = ~ (if m Mod 2 = 0 then 0. else ~ 1. ^ (m Div 2) * ℕℝ (m !) ^-¹)
sin_cos_consistency_thm	⊢ ∃ s c • (∀ y• (s Deriv c y) y) ∧ (∀ y• (c Deriv ~ (s y)) y) ∧ s 0. = 0. ∧ c 0. = 1. ∧ (∀ x • (λ n • PowerSeries (λ m • if m Mod 2 = 0 then 0. else ~ 1. ^ (m Div 2) * ℕℝ (m !) ^-¹) n x) -> s x) ∧ (∀ x • (λ n • PowerSeries (λ m • ℕℝ (m + 1) * (if (m + 1) Mod 2 = 0 then 0. else ~ 1. ^ ((m + 1) Div 2) * ℕℝ ((m + 1) !) ^-¹)) n x) -> c x)
Sin_consistent Cos_consistent	⊢ Consistent (λ (Sin', Cos') • Sin' 0. = 0. ∧ Cos' 0. = 1. ∧ (∀ x• (Sin' Deriv Cos' x) x) ∧ (∀ x• (Cos' Deriv ~ (Sin' x)) x))
sin_def cos_def	⊢ Sin 0. = 0. ∧ Cos 0. = 1. ∧ (∀ x• (Sin Deriv Cos x) x) ∧ (∀ x• (Cos Deriv ~ (Sin x)) x)
sin_cos_cts_thm	⊢ ∀ x• Sin Cts x ∧ Cos Cts x
cos_squared_plus_sin_squared_thm	⊢ ∀ x• Cos x ^ 2 + Sin x ^ 2 = 1.
sin_cos_unique_lemma1	⊢ ∀ f g x • (∀ x• (f Deriv g x) x) ∧ (∀ x• (g Deriv ~ (f x)) x) ⇒ Cos x * g x + Sin x * f x = g 0. ∧ Cos x * f x - Sin x * g x = f 0.
sin_cos_unique_lemma2	⊢ ∀ f g x • (∀ x• (f Deriv g x) x) ∧ (∀ x• (g Deriv ~ (f x)) x) ⇒ f x = f 0. * Cos x + g 0. * Sin x ∧ g x = g 0. * Cos x - f 0. * Sin x
sin_cos_unique_thm	⊢ ∀ f g x • f 0. = 0. ∧ g 0. = 1. ∧ (∀ x• (f Deriv g x) x) ∧ (∀ x• (g Deriv ~ (f x)) x) ⇒ f x = Sin x ∧ g x = Cos x
sin_cos_power_series_thm	⊢ ∀ x • (λ n • PowerSeries (λ m • if m Mod 2 = 0 then 0. else ~ 1. ^ (m Div 2) * ℕℝ (m !) ^-¹) n x) -> Sin x ∧ (λ n • PowerSeries (λ m • ℕℝ (m + 1) * (if (m + 1) Mod 2 = 0 then 0. else ~ 1. ^ ((m + 1) Div 2) * ℕℝ ((m + 1) !) ^-¹)) n x) -> Cos x
sin_cos_plus_thm	⊢ ∀ x y • Sin (x + y) = Sin x * Cos y + Cos x * Sin y ∧ Cos (x + y) = Cos x * Cos y - Sin x * Sin y
sin_cos_minus_thm	⊢ ∀ x• Sin (~ x) = ~ (Sin x) ∧ Cos (~ x) = Cos x
sin_0_group_thm	⊢ 0. ∈ {x\|Sin x = 0.} ∧ (∀ x y • x ∈ {x\|Sin x = 0.} ∧ y ∈ {x\|Sin x = 0.} ⇒ x + y ∈ {x\|Sin x = 0.}) ∧ (∀ x• x ∈ {x\|Sin x = 0.} ⇒ ~ x ∈ {x\|Sin x = 0.})
sin_0_ℕℝ_times_thm	⊢ ∀ x m• Sin x = 0. ⇒ Sin (ℕℝ m * x) = 0.
sin_eq_cos_sin_cos_twice_thm	⊢ ∀ x • Sin x = Cos x ⇒ Sin (2. * x) = 1. ∧ Cos (2. * x) = 0.
sum_squares_abs_bound_thm	⊢ ∀ x y z• x ^ 2 + y ^ 2 = z ^ 2 ⇒ Abs x ≤ Abs z
sum_squares_abs_bound_thm1	⊢ ∀ x y• x ^ 2 + y ^ 2 = 1. ⇒ Abs x ≤ 1.
abs_sin_abs_cos_≤_1_thm	⊢ ∀ x• Abs (Sin x) ≤ 1. ∧ Abs (Cos x) ≤ 1.
cos_positive_estimate_thm	⊢ ∀ x• x ∈ OpenInterval 0. 1. ⇒ 0. < Cos x
sin_positive_estimate_thm	⊢ ∀ x• x ∈ OpenInterval 0. 2. ⇒ 0. < Sin x
cos_greater_root_2_thm	⊢ ∀ t • 0. < t ∧ (∀ x• 0. < x ∧ x < t ⇒ 1 / 2 < Cos x ^ 2) ⇒ t ^ 2 ≤ 2.
cos_squared_eq_half_thm	⊢ ∀ e • 0. < e ⇒ (∃ x • 0. < x ∧ x ^ 2 < 2. + e ∧ 0. < Cos x ∧ Cos x ^ 2 = 1 / 2)
sin_eq_cos_exists_thm	⊢ ∃ x• x ∈ OpenInterval 0. 2. ∧ Sin x = Cos x
sin_positive_zero_thm	⊢ ∃ x• 0. < x ∧ Sin x = 0.
ℝ_discrete_subgroup_thm	⊢ ∀ G h a • 0. ∈ G ∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G) ∧ (∀ g• g ∈ G ⇒ ~ g ∈ G) ∧ 0. < h ∧ h ∈ G ∧ 0. < a ∧ (∀ h• 0. < h ∧ h ∈ G ⇒ a < h) ⇒ (∃ g • 0. < g ∧ g ∈ G ∧ (∀ h • 0. < h ∧ h ∈ G ⇒ (∃ m• h = ℕℝ m * g)))
pi_consistency_thm	⊢ ∃ pi • 0. < pi ∧ Sin pi = 0. ∧ (∀ x • 0. < x ∧ Sin x = 0. ⇒ (∃ m• x = ℕℝ m * pi))
ArchimedesConstant_consistent	⊢ Consistent (λ ArchimedesConstant' • 0. < ArchimedesConstant' ∧ (∀ x • Sin x = 0. ⇔ (∃ m• x = ℕℝ m * ArchimedesConstant') ∨ (∃ m • x = ~ (ℕℝ m * ArchimedesConstant'))))
π_def	⊢ 0. < π ∧ (∀ x • Sin x = 0. ⇔ (∃ m• x = ℕℝ m * π) ∨ (∃ m• x = ~ (ℕℝ m * π)))
ℕℝ_plus_1_times_bound_thm	⊢ (∀ c m• 0. < c ⇒ c ≤ ℕℝ (m + 1) * c) ∧ (∀ c m• c < 0. ⇒ ℕℝ (m + 1) * c ≤ c)
ℕℝ_0_less_¬_ℕℝ_times_π_thm	⊢ ∀ x m• 0. < x ⇒ ¬ x = ~ (ℕℝ m * π)
sin_¬_eq_0_thm	⊢ ∀ x• 0. < x ∧ x < π ⇒ ¬ Sin x = 0.
sin_0_π_0_less_thm	⊢ ∀ x• x ∈ OpenInterval 0. π ⇒ 0. < Sin x
sin_cos_π_over_2_thm	⊢ Sin (1 / 2 * π) = 1. ∧ Cos (1 / 2 * π) = 0.
sin_cos_plus_π_over_2_thm	⊢ ∀ x • Sin (x + 1 / 2 * π) = Cos x ∧ Cos (x + 1 / 2 * π) = ~ (Sin x)
cos_¬_eq_0_thm	⊢ ∀ x• ~ (1 / 2) * π < x ∧ x < 1 / 2 * π ⇒ ¬ Cos x = 0.
cos_eq_0_thm	⊢ ∀ x • Cos x = 0. ⇔ (∃ m• x = 1 / 2 * π + ℕℝ m * π) ∨ (∃ m• x = 1 / 2 * π - ℕℝ m * π)
sin_cos_plus_π_thm	⊢ ∀ x • Sin (x + π) = ~ (Sin x) ∧ Cos (x + π) = ~ (Cos x)
sin_cos_π_thm	⊢ Sin π = 0. ∧ Cos π = ~ 1.
sin_cos_plus_2_π_thm	⊢ ∀ x • Sin (x + 2. * π) = Sin x ∧ Cos (x + 2. * π) = Cos x
sin_cos_2_π_thm	⊢ Sin (2. * π) = 0. ∧ Cos (2. * π) = 1.
sin_cos_plus_even_times_π_thm	⊢ ∀ x m • Sin (x + ℕℝ (2 * m) * π) = Sin x ∧ Cos (x + ℕℝ (2 * m) * π) = Cos x
sin_cos_even_times_π_thm	⊢ ∀ m • Sin (ℕℝ (2 * m) * π) = 0. ∧ Cos (ℕℝ (2 * m) * π) = 1.
sin_cos_period_thm	⊢ ∀ x y • x < y ⇒ (Sin x = Sin y ∧ Cos x = Cos y ⇔ (∃ m• y = x + ℕℝ (2 * m) * π))
sin_cos_onto_unit_circle_thm	⊢ ∀ x y • x ^ 2 + y ^ 2 = 1. ⇒ (∃ z • 0. ≤ z ∧ z < 2. * π ∧ x = Cos z ∧ y = Sin z)
sin_cos_onto_unit_circle_thm1	⊢ ∀ x y • x ^ 2 + y ^ 2 = 1. ⇒ (∃₁ z • 0. ≤ z ∧ z < 2. * π ∧ x = Cos z ∧ y = Sin z)
lim_right_lim_seq_thm	⊢ ∀ f c x • (f +#-> c) x ⇔ (∀ s • s -> x ∧ (∀ m• x < s m) ⇒ (λ m• f (s m)) -> c)
lim_fun_lim_right_thm	⊢ ∀ f c x • (f --> c) x ⇔ (f +#-> c) x ∧ ((λ y• f (~ y)) +#-> c) (~ x)
const_lim_right_thm	⊢ ∀ c x• ((λ x• c) +#-> c) x
id_lim_right_thm	⊢ ∀ x• ((λ x• x) +#-> x) x
plus_lim_right_thm	⊢ ∀ f1 c1 f2 c2 x • (f1 +#-> c1) x ∧ (f2 +#-> c2) x ⇒ ((λ x• f1 x + f2 x) +#-> c1 + c2) x
times_lim_right_thm	⊢ ∀ f1 c1 f2 c2 x • (f1 +#-> c1) x ∧ (f2 +#-> c2) x ⇒ ((λ x• f1 x * f2 x) +#-> c1 * c2) x
poly_lim_right_thm	⊢ ∀ f g c x • f ∈ PolyFunc ∧ (g +#-> c) x ⇒ ((λ x• f (g x)) +#-> f c) x
recip_lim_right_thm	⊢ ∀ f c x • (f +#-> c) x ∧ ¬ c = 0. ⇒ ((λ x• f x ^-¹) +#-> c ^-¹) x
lim_right_unique_thm	⊢ ∀ f c d x• (f +#-> c) x ∧ (f +#-> d) x ⇒ c = d
cts_lim_right_thm	⊢ ∀ f c x• f Cts x ∧ (f +#-> c) x ⇒ f x = c
lim_infinity_lim_seq_thm	⊢ ∀ f c • f -+#> c ⇔ (∀ s• (∀ m• ℕℝ m ≤ s m) ⇒ (λ m• f (s m)) -> c)
lim_infinity_lim_right_thm	⊢ ∀ f c• f -+#> c ⇔ ((λ x• f (x ^-¹)) +#-> c) 0.
lim_right_lim_infinity_thm	⊢ ∀ f c• ((λ x• f (x ^-¹)) +#-> c) 0. ⇔ f -+#> c
const_lim_infinity_thm	⊢ ∀ c• (λ x• c) -+#> c
id_lim_infinity_thm	⊢ ∀ c• ¬ (λ x• x) -+#> c
plus_lim_infinity_thm	⊢ ∀ f1 c1 f2 c2 • f1 -+#> c1 ∧ f2 -+#> c2 ⇒ (λ x• f1 x + f2 x) -+#> c1 + c2
times_lim_infinity_thm	⊢ ∀ f1 c1 f2 c2 • f1 -+#> c1 ∧ f2 -+#> c2 ⇒ (λ x• f1 x * f2 x) -+#> c1 * c2
poly_lim_infinity_thm	⊢ ∀ f g c • f ∈ PolyFunc ∧ g -+#> c ⇒ (λ x• f (g x)) -+#> f c
recip_lim_infinity_thm	⊢ ∀ f c • f -+#> c ∧ ¬ c = 0. ⇒ (λ x• f x ^-¹) -+#> c ^-¹
recip_lim_infinity_0_thm	⊢ (λ x• x ^-¹) -+#> 0.
lim_infinity_unique_thm	⊢ ∀ f c d• f -+#> c ∧ f -+#> d ⇒ c = d
div_infinity_pos_thm	⊢ ∀ f • f -+#>+# ⇒ (∃ b• 0. < b ∧ (∀ x• b < x ⇒ 0. < f x))
const_plus_div_infinity_thm	⊢ ∀ f c• f -+#>+# ⇒ (λ x• c + f x) -+#>+#
id_div_infinity_thm	⊢ (λ x• x) -+#>+#
plus_div_infinity_thm	⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f x + g x) -+#>+#
const_times_div_infinity_thm	⊢ ∀ f c• f -+#>+# ∧ 0. < c ⇒ (λ x• c * f x) -+#>+#
times_div_infinity_thm	⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f x * g x) -+#>+#
power_div_infinity_thm	⊢ ∀ m• (λ x• x ^ (m + 1)) -+#>+#
less_div_infinity_thm	⊢ ∀ f g a • f -+#>+# ∧ (∀ x• a < x ⇒ f x < g x) ⇒ g -+#>+#
bounded_deriv_div_infinity_thm	⊢ ∀ f df a c • 0. < c ∧ (∀ x• a ≤ x ⇒ (f Deriv df x) x) ∧ (∀ x• a ≤ x ⇒ c < df x) ⇒ f -+#>+#
exp_div_infinity_thm	⊢ Exp -+#>+#
log_div_infinity_thm	⊢ Log -+#>+#
div_infinity_times_recip_thm	⊢ ∀ f a e • f -+#>+# ∧ 0. < a ∧ 0. < e ⇒ (∃ b• ∀ x• b < x ⇒ a * f x ^-¹ < e)
div_infinity_lim_right_thm	⊢ ∀ f • f -+#>+# ⇔ ((λ x• f (x ^-¹) ^-¹) +#-> 0.) 0. ∧ (∃ b• ∀ x• b < x ⇒ 0. < f x)
div_infinity_lim_infinity_thm	⊢ ∀ f • f -+#>+# ⇔ (λ x• f x ^-¹) -+#> 0. ∧ (∃ b• ∀ x• b < x ⇒ 0. < f x)
comp_div_infinity_thm	⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f (g x)) -+#>+#
rolle_thm1	⊢ ∀ f df a b • a < b ∧ (∀ x• a ≤ x ∧ x < b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ∧ (∀ x• a < x ∧ x < b ⇒ ¬ df x = 0.) ⇒ (∀ x• a < x ∧ x < b ⇒ ¬ f x = f a)
l'hopital_lim_right_thm	⊢ ∀ f df g dg a b c • a < b ∧ f a = 0. ∧ g a = 0. ∧ (∀ x• a ≤ x ∧ x < b ⇒ f Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x) ∧ (∀ x• a ≤ x ∧ x < b ⇒ g Cts x) ∧ (∀ x• a < x ∧ x < b ⇒ (g Deriv dg x) x) ∧ (∀ x• a < x ∧ x < b ⇒ ¬ dg x = 0.) ∧ ((λ x• df x * dg x ^-¹) +#-> c) a ⇒ ((λ x• f x * g x ^-¹) +#-> c) a
cts_comp_minus_thm	⊢ ∀ f x• (λ x• f (~ x)) Cts x ⇔ f Cts ~ x
deriv_comp_minus_thm	⊢ ∀ f df x • ((λ x• f (~ x)) Deriv ~ (df (~ x))) x ⇔ (f Deriv df (~ x)) (~ x)
l'hopital_lim_fun_thm	⊢ ∀ f df g dg a b c x • a < x ∧ x < b ∧ f x = 0. ∧ g x = 0. ∧ (∀ y• a < y ∧ y < b ⇒ f Cts y) ∧ (∀ y • a < y ∧ y < b ∧ ¬ y = x ⇒ (f Deriv df y) y) ∧ (∀ y• a < y ∧ y < b ⇒ g Cts y) ∧ (∀ y • a < y ∧ y < b ∧ ¬ y = x ⇒ (g Deriv dg y) y) ∧ (∀ y• a < y ∧ y < b ⇒ ¬ dg y = 0.) ∧ ((λ y• df y * dg y ^-¹) --> c) x ⇒ ((λ y• f y * g y ^-¹) --> c) x
l'hopital_lim_infinity_thm	⊢ ∀ f df g dg a c • g -+#>+# ∧ (∀ x• a < x ⇒ (f Deriv df x) x) ∧ (∀ x• a < x ⇒ (g Deriv dg x) x) ∧ (∀ x• a < x ⇒ ¬ dg x = 0.) ∧ (λ x• df x * dg x ^-¹) -+#> c ⇒ (λ x• f x * g x ^-¹) -+#> c
cts_deriv_deriv_thm	⊢ ∀ f df a b t • (∀ x • x ∈ OpenInterval a b \ {t} ⇒ (f Deriv df x) x) ∧ (∀ x• x ∈ OpenInterval a b ⇒ df Cts x) ∧ f Cts t ∧ t ∈ OpenInterval a b ⇒ (∀ x• x ∈ OpenInterval a b ⇒ (f Deriv df x) x)
lim_fun_id_over_sin_thm	⊢ ((λ x• x * Sin x ^-¹) --> 1.) 0.
lim_infinity_recip_exp_thm	⊢ (λ x• Exp x ^-¹) -+#> 0.
lim_infinity_id_over_exp_thm	⊢ (λ x• x * Exp x ^-¹) -+#> 0.
lim_fun_power_over_exp_thm	⊢ ∀ m• (λ x• x ^ m * Exp x ^-¹) -+#> 0.
lim_infinity_log_over_id_thm	⊢ (λ x• Log x * x ^-¹) -+#> 0.
lim_fun_log_over_id_minus_1_thm	⊢ ((λ x• Log x * (x - 1.) ^-¹) --> 1.) 1.
lim_fun_log_1_plus_over_id_thm	⊢ ((λ x• Log (1. + x) * x ^-¹) --> 1.) 0.
lim_fun_e_thm	⊢ ((λ x• Exp (x ^-¹ * Log (1. + x))) --> Exp 1.) 0.
lim_seq_e_thm	⊢ (λ m• (1. + ℕℝ m ^-¹) ^ m) -> Exp 1.
ℝ_less_mono_⇔_thm	⊢ ∀ f • (∀ x y• x < y ⇒ f x < f y) ⇔ (∀ x y• f x < f y ⇔ x < y)
ℝ_less_mono_⇔_≤_thm	⊢ ∀ f • (∀ x y• x < y ⇒ f x < f y) ⇔ (∀ x y• f x ≤ f y ⇔ x ≤ y)
ℝ_less_mono_one_one_thm	⊢ ∀ f • (∀ x y• x < y ⇒ f x < f y) ⇒ (∀ x y• f x = f y ⇔ x = y)
total_inverse_cts_thm	⊢ ∀ f g x • (∀ x y• x < y ⇒ f x < f y) ∧ (∀ x• g (f x) = x) ∧ (∀ y• f (g y) = y) ⇒ g Cts f x
total_inverse_thm	⊢ ∀ f • (∀ x y• x < y ⇒ f x < f y) ∧ (∀ y• ∃ x• f x = y) ⇒ (∃ g • (∀ x• g (f x) = x) ∧ (∀ y• f (g y) = y) ∧ (∀ y• g Cts y) ∧ (∀ x y• x < y ⇒ g x < g y))
closed_half_infinite_inverse_thm1	⊢ ∀ f a • (∀ x• a ≤ x ⇒ f Cts x) ∧ (∀ x y• a ≤ x ∧ x < y ⇒ f x < f y) ∧ (∀ y• f a ≤ y ⇒ (∃ x• a ≤ x ∧ f x = y)) ⇒ (∃ g • (∀ x• a ≤ x ⇒ g (f x) = x) ∧ (∀ y• f a ≤ y ⇒ f (g y) = y) ∧ (∀ y• g Cts y) ∧ (∀ x y• x < y ⇒ g x < g y))
closed_half_infinite_inverse_thm	⊢ ∀ f df a • (∀ x• a ≤ x ⇒ f Cts x) ∧ (∀ x• a < x ⇒ (f Deriv df x) x) ∧ (∀ x• a < x ⇒ 0. < df x) ∧ (∀ y• f a ≤ y ⇒ (∃ x• a ≤ x ∧ f x = y)) ⇒ (∃ g • (∀ x• a ≤ x ⇒ g (f x) = x) ∧ (∀ y• f a ≤ y ⇒ f (g y) = y) ∧ (∀ y• g Cts y) ∧ (∀ x y• x < y ⇒ g x < g y))
cond_cts_thm	⊢ ∀ f g y • f Cts y ∧ g Cts y ∧ f y = g y ⇒ (λ z• if z ≤ y then f z else g z) Cts y
cond_cts_thm1	⊢ ∀ f g a b y x • (∀ x• x ∈ ClosedInterval a y ⇒ f Cts x) ∧ (∀ x• x ∈ ClosedInterval y b ⇒ g Cts x) ∧ f y = g y ∧ x ∈ ClosedInterval a b ⇒ (λ z• if z ≤ y then f z else g z) Cts x
closed_interval_inverse_thm	⊢ ∀ f df a b • a < b ∧ (∀ x• x ∈ ClosedInterval a b ⇒ f Cts x) ∧ (∀ x • x ∈ OpenInterval a b ⇒ (f Deriv df x) x) ∧ (∀ x• x ∈ OpenInterval a b ⇒ 0. < df x) ⇒ (∃ g • (∀ x• x ∈ ClosedInterval a b ⇒ g (f x) = x) ∧ (∀ y • y ∈ ClosedInterval (f a) (f b) ⇒ f (g y) = y) ∧ (∀ y• g Cts y) ∧ (∀ x y• x < y ⇒ g x < g y))
Sqrt_consistent	⊢ Consistent (λ Sqrt' • ∀ x • 0. ≤ x ⇒ 0. ≤ Sqrt' x ∧ Sqrt' x ^ 2 = x ∧ Sqrt' Cts x)
sqrt_def	⊢ ∀ x • 0. ≤ x ⇒ 0. ≤ Sqrt x ∧ Sqrt x ^ 2 = x ∧ Sqrt Cts x
sqrt_thm	⊢ ∀ x• 0. ≤ x ⇒ Sqrt x ^ 2 = x
sqrt_0_≤_thm	⊢ ∀ x• 0. ≤ x ⇒ 0. ≤ Sqrt x
sqrt_cts_thm	⊢ ∀ x• 0. ≤ x ⇒ Sqrt Cts x
sqrt_square_thm	⊢ ∀ x• Sqrt (x ^ 2) = Abs x
square_sqrt_thm	⊢ ∀ x y• x = y ^ 2 ⇒ Sqrt x = Abs y
sqrt_0_1_thm	⊢ Sqrt 0. = 0. ∧ Sqrt 1. = 1.
square_times_thm	⊢ ∀ x y• (x * y) ^ 2 = x ^ 2 * y ^ 2
sqrt_times_thm	⊢ ∀ x y • 0. ≤ x ∧ 0. ≤ y ⇒ Sqrt (x * y) = Sqrt x * Sqrt y
square_recip_thm	⊢ ∀ x• ¬ x = 0. ⇒ (x ^-¹) ^ 2 = (x ^ 2) ^-¹
sqrt_pos_thm	⊢ ∀ x• 0. < x ⇒ 0. < Sqrt x
sqrt_recip_thm	⊢ ∀ x• 0. < x ⇒ Sqrt (x ^-¹) = Sqrt x ^-¹
sqrt_exp_log_thm	⊢ ∀ x• 0. < x ⇒ Sqrt x = Exp (1 / 2 * Log x)
sqrt_deriv_thm	⊢ ∀ x• 0. < x ⇒ (Sqrt Deriv 1 / 2 * Sqrt x * x ^-¹) x
sqrt_mono_thm	⊢ ∀ x y• 0. ≤ x ∧ x < y ⇒ Sqrt x < Sqrt y
square_mono_≤_thm	⊢ ∀ x y• 0. ≤ x ∧ 0. ≤ y ⇒ (x ≤ y ⇔ x ^ 2 ≤ y ^ 2)
id_over_sqrt_thm	⊢ ∀ x• 0. < x ⇒ x * Sqrt x ^-¹ = Sqrt x
sqrt_1_minus_sin_squared_thm	⊢ ∀ x• Sqrt (1. - Sin x ^ 2) = Abs (Cos x)
sqrt_1_minus_cos_squared_thm	⊢ ∀ x• Sqrt (1. - Cos x ^ 2) = Abs (Sin x)
tan_deriv_thm	⊢ ∀ x• ¬ Cos x = 0. ⇒ (Tan Deriv 1. + Tan x ^ 2) x
cotan_deriv_thm	⊢ ∀ x • ¬ Sin x = 0. ⇒ (Cotan Deriv ~ (1. + Cotan x ^ 2)) x
sec_deriv_thm	⊢ ∀ x• ¬ Cos x = 0. ⇒ (Sec Deriv Sec x * Tan x) x
cosec_deriv_thm	⊢ ∀ x • ¬ Sin x = 0. ⇒ (Cosec Deriv ~ (Cosec x) * Cotan x) x
cos_0_less_thm	⊢ ∀ x• ~ (1 / 2) * π < x ∧ x < 1 / 2 * π ⇒ 0. < Cos x
ArcSin_consistent	⊢ Consistent (λ ArcSin' • (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin' (Sin x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Sin (ArcSin' x) = x ∧ ArcSin' Cts x))
arc_sin_def	⊢ (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin (Sin x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Sin (ArcSin x) = x ∧ ArcSin Cts x)
sin_arc_sin_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ Sin (ArcSin x) = x
arc_sin_sin_thm	⊢ ∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin (Sin x) = x
arc_sin_cts_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ ArcSin Cts x
abs_arc_sin_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ Abs (ArcSin x) ≤ 1 / 2 * π
cos_arc_sin_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ Cos (ArcSin x) = Sqrt (1. - x ^ 2)
arc_sin_1_minus_1_thm	⊢ ArcSin 1. = 1 / 2 * π ∧ ArcSin (~ 1.) = ~ (1 / 2) * π
arc_sin_deriv_thm	⊢ ∀ x • Abs x < 1. ⇒ (ArcSin Deriv Sqrt (1. - x ^ 2) ^-¹) x
ArcCos_consistent	⊢ Consistent (λ ArcCos' • (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos' (Cos x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Cos (ArcCos' x) = x ∧ ArcCos' Cts x))
arc_cos_def	⊢ (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos (Cos x) = x) ∧ (∀ x • Abs x ≤ 1. ⇒ Cos (ArcCos x) = x ∧ ArcCos Cts x)
cos_arc_cos_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ Cos (ArcCos x) = x
arc_cos_cos_thm	⊢ ∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos (Cos x) = x
arc_cos_cts_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ ArcCos Cts x
abs_arc_cos_thm	⊢ ∀ x• Abs x ≤ 1. ⇒ 0. ≤ ArcCos x ∧ ArcCos x ≤ π
sinh_deriv_thm	⊢ ∀ x• (Sinh Deriv Cosh x) x
cosh_deriv_thm	⊢ ∀ x• (Cosh Deriv Sinh x) x
cosh_0_less_thm	⊢ ∀ x• 0. < Cosh x
cosh_non_0_thm	⊢ ∀ x• ¬ Cosh x = 0.
sinh_non_0_thm	⊢ ∀ x• Sinh x = 0. ⇔ x = 0.
cosh_squared_minus_sinh_squared_thm	⊢ ∀ x• Cosh x ^ 2 - Sinh x ^ 2 = 1.
tanh_deriv_thm	⊢ ∀ x• (Tanh Deriv 1. - Tanh x ^ 2) x
cotanh_deriv_thm	⊢ ∀ x• ¬ x = 0. ⇒ (Cotanh Deriv 1. - Cotanh x ^ 2) x
sech_deriv_thm	⊢ ∀ x• (Sech Deriv ~ (Sech x) * Tanh x) x
cosech_deriv_thm	⊢ ∀ x • ¬ x = 0. ⇒ (Cosech Deriv ~ (Cosech x) * Cotanh x) x
sinh_cts_thm	⊢ ∀ x• Sinh Cts x
cosh_cts_thm	⊢ ∀ x• Cosh Cts x
sinh_mono_thm	⊢ ∀ x y• x < y ⇒ Sinh x < Sinh y
sinh_cosh_0_thm	⊢ Sinh 0. = 0. ∧ Cosh 0. = 1.
sinh_cosh_minus_thm	⊢ ∀ x• Sinh (~ x) = ~ (Sinh x) ∧ Cosh (~ x) = Cosh x
ArcSinh_consistent	⊢ Consistent (λ ArcSinh' • ∀ x • ArcSinh' (Sinh x) = x ∧ Sinh (ArcSinh' x) = x ∧ ArcSinh' Cts x)
arc_sinh_def	⊢ ∀ x • ArcSinh (Sinh x) = x ∧ Sinh (ArcSinh x) = x ∧ ArcSinh Cts x
sqrt_1_plus_sinh_squared_thm	⊢ ∀ x• Sqrt (1. + Sinh x ^ 2) = Cosh x
cosh_arc_sinh_thm	⊢ ∀ x• Cosh (ArcSinh x) = Sqrt (1. + x ^ 2)
arc_sinh_deriv_thm	⊢ ∀ x• (ArcSinh Deriv Sqrt (1. + x ^ 2) ^-¹) x
gauge_∩_thm	⊢ ∀ G1 G2 • G1 ∈ Gauge ∧ G2 ∈ Gauge ⇒ (λ x• G1 x ∩ G2 x) ∈ Gauge
gauge_o_minus_thm	⊢ ∀ G• G ∈ Gauge ⇒ (λ x• {t\|~ t ∈ G (~ x)}) ∈ Gauge
gauge_o_plus_thm	⊢ ∀ G h • G ∈ Gauge ⇒ (λ x• {t\|t + h ∈ G (x + h)}) ∈ Gauge
gauge_o_times_thm	⊢ ∀ c G • G ∈ Gauge ∧ ¬ c = 0. ⇒ (λ x• {t\|c * t ∈ G (c * x)}) ∈ Gauge
gauge_refinement_thm	⊢ ∀ G1 G2 • G1 ∈ Gauge ∧ G2 ∈ Gauge ⇒ (∃ G • G ∈ Gauge ∧ (∀ x• G x ⊆ G1 x) ∧ (∀ x• G x ⊆ G2 x))
gauge_refine_3_thm	⊢ ∀ G1 G2 G3 • G1 ∈ Gauge ∧ G2 ∈ Gauge ∧ G3 ∈ Gauge ⇒ (∃ G • G ∈ Gauge ∧ (∀ x• G x ⊆ G1 x) ∧ (∀ x• G x ⊆ G2 x) ∧ (∀ x• G x ⊆ G3 x))
fine_refinement_thm	⊢ ∀ G1 G2 t I n • (∀ x• G1 x ⊆ G2 x) ∧ (t, I, n) ∈ G1 Fine ⇒ (t, I, n) ∈ G2 Fine
chosen_tag_thm	⊢ ∀ a • ∃ G1 • G1 ∈ Gauge ∧ (∀ G2 • G2 ∈ Gauge ∧ (∀ x• G2 x ⊆ G1 x) ⇒ (∀ t I n m • m < n ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G2 Fine ∧ a ∈ ClosedInterval (I m) (I (m + 1)) ⇒ t m = a))
chosen_tags_thm	⊢ ∀ list • ∃ G1 • G1 ∈ Gauge ∧ (∀ G2 • G2 ∈ Gauge ∧ (∀ x• G2 x ⊆ G1 x) ⇒ (∀ t I n m a • m < n ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G2 Fine ∧ a ∈ ClosedInterval (I m) (I (m + 1)) ∧ a ∈ Elems list ⇒ t m = a))
riemann_gauge_thm	⊢ ∀ e • 0. < e ⇒ (∃ G • G ∈ Gauge ∧ (∀ t I n m • m < n ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G Fine ⇒ I (m + 1) - I m < e))
tagged_partition_∃_thm cousin_lemma	⊢ ∀ G a b • G ∈ Gauge ∧ a ≤ b ⇒ (∃ t I n • I 0 = a ∧ I n = b ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G Fine)
riemann_sum_induction_thm	⊢ ∀ f t I n • RiemannSum f (t, I, 0) = 0. ∧ RiemannSum f (t, I, n + 1) = RiemannSum f (t, I, n) + f (t n) * (I (n + 1) - I n)
series_induction_thm1	⊢ ∀ s n • Series s (n + 1) = s 0 + Series (λ m• s (m + 1)) n
ℝ_abs_series_thm	⊢ ∀ s n• Abs (Series s n) ≤ Series (λ m• Abs (s m)) n
riemann_sum_induction_thm1	⊢ ∀ f t I n • RiemannSum f (t, I, 0) = 0. ∧ RiemannSum f (t, I, n + 1) = f (t 0) * (I 1 - I 0) + RiemannSum f ((λ m• t (m + 1)), (λ m• I (m + 1)), n)
riemann_sum_plus_thm	⊢ ∀ f g t I n • RiemannSum (λ x• f x + g x) (t, I, n) = RiemannSum f (t, I, n) + RiemannSum g (t, I, n)
riemann_sum_const_times_thm	⊢ ∀ f c t I n • RiemannSum (λ x• c * f x) (t, I, n) = c * RiemannSum f (t, I, n)
riemann_sum_minus_thm	⊢ ∀ f t I n • RiemannSum (λ x• ~ (f x)) (t, I, n) = ~ (RiemannSum f (t, I, n))
riemann_sum_local_thm	⊢ ∀ f t I s J n • (∀ m• m < n ⇒ t m = s m) ∧ (∀ m• m ≤ n ⇒ I m = J m) ⇒ RiemannSum f (t, I, n) = RiemannSum f (s, J, n)
riemann_sum_o_minus_thm	⊢ ∀ f t I n • RiemannSum f (t, I, n) = RiemannSum (λ x• f (~ x)) ((λ m• ~ (t (n - 1 - m))), (λ m• ~ (I (n - m))), n)
riemann_sum_o_times_thm	⊢ ∀ f t I n c • ¬ c = 0. ⇒ RiemannSum (λ x• f (c * x)) (t, I, n) = c ^-¹ * RiemannSum f ((λ m• c * t m), (λ m• c * I m), n)
partition_reverse_clauses	⊢ ∀ f t I n G • ((t, I, n) ∈ TaggedPartition ⇒ ((λ m• ~ (t (n - 1 - m))), (λ m• ~ (I (n - m))), n) ∈ TaggedPartition) ∧ ((t, I, n) ∈ G Fine ⇒ ((λ m• ~ (t (n - 1 - m))), (λ m• ~ (I (n - m))), n) ∈ (λ x• {t\|~ t ∈ G (~ x)}) Fine)
tagged_partition_append_thm	⊢ ∀ s J m t I n • (s, J, m) ∈ TaggedPartition ∧ (t, I, n) ∈ TaggedPartition ∧ J m = I 0 ⇒ ((λ k• if k < m then s k else t (k - m)), (λ k• if k ≤ m then J k else I (k - m)), m + n) ∈ TaggedPartition
fine_append_thm	⊢ ∀ G s J m t I n • (s, J, m) ∈ G Fine ∧ (t, I, n) ∈ G Fine ∧ J m = I 0 ⇒ ((λ k• if k < m then s k else t (k - m)), (λ k• if k ≤ m then J k else I (k - m)), m + n) ∈ G Fine
riemann_sum_0_thm	⊢ ∀ t I n• RiemannSum (λ x• 0.) (t, I, n) = 0.
riemann_sum_append_thm	⊢ ∀ f t I m n • RiemannSum f (t, I, m + n) = RiemannSum f (t, I, m) + RiemannSum f ((λ k• t (m + k)), (λ k• I (m + k)), n)
riemann_sum_¬_0_thm	⊢ ∀ f t I n • ¬ RiemannSum f (t, I, n) = 0. ⇒ (∃ m • m < n ∧ ¬ f (t m) = 0. ∧ RiemannSum f (t, I, n) = RiemannSum f (t, I, m + 1))
partition_mono_thm	⊢ ∀ t I n k m • (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n ⇒ I k < I (m + 1)
tag_mono_thm	⊢ ∀ t I n k m • (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n ⇒ t k ≤ t m
tag_upper_bound_thm	⊢ ∀ t I n k m • (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n ⇒ t k ≤ I (m + 1)
tag_lower_bound_thm	⊢ ∀ t I n k m • (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n ⇒ I k ≤ t m
subpartition_thm	⊢ ∀ n m t I • m ≤ n ∧ (t, I, n) ∈ TaggedPartition ⇒ (t, I, m) ∈ TaggedPartition
subpartition_fine_thm	⊢ ∀ n m t I n G • m ≤ n ∧ (t, I, n) ∈ G Fine ⇒ (t, I, m) ∈ G Fine
riemann_sum_local_thm1	⊢ ∀ f g t I n • (∀ x• I 0 ≤ x ∧ x ≤ I n ⇒ f x = g x) ∧ (t, I, n) ∈ TaggedPartition ⇒ RiemannSum f (t, I, n) = RiemannSum g (t, I, n)
riemann_sum_0_≤_thm	⊢ ∀ f t I n • (∀ x• 0. ≤ f x) ∧ (t, I, n) ∈ TaggedPartition ⇒ 0. ≤ RiemannSum f (t, I, n)
tag_unique_thm	⊢ ∀ t I n k m • (t, I, n) ∈ TaggedPartition ∧ k < m ∧ m < n ∧ t k = t m ⇒ m = k + 1
partition_cover_thm	⊢ ∀ t I n x • (t, I, n) ∈ TaggedPartition ∧ I 0 < x ∧ x ≤ I n ⇒ (∃ m• m < n ∧ I m < x ∧ x ≤ I (m + 1))
partition_cover_thm1	⊢ ∀ t I n x • (t, I, n) ∈ TaggedPartition ∧ I 0 ≤ x ∧ x < I n ⇒ (∃ m• m < n ∧ I m ≤ x ∧ x < I (m + 1))
riemann_sum_χ_singleton_thm	⊢ ∀ c t I n • (t, I, n) ∈ TaggedPartition ⇒ RiemannSum (χ {c}) (t, I, n) = 0. ∨ (∃ m • m < n ∧ RiemannSum (χ {c}) (t, I, n) = I (m + 1) - I m) ∨ (∃ m • m + 1 < n ∧ RiemannSum (χ {c}) (t, I, n) = I (m + 2) - I m)
int_ℝ_plus_thm	⊢ ∀ f g c d • f Int_R c ∧ g Int_R d ⇒ (λ x• f x + g x) Int_R c + d
int_ℝ_minus_thm	⊢ ∀ f c• f Int_R c ⇒ (λ x• ~ (f x)) Int_R ~ c
int_ℝ_0_thm	⊢ (λ x• 0.) Int_R 0.
int_ℝ_const_times_thm	⊢ ∀ f c d• f Int_R d ⇒ (λ x• c * f x) Int_R c * d
int_ℝ_diff_0_thm	⊢ ∀ f g c • (λ x• f x - g x) Int_R 0. ⇒ (f Int_R c ⇔ g Int_R c)
int_ℝ_unique_thm	⊢ ∀ f c d• f Int_R c ∧ f Int_R d ⇒ c = d
int_ℝ_0_≤_thm	⊢ ∀ f c• (∀ x• 0. ≤ f x) ∧ f Int_R c ⇒ 0. ≤ c
int_ℝ_≤_thm	⊢ ∀ f g c d • (∀ x• f x ≤ g x) ∧ f Int_R c ∧ g Int_R d ⇒ c ≤ d
int_ℝ_0_dominated_thm	⊢ ∀ f g • (∀ x• 0. ≤ f x) ∧ (∀ x• f x ≤ g x) ∧ g Int_R 0. ⇒ f Int_R 0.
int_ℝ_χ_singleton_lemma	⊢ ∀ G e c t I n • 0. < e ∧ G ∈ Gauge ∧ (∀ t I n m • m < n ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G Fine ⇒ I (m + 1) - I m < e) ∧ (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum (χ {c}) (t, I, n)) < 2. * e
int_ℝ_χ_singleton_thm	⊢ ∀ c• χ {c} Int_R 0.
int_ℝ_singleton_support_thm	⊢ ∀ f c• (∀ x• ¬ f x = 0. ⇒ x = c) ⇒ f Int_R 0.
int_ℝ_finite_support_thm	⊢ ∀ f list • (∀ x• ¬ f x = 0. ⇒ x ∈ Elems list) ⇒ f Int_R 0.
int_ℝ_χ_0_⊆_thm	⊢ ∀ A B• A ⊆ B ∧ χ B Int_R 0. ⇒ χ A Int_R 0.
int_ℝ_χ_0_∩_thm	⊢ ∀ A B• χ A Int_R 0. ⇒ χ (A ∩ B) Int_R 0.
χ_∪_∩_thm	⊢ ∀ A B x• χ (A ∪ B) x = χ A x + χ B x - χ (A ∩ B) x
int_ℝ_χ_0_∪_thm	⊢ ∀ A B • χ A Int_R 0. ∧ χ B Int_R 0. ⇒ χ (A ∪ B) Int_R 0.
int_half_infinite_interval_thm	⊢ ∀ f c a• (f Int c) {x\|a ≤ x} ⇔ (f Int c) {x\|a < x}
chosen_value_thm	⊢ ∀ y f c A • (f Int c) A ⇔ ((λ x• if x = y then 0. else f x) Int c) A
int_interval_thm	⊢ ∀ f g a b c • (f Int c) (ClosedInterval a b) ⇔ (f Int c) (OpenInterval a b)
int_ℝ_o_minus_thm	⊢ ∀ f c• f Int_R c ⇔ (λ x• f (~ x)) Int_R c
int_ℝ_o_plus_thm	⊢ ∀ f c h• f Int_R c ⇔ (λ x• f (x + h)) Int_R c
int_ℝ_o_times_thm	⊢ ∀ f c d • ¬ 0. = d ∧ f Int_R c ⇒ (λ x• f (d * x)) Int_R Abs d ^-¹ * c
int_ℝ_support_bounded_below_thm	⊢ ∀ a c f • (∀ x• x ≤ a ⇒ f x = 0.) ⇒ (f Int_R c ⇔ (∀ e • 0. < e ⇒ (∃ G b • G ∈ Gauge ∧ a < b ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ b < I n ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e))))
int_support_bounded_below_lemma	⊢ ∀ a f g c • (∀ x• a < x ⇒ f x = g x) ⇒ ((∀ e • 0. < e ⇒ (∃ G b • G ∈ Gauge ∧ a < b ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ b < I n ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e))) ⇔ (∀ e • 0. < e ⇒ (∃ G b • G ∈ Gauge ∧ a < b ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ b < I n ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum g (t, I, n) - c) < e))))
int_bounded_below_thm	⊢ ∀ a b c f • (f Int c) {x\|a ≤ x} ⇔ (∀ e • 0. < e ⇒ (∃ G b • G ∈ Gauge ∧ a < b ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ b < I n ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e)))
int_ℝ_bounded_support_thm	⊢ ∀ a b c f • a < b ∧ (∀ x• x ≤ a ⇒ f x = 0.) ∧ (∀ x• b ≤ x ⇒ f x = 0.) ⇒ (f Int_R c ⇔ (∀ e • 0. < e ⇒ (∃ G • G ∈ Gauge ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ I n = b ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e))))
bounded_int_thm	⊢ ∀ a b c f • a < b ⇒ ((f Int c) (ClosedInterval a b) ⇔ (∀ e • 0. < e ⇒ (∃ G • G ∈ Gauge ∧ (∀ t I n • (t, I, n) ∈ TaggedPartition ∧ I 0 = a ∧ I n = b ∧ (t, I, n) ∈ G Fine ⇒ Abs (RiemannSum f (t, I, n) - c) < e))))
bounded_int_local_thm	⊢ ∀ a b f g c • a < b ∧ (∀ x• x ∈ ClosedInterval a b ⇒ f x = g x) ⇒ ((g Int c) (ClosedInterval a b) ⇔ (f Int c) (ClosedInterval a b))
straddle_thm	⊢ ∀ f df x e • (f Deriv df x) x ∧ 0. < e ⇒ (∃ d • 0. < d ∧ (∀ u v • u ∈ OpenInterval (x - d) (x + d) ∧ v ∈ OpenInterval (x - d) (x + d) ∧ u ≤ x ∧ x ≤ v ⇒ Abs (df x * (v - u) - (f v - f u)) ≤ e * (v - u)))
straddle_gauge_thm	⊢ ∀ A e f df • (∀ x• x ∈ A ⇒ (f Deriv df x) x) ∧ 0. < e ⇒ (∃ G • G ∈ Gauge ∧ (∀ t I n m • (t, I, n) ∈ TaggedPartition ∧ (t, I, n) ∈ G Fine ∧ m < n ∧ t m ∈ A ⇒ Abs (df (t m) * (I (m + 1) - I m) - (f (I (m + 1)) - f (I m))) ≤ e * (I (m + 1) - I m)))
int_deriv_thm2	⊢ ∀ a b sf f • a < b ∧ (∀ x• a ≤ x ∧ x < b ⇒ (sf Deriv f x) x) ∧ sf Cts b ⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm3	⊢ ∀ a b sf f • a < b ∧ (∀ x• a < x ∧ x ≤ b ⇒ (sf Deriv f x) x) ∧ sf Cts a ⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm	⊢ ∀ a b sf f • a < b ∧ (∀ x• a < x ∧ x < b ⇒ (sf Deriv f x) x) ∧ sf Cts a ∧ sf Cts b ⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm1	⊢ ∀ a b sf f • a < b ∧ (∀ x • x ∈ ClosedInterval a b ⇒ (sf Deriv f x) x) ⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_ℝ_χ_interval_thm	⊢ ∀ a b• a ≤ b ⇒ χ (ClosedInterval a b) Int_R b - a
int_example_thm	⊢ ((λ x• Sqrt (1. - x ^ 2) ^-¹) Int π) (ClosedInterval (~ 1.) 1.)
int_recip_thm	⊢ ∀ a b • 0. < a ∧ a < b ⇒ ((λ x• x ^-¹) Int Log b - Log a) (ClosedInterval a b)
log_minus_log_estimate_thm	⊢ ∀ a b • 0. < a ∧ a < b ⇒ Log b - Log a ≤ (b - a) * a ^-¹
harmonic_series_estimate_thm	⊢ ∀ m • Log (ℕℝ (m + 1)) ≤ Series (λ m• ℕℝ (m + 1) ^-¹) m
harmonic_series_divergent_thm	⊢ ∀ c• ¬ Series (λ m• ℕℝ (m + 1) ^-¹) -> c
area_unique_thm	⊢ ∀ A c d• A Area c ∧ A Area d ⇒ c = d
area_translate_thm	⊢ ∀ A c u v • A Area c ⇒ {(x, y)\|(x + u, y + v) ∈ A} Area c
area_dilate_thm	⊢ ∀ A c d e • A Area c ∧ ¬ d = 0. ∧ ¬ e = 0. ⇒ {(x, y)\|(d ^-¹ * x, e ^-¹ * y) ∈ A} Area Abs d * Abs e * c
area_dilate_thm1	⊢ ∀ A c d • A Area c ∧ ¬ d = 0. ⇒ {(x, y)\|(d ^-¹ * x, d ^-¹ * y) ∈ A} Area d ^ 2 * c
area_empty_thm	⊢ {} Area 0.
area_∪_thm	⊢ ∀ A B c d y • A Area c ∧ B Area d ∧ A ∩ B Area y ⇒ A ∪ B Area c + d - y
area_∩_thm	⊢ ∀ A B c d y • A Area c ∧ B Area d ∧ A ∪ B Area y ⇒ A ∩ B Area c + d - y
area_rectangle_thm	⊢ ∀ w h • 0. ≤ h ∧ 0. ≤ w ⇒ {(x, y) \|x ∈ ClosedInterval 0. w ∧ y ∈ ClosedInterval 0. h} Area w * h
area_circle_lemma1	⊢ ∀ x • Abs x < 1. ⇒ ((λ x• x * Sqrt (1. - x ^ 2) + ArcSin x) Deriv 2. * Sqrt (1. - x ^ 2)) x
area_circle_lemma2	⊢ ∀ x• Abs x ≤ 1. ⇒ 0. ≤ 1. - x ^ 2
area_circle_lemma3	⊢ ∀ x • Abs x ≤ 1. ⇒ (λ x• x * Sqrt (1. - x ^ 2) + ArcSin x) Cts x
area_circle_lemma4	⊢ ∀ r x y • Abs x ≤ r ⇒ (Sqrt (x ^ 2 + y ^ 2) ≤ r ⇔ Abs y ≤ Sqrt (r ^ 2 - x ^ 2))
area_circle_int_thm	⊢ ((λ x• 2. * Sqrt (1. - x ^ 2)) Int π) (ClosedInterval (~ 1.) 1.)
area_unit_circle_thm	⊢ {(x, y)\|Sqrt (x ^ 2 + y ^ 2) ≤ 1.} Area π
circle_dilate_thm	⊢ ∀ r • 0. < r ⇒ {(x, y)\|Sqrt (x ^ 2 + y ^ 2) ≤ r} = {(x, y) \|Sqrt ((r ^-¹ * x) ^ 2 + (r ^-¹ * y) ^ 2) ≤ 1.}
area_circle_thm	⊢ ∀ r • 0. < r ⇒ {(x, y)\|Sqrt (x ^ 2 + y ^ 2) ≤ r} Area π * r ^ 2
buffon_needle_lemma	⊢ let S = {(θ, d) \|θ ∈ ClosedInterval 0. π ∧ d ∈ ClosedInterval 0. 1.} in let x_axis = {(x, y)\|y = 0.} in let needle (θ, d) = {(x, y) \|∃ t • t ∈ ClosedInterval 0. 1. ∧ x = t * Cos θ ∧ y = d - t * Sin θ} in let X = {(θ, d) \|(θ, d) ∈ S ∧ ¬ needle (θ, d) ∩ x_axis = {}} in X Area 2.
buffon_needle_thm	⊢ let S = {(θ, d) \|θ ∈ ClosedInterval 0. π ∧ d ∈ ClosedInterval 0. 1.} in let x_axis = {(x, y)\|y = 0.} in let needle (θ, d) = {(x, y) \|∃ t • t ∈ ClosedInterval 0. 1. ∧ x = t * Cos θ ∧ y = d - t * Sin θ} in let X = {(θ, d) \|(θ, d) ∈ S ∧ ¬ needle (θ, d) ∩ x_axis = {}} in X ⊆ S ∧ (∃ x s • ¬ s = 0. ∧ X Area x ∧ S Area s ∧ x / s = 2. / π)

Created: