xl-gft sqrt_2_irrational_thm ⊢ ¬Sqrt 2. ∈ ℚ

xl-gft ℂ_sigma_def ⊢ (∀ s• SigmaC s 0 = ℕℂ 0) ∧ (∀s n• SigmaC s(n + 1) = SigmaC s n + s n) ℂ_poly_def ⊢ ∀c n z• PolyC(c, n) z = SigmaC (λ i• c i * z ^ i) (n + 1) fta_thm ⊢ ∀c n• c 0 = ℕℂ 0 ∨ ¬n = 0 ∧ ¬c n = ℕℂ 0 ⇒ (∃ z• PolyC(c, n) z = ℕℂ 0)

xl-gft ℚ_countable_thm ⊢ ∃f : ℕ → ℝ• ∀x• x ∈ ℚ ⇒ ∃p•f p = x

xl-gft pythagoras_thm ⊢ ∀u v : GA• u ⊥ v ⇒ (u - v)^2 = u^2 + v^2

xl-gft area_circle_thm ⊢ ∀r• 0. < r ⇒ {(x, y) | Sqrt(x^2 + y^2) ≤ r} Area π * r ^ 2

xl-gft prime_infinite_thm ⊢ ¬ Prime ∈ Finite

xl-gft 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)

xl-gft de_moivre_thm ⊢ ∀ x m• (Cos x, Sin x) ^ m = (Cos (ℕℝ m * x), Sin (ℕℝ m * x))

xl-gft two_squares_thm ⊢ ∀p m• p ∈ Prime ∧p = 4*m + 1 ⇒∃a b• p = a^2 + b^2

xl-gft ℝ_uncountable_thm ⊢ ∀X: ℕ → ℝ• ∃x• ∀m• ¬x = X m

xl-gft pythagorean_triples_thm ⊢ ∀a b c: ℕ• a^2 + b^2 = c^2 ⇔∃m n d• {a; b} = {d*n*(2*m + n); 2*d*m*(m + n)} ∧c = d*(m^2 + (m + n)^2)

xl-gft schroeder_bernstein_thm ⊢ ∀a b f g• f ∈ a ↣ b ∧ g ∈ b ↣ a ⇒ ∃h• h ∈ a ⤖ b

xl-gft ballot_thm ⊢ ∀m n• letS = BallotCounts m n in letX = {s | s ∈ S ∧ ∀ i• ℕ⿿ 0 < s (i+1)} in S ∈ Finite ∧¬#S = 0 ∧X ⊆ S ∧(n < m ⇒ #X / #S = (m - n) / (m + n))

xl-gft fin_exp_2_ramsey_thm ⊢ ∀a b • ∃n • ∀(V, E) • (V, E) ∈ symg ∧ V ∈ Finite ∧ #V ≥ n ⇒(∃ C • C clique_of (V,E) ∧ #C = a ∨ C indep_of (V,E) ∧ #C = b) infinite_ramsey_thm ⊢ ∀n X C; m : ℕ• X ∈ Infinite ∧ (∀a• C a < m) ⇒(∃Y c•Y ⊆ X ∧ Y ∈ Infinite ∧ c < m ∧∀a• a ⊆ Y ∧ a ∈ Finite ∧ #a = n ⇒ C a = c)

xl-gft harmonic_series_divergent_thm ⊢ ∀c• ¬ Sigma (λm• ℕℝ (m+1) -1) -> c

xl-gft 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!)-1) (n+1) (b-a) + D (n+1) x * (b-a) ^ (n+1) * ℕℝ((n+1)!)-1

xl-gft cauchy_mean_thm ⊢ ∀A f a• A ∈ Finite ∧ ¬A = {} ∧ (∀ x• x ∈ A ⇒ 0. < f x) ⇒Root (#A) (Π A f) ≤ Σ A f / ℕℝ(#A)

xl-gft minkowski_thm ⊢ ∀A a• A ∈ Convex ∧A ∈ Bounded ∧¬A = {} ∧(∀x y• (x, y) ∈ A ⇒ (~x, ~y) ∈ A) ∧A Area a ∧a > 4. ⇒∃i j• (⿿ℝ i, ⿿ℝ j) ∈ A ∧¬(⿿ℝ i, ⿿ℝ j) = (0., 0.)

xl-gft sum_recip_triangulars_thm ⊢ Sigma (λm• 2/((m+1)*(m+2))) -> 2.

xl-gft binomial_thm ⊢ ∀x y n• (x + y) ^ n = Sigma (λm•ℕℝ(Binomial n m) * x ^ m * y ^ (n - m)) (n+1)

xl-gft wilson_thm ⊢ ∀ p• 1 < p ⇒ (p ∈ Prime ⇔ (p - 1)! Mod p = p - 1)

xl-gft ℙ_finite_size_thm ⊢ ∀a• a ∈ Finite ⇒ ℙ a ∈ Finite ∧ #(ℙ a) = 2 ^ #a

xl-gft combinations_finite_size_thm ⊢ ∀A n m• A ∈ Finite ∧ #A = n ⇒{X | X ⊆ A ∧ #X = m} ∈ Finite ∧#{X | X ⊆ A ∧ #X = m} = Binomial n m

xl-gft bezout_thm ⊢ ∀m n• 0 < m ∧ 0 < n ⇒(∃a b• b*n ≤ a*m ∧ Gcd m n = a*m - b*n) ∨(∃a b• a*m ≤ b*n ∧ Gcd m n = b*n - a*m)

xl-gft cantor_thm ⊢ ∀f : 'a → 'a SET• ∃A• ∀x• ¬f x = A

xl-gft 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 -1) +#-> c) a ⇒((λx• f x * g x -1) +#-> c) a

