diff --git a/packages/proveit/numbers/__init__.py b/packages/proveit/numbers/__init__.py index 4c25a2184db5..9b8f90916a1e 100644 --- a/packages/proveit/numbers/__init__.py +++ b/packages/proveit/numbers/__init__.py @@ -1,16 +1,17 @@ # Arithmetic and number theory concepts. from .number_sets import ( - ZeroSet, Natural, NaturalPos, - Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos, - IntegerOdd, Rational, RationalNonZero, RationalPos, RationalNeg, + ZeroSet, Natural, NaturalPos, Integer, IntegerEven, + IntegerNonZero, IntegerNeg, IntegerNonPos, IntegerOdd, + Prime, Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, Real, RealNonZero, RealNeg, RealPos, RealNonNeg, RealNonPos, Complex, ComplexNonZero, Conjugate, complex_polar_coordinates, unit_length_complex_polar_angle) -from .number_sets import Interval, RealInterval, IntervalOO, IntervalCC, IntervalCO, IntervalOC +from .number_sets import ( + Interval, RealInterval, IntervalOO, IntervalCC, IntervalCO, IntervalOC) from .number_sets import e, pi, i, infinity from .number_operation import (NumberOperation, readily_factorable, deduce_in_number_set, @@ -36,7 +37,8 @@ less_eq_numeric_rationals, not_equal_numeric_rationals, deduce_not_equal_numeric_rationals) -from .numerals import zero, one, two, three, four, five, six, seven, eight, nine, hexa, hexb, hexc, hexd, hexe, hexf +from .numerals import (zero, one, two, three, four, five, six, seven, + eight, nine, hexa, hexb, hexc, hexd, hexe, hexf) from .addition import (Add, subtract, dist_subtract, dist_add) from .negation import Neg, negated from .ordering import (NumberOrderingRelation, number_ordering, diff --git a/packages/proveit/numbers/number_sets/__init__.py b/packages/proveit/numbers/number_sets/__init__.py index ab18fc7b3c39..23ebd7a35fd0 100644 --- a/packages/proveit/numbers/number_sets/__init__.py +++ b/packages/proveit/numbers/number_sets/__init__.py @@ -1,6 +1,6 @@ from .integers import ( Integer, IntegerEven, IntegerNeg, IntegerNonZero, - IntegerNonPos, IntegerOdd, Interval, infinity) + IntegerNonPos, IntegerOdd, Interval, infinity, Prime) from .natural_numbers import ZeroSet, Natural, NaturalPos from .rational_numbers import (Rational, RationalNonZero, RationalPos, RationalNeg, diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/common.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/common.ipynb index 4c5ad859eb51..cecf26d8db23 100644 --- a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/common.ipynb +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/common.ipynb @@ -18,8 +18,11 @@ "# Prepare this notebook for defining the common expressions of a theory:\n", "%common_expressions_notebook # Keep this at the top following 'import proveit'.\n", "from proveit import Literal\n", + "from proveit.logic.sets import Set\n", + "from proveit.numbers import two, three, five, seven, num\n", "from proveit.numbers.number_sets.integers.integer import (\n", - " IntegerSet, IntegerEvenSet, IntegerNegSet, IntegerNonZeroSet, IntegerNonPosSet, IntegerOddSet)\n", + " IntegerSet, IntegerEvenSet, IntegerNegSet, IntegerNonZeroSet, IntegerNonPosSet,\n", + " IntegerOddSet, PrimeSet)\n", "%begin common" ] }, @@ -77,6 +80,15 @@ "IntegerOdd = IntegerOddSet()" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Prime = PrimeSet()" + ] + }, { "cell_type": "code", "execution_count": null, @@ -86,6 +98,32 @@ "infinity = Literal('infinity',r'\\infty')" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "first_10_primes = (\n", + " Set(two, three, five, seven, num(11),\n", + " num(13), num(17), num(19), num(23), num(29))\n", + ")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "primes_less_than_100 = (\n", + " Set(two, three, five, seven, num(11), num(13), num(17),\n", + " num(19), num(23), num(29), num(31), num(37), num(41),\n", + " num(43), num(47), num(53), num(59), num(61), num(67),\n", + " num(71), num(73), num(79), num(83), num(89), num(97))\n", + ")" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/demonstrations.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/demonstrations.ipynb index 8955e4f9810a..9a133c0a7057 100644 --- a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/demonstrations.ipynb @@ -19,9 +19,10 @@ "from proveit.logic import Boolean, Equals, Exists, NotEquals, InSet, NotInSet, Or\n", "from proveit.numbers import (Add, Neg, Less, LessEq, greater, greater_eq,\n", " number_ordering, Mult, num, subtract)\n", - "from proveit.numbers import (zero, one, two, three, four, five, six, seven,\n", - " eight, nine, Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos,\n", - " IntegerOdd, Interval, Natural, NaturalPos, Rational, Real)\n", + "from proveit.numbers import (\n", + " zero, one, two, three, four, five, six, seven, eight, nine,\n", + " Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos,\n", + " IntegerOdd, Interval, Natural, NaturalPos, Prime, Rational, Real)\n", "%begin demonstrations" ] }, @@ -1485,6 +1486,120 @@ "InSet(num(13), IntegerOdd).prove()" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Prime Numbers (`Prime`), Prime Membership (`PrimeMembership`)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Prime)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(InSet(y, Prime), Boolean).prove()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Integer).prove(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# A side-effect of y being prime: y is 2 or y is odd\n", + "Or(Equals(y, two), InSet(y, IntegerOdd)).prove(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Rational).prove(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Prime).derive_element_in_rational(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Real).prove(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(y, Prime).derive_element_in_real(assumptions=[InSet(y, Prime)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from proveit.numbers.number_sets.integers import first_10_primes\n", + "first_10_primes" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from proveit.logic.sets import Set\n", + "small_primes = [two, three, five, seven, num(11)]\n", + "for p in small_primes:\n", + " display(InSet(p, Prime).conclude())" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "try:\n", + " InSet(num(53), Prime).conclude()\n", + "except Exception as the_exception:\n", + " print(f\"EXCEPTION: {the_exception}\")" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_is_two_or_odd/thm_proof.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_is_two_or_odd/thm_proof.ipynb new file mode 100644 index 000000000000..b87367324c54 --- /dev/null +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_is_two_or_odd/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.integers.prime_is_two_or_odd theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving prime_is_two_or_odd" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_membership_is_bool/thm_proof.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_membership_is_bool/thm_proof.ipynb new file mode 100644 index 000000000000..a14b46471ba3 --- /dev/null +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_membership_is_bool/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.integers.prime_membership_is_bool theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving prime_membership_is_bool" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_within_int/thm_proof.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_within_int/thm_proof.ipynb new file mode 100644 index 000000000000..f3c42e7796b8 --- /dev/null +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_within_int/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.integers.prime_within_int theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving prime_within_int" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/small_primes_are_prime/thm_proof.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/small_primes_are_prime/thm_proof.ipynb new file mode 100644 index 000000000000..4a0b354e4877 --- /dev/null +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/small_primes_are_prime/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.integers.small_primes_are_prime theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving small_primes_are_prime" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/theorems.ipynb b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/theorems.ipynb index 7c339c40e6f4..d6b6969b6577 100644 --- a/packages/proveit/numbers/number_sets/integers/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/numbers/number_sets/integers/_theory_nbs_/theorems.ipynb @@ -18,18 +18,19 @@ "# Prepare this notebook for defining the theorems of a theory:\n", "%theorems_notebook # Keep this at the top following 'import proveit'.\n", "from proveit import Operation, IndexedVar\n", - "from proveit import a, b, c, d, e, f, g, h, i, m, n, x, y, z, S, P\n", + "from proveit import a, b, c, d, e, f, g, h, i, m, n, p, x, y, z, S, P\n", "from proveit.core_expr_types import (y_1_to_n)\n", "from proveit.logic import (And, Equals, Exists, Forall, Implies, in_bool, InSet, NotInSet, Set,\n", " NotEquals, Or, ProperSubset, SubsetEq, SetEquiv, EmptySet)\n", "from proveit.logic.sets import Card, Disjoint, x_equals_any_y\n", "from proveit.numbers import (zero, one, two, three, four, five, six, seven, eight, nine,\n", " num, frac, Neg)\n", - "from proveit.numbers import (ZeroSet, Natural, NaturalPos, \n", - " Integer, IntegerEven, IntegerNeg, IntegerNonZero, IntegerNonPos,\n", - " IntegerOdd, Interval, Complex)\n", + "from proveit.numbers import (Complex, Integer, IntegerEven, IntegerNeg, IntegerNonPos,\n", + " IntegerNonZero, IntegerOdd, Interval, Natural, NaturalPos,\n", + " Prime, ZeroSet)\n", "from proveit.numbers import Add, subtract, greater, greater_eq, Less, LessEq, Mult, number_ordering\n", - "from proveit.numbers import Pzero, Pone, Pm, P_mAddOne, Pn" + "from proveit.numbers import Pzero, Pone, Pm, P_mAddOne, Pn\n", + "from proveit.numbers.number_sets.integers import first_10_primes" ] }, { @@ -167,6 +168,19 @@ "nine_is_odd = InSet(nine, IntegerOdd)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# This theorem format works fine as along as the underlying set\n", + "# has <= 13 elements (not sure why)\n", + "small_primes_are_prime = Forall(\n", + " p, InSet(p, Prime),\n", + " domain = first_10_primes)" + ] + }, { "cell_type": "code", "execution_count": null, @@ -489,6 +503,15 @@ "odd_int_within_int = ProperSubset(IntegerOdd, Integer)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "prime_within_int = ProperSubset(Prime, Integer)" + ] + }, { "cell_type": "code", "execution_count": null, @@ -670,6 +693,16 @@ "domain = IntegerEven)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# a prime number is either 2 or odd\n", + "prime_is_two_or_odd = Forall(p, Or(Equals(p, two), InSet(p, IntegerOdd)), domain = Prime)" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -732,6 +765,15 @@ "odd_int_membership_is_bool = Forall(x, in_bool(InSet(x, IntegerOdd)))" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "prime_membership_is_bool = Forall(x, in_bool(InSet(x, Prime)))" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/numbers/number_sets/integers/integer.py b/packages/proveit/numbers/number_sets/integers/integer.py index cd18ecd261da..949da8c019fd 100644 --- a/packages/proveit/numbers/number_sets/integers/integer.py +++ b/packages/proveit/numbers/number_sets/integers/integer.py @@ -304,10 +304,21 @@ def membership_object(self, element): return IntegerOddMembership(element) +class PrimeSet(NumberSet): + def __init__(self, *, styles=None): + NumberSet.__init__(self, 'PRIMES', r'\mathbb{P}', + theory=__file__, styles=styles) + + def membership_object(self, element): + from .integer_membership import PrimeMembership + return PrimeMembership(element) + + if proveit.defaults.running_theory_notebook is None: # Import some fundamental theorems without quantifiers when not # running an common/axioms/theorems theory notebook. from . import (zero_set_within_int, zero_set_within_nonpos_int, + prime_within_int, nat_within_int, nat_pos_within_int, nat_pos_within_nonzero_int, diff --git a/packages/proveit/numbers/number_sets/integers/integer_membership.py b/packages/proveit/numbers/number_sets/integers/integer_membership.py index 50447269c7ef..126bb49ff37e 100644 --- a/packages/proveit/numbers/number_sets/integers/integer_membership.py +++ b/packages/proveit/numbers/number_sets/integers/integer_membership.py @@ -4,7 +4,7 @@ from proveit.numbers import Add, Less, LessEq, Mult, Neg, subtract from proveit.numbers import ( zero, one, two, Integer, IntegerEven, IntegerNeg, - IntegerNonPos, IntegerNonZero, IntegerOdd) + IntegerNonPos, IntegerNonZero, IntegerOdd, Prime) from proveit.numbers.number_sets.number_set import NumberMembership @@ -503,3 +503,84 @@ def derive_element_as_double_int_plus_one(self, **defaults_config): from . import odd_int_is_double_int_plus_one _a_sub = self.element return odd_int_is_double_int_plus_one.instantiate({a:_a_sub}) + + +class PrimeMembership(NumberMembership): + ''' + Defines methods that apply to membership in the set of prime + numbers {2, 3, 5, 7, 11, ...}. + ''' + + def __init__(self, element): + NumberMembership.__init__(self, element, Prime) + + def _readily_provable(self): + return NumberMembership._readily_provable(self) + + @prover + def conclude(self, **defaults_config): + ''' + Concluding that an arbitrary number is prime is challenging. + For self.element that is an actual number, one could possibly + perform trial division of the given element by the numbers + 2, 3, 4, ..., k, where k ≤ sqrt(element) (which we definitely + do NOT try to do here right now). For small + numbers, we resort to a list of the first 10 prime numbers. + ''' + from proveit.numbers import DecimalSequence, Numeral + if (isinstance(self.element, Numeral) + or isinstance(self.element, DecimalSequence)): + if self.element.as_int() < 30: + from proveit import p + from . import small_primes_are_prime + return small_primes_are_prime.instantiate( + {p:self.element}) + + raise NotImplementedError( + "PrimeMembership.conclude() still under development " + "and currently only works for literal prime numbers " + "less than 30.") + + return NumberMembership.conclude(self) + + def side_effects(self, judgment): + ''' + Yield side-effects when proving 'n in Prime' for: + (1) A prime number p is an integer (this will cascade to + rationals, reals, and complex numbers); + (2) A prime is either 2 or an odd integer. + ''' + yield self.derive_element_in_integer + yield self.derive_element_as_two_or_odd + + @relation_prover + def deduce_in_bool(self, **defaults_config): + from . import prime_membership_is_bool + return prime_membership_is_bool.instantiate( + {x: self.element}, auto_simplify=False) + + @prover + def derive_element_in_integer(self, **defaults_config): + from . import prime_within_int + return prime_within_int.derive_superset_membership( + self.element, auto_simplify=False) + + @prover + def derive_element_in_rational(self, **defaults_config): + from proveit.numbers.number_sets.rational_numbers import ( + prime_within_rational) + return prime_within_rational.derive_superset_membership( + self.element, auto_simplify=False) + + @prover + def derive_element_in_real(self, **defaults_config): + from proveit.numbers.number_sets.real_numbers import ( + prime_within_real) + return prime_within_real.derive_superset_membership( + self.element, auto_simplify=False) + + @prover + def derive_element_as_two_or_odd(self, **defaults_config): + from proveit import p + from . import prime_is_two_or_odd + return prime_is_two_or_odd.instantiate({p: self.element}) diff --git a/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/proofs/prime_within_rational/thm_proof.ipynb b/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/proofs/prime_within_rational/thm_proof.ipynb new file mode 100644 index 000000000000..df6f5fa11da1 --- /dev/null +++ b/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/proofs/prime_within_rational/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.rational_numbers.prime_within_rational theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving prime_within_rational" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/theorems.ipynb b/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/theorems.ipynb index 9eb2bcff3e62..7eca0d45a4a6 100644 --- a/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/numbers/number_sets/rational_numbers/_theory_nbs_/theorems.ipynb @@ -22,7 +22,7 @@ "from proveit.numbers import frac, GCD, Less, LessEq, greater, greater_eq\n", "from proveit.numbers import one, zero\n", "from proveit.numbers import (ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,\n", - " IntegerEven, IntegerOdd, Rational, RationalPos, RationalNeg,\n", + " IntegerEven, IntegerOdd, Prime, Rational, RationalPos, RationalNeg,\n", " RationalNonNeg, RationalNonPos, RationalNonZero, NaturalPos)" ] }, @@ -179,6 +179,15 @@ "odd_int_within_rational = ProperSubset(IntegerOdd, Rational)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "prime_within_rational = ProperSubset(Prime, Rational)" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/proofs/prime_within_real/thm_proof.ipynb b/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/proofs/prime_within_real/thm_proof.ipynb new file mode 100644 index 000000000000..fe97ac88e096 --- /dev/null +++ b/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/proofs/prime_within_real/thm_proof.ipynb @@ -0,0 +1,48 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.numbers.number_sets.real_numbers.prime_within_real theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit import defaults, display_provers # useful imports" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving prime_within_real" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/theorems.ipynb b/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/theorems.ipynb index 87f90a4ffcfc..77013b768665 100644 --- a/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/numbers/number_sets/real_numbers/_theory_nbs_/theorems.ipynb @@ -24,10 +24,11 @@ " IntervalCC, IntervalCO, IntervalOC, IntervalOO,\n", " Less, LessEq, Mult, Neg, number_ordering, sqrt)\n", "from proveit.numbers import (\n", - " zero, one, two, e, pi, ZeroSet, Complex, \n", - " Integer, Natural, NaturalPos, IntegerEven, IntegerNeg, IntegerNonPos, IntegerNonZero,\n", - " IntegerOdd, Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, \n", - " Real, RealNonNeg, RealPos, RealNeg, RealNonPos, RealNonZero)\n" + " zero, one, two, e, pi, ZeroSet, Complex, \n", + " Integer, Natural, NaturalPos, IntegerEven, IntegerNeg, IntegerNonPos,\n", + " IntegerNonZero, IntegerOdd, Prime, Rational, RationalNonZero, RationalPos,\n", + " RationalNeg, RationalNonNeg, RationalNonPos, Real, RealNonNeg, RealPos,\n", + " RealNeg, RealNonPos, RealNonZero)\n" ] }, { @@ -192,6 +193,15 @@ "odd_int_within_real = ProperSubset(IntegerOdd, Real)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "prime_within_real = ProperSubset(Prime, Real)" + ] + }, { "cell_type": "code", "execution_count": null,