xl-gft sqrt_2_irrational_thm Sqrt 2.

xl-gft _countable_thm f : x x pf 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)

xl-gft harmonic_series_divergent_thm c Series (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 Series (m 2/((m+1)*(m+2))) -> 2.

xl-gft binomial_thm x y n (x + y) ^ n = Series (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. (xa x x < b f Cts x) (xa < x x < b (f Deriv df x) x) (xa x x < b g Cts x) (xa < x x < b (g Deriv dg x) x) (xa < 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 -+#>+# (xa < x (f Deriv df x) x) (xa < x (g Deriv dg x) x) (xa < 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. Series ( m x ^ m) (n+1) = (1. - x^(n+1)) / (1. - x)

xl-gft arithmetic_sum_thm c d n Series (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 (xa x x b f Cts x) (xa < x x < b (f Deriv df x) x) (xa x x b g Cts x) (xa < 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 (xa x x b f Cts x) (xa < x x < b (f Deriv df x) x) (xa < 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 (xa 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) (mn m {p | p Prime p n} (p p -1))

xl-gft div_3_rule_thm digits; n: 3 Divides {i | i < n} (idigits i * 10 ^ i) 3 Divides {i | i < n} (idigits 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.