xl-gft 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 -1) -+#> c ⇒(λx• f x * g x -1) -+#> c

xl-gft geometric_sum_thm ⊢ ∀n x• ¬x = 1. ⇒Sigma (λ m• x ^ m) (n+1) = (1. - x^(n+1)) / (1. - x)

xl-gft arithmetic_sum_thm ⊢ ∀c d n• Sigma (λm• c + ℕℝ m * d) n = 1/2 * ℕℝ n * (2. * c + (ℕℝ n - 1.) * d)

xl-gft euclid_algorithm_thm ⊢ ∀m n• 0 < m ∧ 0 < n ⇒Gcd m n = if m < n then Gcd m (n-m) else if m = n then m else Gcd (m-n) n

xl-gft gcd_def ⊢ ∀m n• 0 < m ∧ 0 < n ⇒Gcd m n Divides m ∧ Gcd m n Divides n ∧(∀d• d Divides m ∧ d Divides n ⇒d Divides Gcd m n)

xl-gft lagrange_cosets_thm ⊢ ∀G H• G ∈ Group ∧ Car G ∈ Finite ∧ H ∈ Subgroup G ⇒Car H ∈ Finite ∧ Car(G/H) ∈ Finite ∧ #G = #H * #(G/H)

xl-gft induction_thm ⊢ ∀ p• p 0 ∧ (∀ m• p m ⇒ p (m + 1)) ⇒ (∀ n• p n)

xl-gft 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))

xl-gft 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)

xl-gft schwarz_inequality_thm ⊢ ∀f g A• Supp f ∈ Finite ∧ Supp g ∈ Finite ⇒Abs (f .v g) ≤ Norm f * Norm g

xl-gft 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)

xl-gft unique_factorisation_thm ⊢ ∀m• 0 < m ⇒∃1 e•{k | ¬e k = 0} ∈ Finite ∧ {k | ¬e k = 0} ⊆ Prime ∧m = Π {k | ¬e k = 0} (λp• p ^ e p)

xl-gft recip_primes_div_thm ⊢(∀n•{p | p ∈ Prime ∧ p ≤ n} ∈ Finite) ∧(∀m•∃n• ℕℝ m ≤ Σ {p | p ∈ Prime ∧ p ≤ n} (λp• ℕℝ p -1))

xl-gft div_3_rule_thm ⊢ ∀digits; n:ℕ• 3 Divides Σ {i | i < n} (λi•digits i * 10 ^ i) ⇔ 3 Divides Σ {i | i < n} (λi•digits i)

xl-gft poly_factor_thm ⊢ ∀l1 c• ¬l1 = [] ∧PolyEval l1 c = 0. ⇒∃l2• Length l2 < Length l1 ∧(λx• PolyEval l1 x) = (λx• (x - c)*PolyEval l2 x)

xl-gft poly_remainder_thm ⊢ ∀l1 c• ¬l1 = [] ⇒∃l2• Length l2 < Length l1 ∧(λx• PolyEval l1 x) = (λx• (x - c)*PolyEval l2 x + PolyEval l1 c)

xl-gft triangle_inequality_thm ⊢ ∀f g• Supp f ∈ Finite ∈ Finite ∧ Supp g ∈ Finite ⇒Supp (λx• f x + g x) ∈ Finite ∧Norm (λ x• f x + g x) ≤ Norm f + Norm g

xl-gft birthdays_thm ⊢ letS = {L | Elems L ⊆ {i | 1 ≤ i ∧ i ≤ 365} ∧ # L = 23} in letX = {L | L ∈ S ∧ ¬L ∈ Distinct} in S ∈ Finite ∧¬#S = 0 ∧X ⊆ S ∧#X / #S > 1/2

xl-gft size_inc_exc_thm ⊢ ∀I U A• I ∈ Finite ∧ ¬I = {} ∧(∀i• i ∈ I ⇒ U i ∈ Finite) ∧A = ⋃{B | ∃i• i ∈ I ∧ B = U i} ⇒ℕℝ(# A) = Σ (ℙI \ {{}}) (λJ• ~1. ^ (#J + 1) * ℕℝ(# (⋂{B | ∃j• j ∈ J ∧ B = U j})))

xl-gft buffon_needle_thm ⊢ letS = {(θ, d) | θ ∈ ClosedInterval 0. π ∧ d ∈ ClosedInterval 0. 1.} in letx_axis = {(x, y) | y = 0.} in letneedle(θ, d) = {(x, y) | ∃t• t ∈ ClosedInterval 0. 1. ∧ x = t * Cos θ ∧ y = d - t * Sin θ} in letX = {(θ, d) | (θ, d) ∈ S ∧ ¬needle(θ, d) ∩ x_axis = {}} in X ⊆ S ∧∃x s• ¬s = 0. ∧ X Area x ∧S Area s ∧x / s = 2. / π

xl-gft descartes_rule_thm ⊢ ∀f• f ∈ PolyFunc ∧¬f = (λx• 0.) ⇒∃k• SignChanges (Coeffs f) = Σ {r | 0. < r ∧ r ∈ Roots f} (λr• RootMultiplicity f r) + 2*k

This page was prepared as a ProofPower document by Rob Arthan and translated into HTML in collusion with Roger Jones.