Home | Intuitionistic Logic Explorer Theorem List (p. 130 of 133) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||
Theorem | sinhalfpip 12901 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴)) | ||||||||||||||||||||||||||
Theorem | sinhalfpim 12902 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴)) | ||||||||||||||||||||||||||
Theorem | coshalfpip 12903 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴)) | ||||||||||||||||||||||||||
Theorem | coshalfpim 12904 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴)) | ||||||||||||||||||||||||||
Theorem | ptolemy 12905 | Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 11451, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.) | ||||||||||||||||||||||||
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = π) → (((sin‘𝐴) · (sin‘𝐵)) + ((sin‘𝐶) · (sin‘𝐷))) = ((sin‘(𝐵 + 𝐶)) · (sin‘(𝐴 + 𝐶)))) | ||||||||||||||||||||||||||
Theorem | sincosq1lem 12906 | Lemma for sincosq1sgn 12907. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴)) | ||||||||||||||||||||||||||
Theorem | sincosq1sgn 12907 | The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴))) | ||||||||||||||||||||||||||
Theorem | sincosq2sgn 12908 | The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ((π / 2)(,)π) → (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0)) | ||||||||||||||||||||||||||
Theorem | sincosq3sgn 12909 | The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (π(,)(3 · (π / 2))) → ((sin‘𝐴) < 0 ∧ (cos‘𝐴) < 0)) | ||||||||||||||||||||||||||
Theorem | sincosq4sgn 12910 | The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ((3 · (π / 2))(,)(2 · π)) → ((sin‘𝐴) < 0 ∧ 0 < (cos‘𝐴))) | ||||||||||||||||||||||||||
Theorem | sinq12gt0 12911 | The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴)) | ||||||||||||||||||||||||||
Theorem | sinq34lt0t 12912 | The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0) | ||||||||||||||||||||||||||
Theorem | cosq14gt0 12913 | The cosine of a number strictly between -π / 2 and π / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘𝐴)) | ||||||||||||||||||||||||||
Theorem | cosq23lt0 12914 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ ((π / 2)(,)(3 · (π / 2))) → (cos‘𝐴) < 0) | ||||||||||||||||||||||||||
Theorem | coseq0q4123 12915 | Location of the zeroes of cosine in (-(π / 2)(,)(3 · (π / 2))). (Contributed by Jim Kingdon, 14-Mar-2024.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (-(π / 2)(,)(3 · (π / 2))) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||||||||||||||||||||||||||
Theorem | coseq00topi 12916 | Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||||||||||||||||||||||||||
Theorem | coseq0negpitopi 12917 | Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)})) | ||||||||||||||||||||||||||
Theorem | tanrpcl 12918 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+) | ||||||||||||||||||||||||||
Theorem | tangtx 12919 | The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (tan‘𝐴)) | ||||||||||||||||||||||||||
Theorem | sincosq1eq 12920 | Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.) | ||||||||||||||||||||||||
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐴 + 𝐵) = 1) → (sin‘(𝐴 · (π / 2))) = (cos‘(𝐵 · (π / 2)))) | ||||||||||||||||||||||||||
Theorem | sincos4thpi 12921 | The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.) | ||||||||||||||||||||||||
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2))) | ||||||||||||||||||||||||||
Theorem | tan4thpi 12922 | The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) | ||||||||||||||||||||||||
⊢ (tan‘(π / 4)) = 1 | ||||||||||||||||||||||||||
Theorem | sincos6thpi 12923 | The sine and cosine of π / 6. (Contributed by Paul Chapman, 25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.) | ||||||||||||||||||||||||
⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2)) | ||||||||||||||||||||||||||
Theorem | sincos3rdpi 12924 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) | ||||||||||||||||||||||||
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||||||||||||||||||||||||||
Theorem | pigt3 12925 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) | ||||||||||||||||||||||||
⊢ 3 < π | ||||||||||||||||||||||||||
Theorem | pige3 12926 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) | ||||||||||||||||||||||||
⊢ 3 ≤ π | ||||||||||||||||||||||||||
Theorem | abssinper 12927 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) | ||||||||||||||||||||||||
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||||||||||||||||||||||||||
Theorem | sinkpi 12928 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) | ||||||||||||||||||||||||
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||||||||||||||||||||||||||
Theorem | coskpi 12929 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) | ||||||||||||||||||||||||
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||||||||||||||||||||||||||
Theorem | cosordlem 12930 | Cosine is decreasing over the closed interval from 0 to π. (Contributed by Mario Carneiro, 10-May-2014.) | ||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) | ||||||||||||||||||||||||||
Theorem | cosq34lt1 12931 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||||||||||||||||||||||||||
Theorem | cos02pilt1 12932 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 19-Mar-2024.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||||||||||||||||||||||||||
This section describes the conventions we use. These conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first-order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:
| ||||||||||||||||||||||||||
Theorem | conventions 12933 |
Unless there is a reason to diverge, we follow the conventions of the
Metamath Proof Explorer (MPE, set.mm). This list of conventions is
intended to be read in conjunction with the corresponding conventions in
the Metamath Proof Explorer, and only the differences are described
below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. For the "g" abbreviation, this is related to the set.mm usage, in which "is a set" conditions are converted from hypotheses to antecedents, but is also used where "is a set" conditions are added relative to similar set.mm theorems.
(Contributed by Jim Kingdon, 24-Feb-2020.) (New usage is discouraged.) | ||||||||||||||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||||||||||||||
Theorem | ex-or 12934 | Example for ax-io 698. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||
⊢ (2 = 3 ∨ 4 = 4) | ||||||||||||||||||||||||||
Theorem | ex-an 12935 | Example for ax-ia1 105. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||
⊢ (2 = 2 ∧ 3 = 3) | ||||||||||||||||||||||||||
Theorem | 1kp2ke3k 12936 |
Example for df-dec 9183, 1000 + 2000 = 3000.
This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with (2 + 1) = 3, commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 9183 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||||||||||||||
⊢ (;;;1000 + ;;;2000) = ;;;3000 | ||||||||||||||||||||||||||
Theorem | ex-fl 12937 | Example for df-fl 10043. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||
⊢ ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2) | ||||||||||||||||||||||||||
Theorem | ex-ceil 12938 | Example for df-ceil 10044. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1) | ||||||||||||||||||||||||||
Theorem | ex-exp 12939 | Example for df-exp 10293. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
⊢ ((5↑2) = ;25 ∧ (-3↑-2) = (1 / 9)) | ||||||||||||||||||||||||||
Theorem | ex-fac 12940 | Example for df-fac 10472. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
⊢ (!‘5) = ;;120 | ||||||||||||||||||||||||||
Theorem | ex-bc 12941 | Example for df-bc 10494. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
⊢ (5C3) = ;10 | ||||||||||||||||||||||||||
Theorem | ex-dvds 12942 | Example for df-dvds 11494: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||
⊢ 3 ∥ 6 | ||||||||||||||||||||||||||
Theorem | ex-gcd 12943 | Example for df-gcd 11636. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||
⊢ (-6 gcd 9) = 3 | ||||||||||||||||||||||||||
Theorem | mathbox 12944 |
(This theorem is a dummy placeholder for these guidelines. The label
of this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of iset.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of iset.mm. Guidelines: Mathboxes in iset.mm follow the same practices as in set.mm, so refer to the mathbox guidelines there for more details. (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (New usage is discouraged.) | ||||||||||||||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||||||||||||||
Theorem | bj-nnsn 12945 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ ¬ 𝜑 → ¬ 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-nnor 12946 | Double negation of a disjunction in terms of implication. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ (¬ ¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → ¬ ¬ 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-nnim 12947 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ ¬ (𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-nnan 12948 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ ¬ (𝜑 ∧ 𝜓) → (¬ ¬ 𝜑 ∧ ¬ ¬ 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-nnal 12949 | The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ ¬ ∀𝑥𝜑 → ∀𝑥 ¬ ¬ 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-nnclavius 12950 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||
⊢ ((¬ 𝜑 → 𝜑) → ¬ ¬ 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-trst 12951 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (𝜑 → STAB 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-fast 12952 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ 𝜑 → STAB 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-nnbist 12953 | If a formula is not refutable, then it is stable if and only if it is provable. By double-negation translation, if 𝜑 is a classical tautology, then ¬ ¬ 𝜑 is an intuitionistic tautology. Therefore, if 𝜑 is a classical tautology, then 𝜑 is intuitionistically equivalent to its stability (and to its decidability, see bj-nnbidc 12962). (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ ¬ 𝜑 → (STAB 𝜑 ↔ 𝜑)) | ||||||||||||||||||||||||||
Theorem | bj-stim 12954 | A conjunction with a stable consequent is stable. See stabnot 818 for negation and bj-stan 12955 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (STAB 𝜓 → STAB (𝜑 → 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-stan 12955 | The conjunction of two stable formulas is stable. See bj-stim 12954 for implication, stabnot 818 for negation, and bj-stal 12957 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ ((STAB 𝜑 ∧ STAB 𝜓) → STAB (𝜑 ∧ 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-stand 12956 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 12955. Its proof is shorter, so one could prove it first and then bj-stan 12955 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ (𝜑 → STAB 𝜓) & ⊢ (𝜑 → STAB 𝜒) ⇒ ⊢ (𝜑 → STAB (𝜓 ∧ 𝜒)) | ||||||||||||||||||||||||||
Theorem | bj-stal 12957 | The universal quantification of stable formula is stable. See bj-stim 12954 for implication, stabnot 818 for negation, and bj-stan 12955 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (∀𝑥STAB 𝜑 → STAB ∀𝑥𝜑) | ||||||||||||||||||||||||||
Theorem | bj-pm2.18st 12958 | Clavius law for stable formulas. See pm2.18dc 840. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||
⊢ (STAB 𝜑 → ((¬ 𝜑 → 𝜑) → 𝜑)) | ||||||||||||||||||||||||||
Theorem | bj-trdc 12959 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (𝜑 → DECID 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-fadc 12960 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ 𝜑 → DECID 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-dcstab 12961 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ (DECID 𝜑 → STAB 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-nnbidc 12962 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 12953. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (¬ ¬ 𝜑 → (DECID 𝜑 ↔ 𝜑)) | ||||||||||||||||||||||||||
Theorem | bj-nndcALT 12963 | Alternate proof of nndc 836. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ ¬ ¬ DECID 𝜑 | ||||||||||||||||||||||||||
Theorem | bj-nnst 12964 | Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ ¬ ¬ STAB 𝜑 | ||||||||||||||||||||||||||
Theorem | bj-dcdc 12965 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ (DECID DECID 𝜑 ↔ DECID 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-stdc 12966 | Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ (STAB DECID 𝜑 ↔ DECID 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-dcst 12967 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
⊢ (DECID STAB 𝜑 ↔ STAB 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-stst 12968 | Stability of a proposition is stable if and only if that proposition is stable. STAB is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
⊢ (STAB STAB 𝜑 ↔ STAB 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-ex 12969* | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1577 and 19.9ht 1620 or 19.23ht 1473). (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ (∃𝑥𝜑 → 𝜑) | ||||||||||||||||||||||||||
Theorem | bj-hbalt 12970 | Closed form of hbal 1453 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||||||||||||||
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||||||||||||||||||||||||||
Theorem | bj-nfalt 12971 | Closed form of nfal 1555 (copied from set.mm). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑) | ||||||||||||||||||||||||||
Theorem | spimd 12972 | Deduction form of spim 1716. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||||||||||||||||||||||||||
Theorem | 2spim 12973* | Double substitution, as in spim 1716. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑧𝜒 & ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑧∀𝑥𝜓 → 𝜒) | ||||||||||||||||||||||||||
Theorem | ch2var 12974* | Implicit substitution of 𝑦 for 𝑥 and 𝑡 for 𝑧 into a theorem. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑧𝜓 & ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||||||||||||||||||||||||||
Theorem | ch2varv 12975* | Version of ch2var 12974 with non-freeness hypotheses replaced with disjoint variable conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||||||||||||||||||||||||||
Theorem | bj-exlimmp 12976 | Lemma for bj-vtoclgf 12983. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜒 → 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-exlimmpi 12977 | Lemma for bj-vtoclgf 12983. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → 𝜑) & ⊢ (𝜒 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||||||||||||||||||||||||||
Theorem | bj-sbimedh 12978 | A strengthening of sbiedh 1760 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → 𝜒)) | ||||||||||||||||||||||||||
Theorem | bj-sbimeh 12979 | A strengthening of sbieh 1763 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓) | ||||||||||||||||||||||||||
Theorem | bj-sbime 12980 | A strengthening of sbie 1764 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓) | ||||||||||||||||||||||||||
Theorem | bj-el2oss1o 12981 | Shorter proof of el2oss1o 13188 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||
⊢ (𝐴 ∈ 2o → 𝐴 ⊆ 1o) | ||||||||||||||||||||||||||
Various utility theorems using FOL and extensionality. | ||||||||||||||||||||||||||
Theorem | bj-vtoclgft 12982 | Weakening two hypotheses of vtoclgf 2744. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝑉 → 𝜓)) | ||||||||||||||||||||||||||
Theorem | bj-vtoclgf 12983 | Weakening two hypotheses of vtoclgf 2744. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → 𝜑) & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||||||||||||||||||||||||||
Theorem | elabgf0 12984 | Lemma for elabgf 2826. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ (𝑥 = 𝐴 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) | ||||||||||||||||||||||||||
Theorem | elabgft1 12985 | One implication of elabgf 2826, in closed form. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝜓)) | ||||||||||||||||||||||||||
Theorem | elabgf1 12986 | One implication of elabgf 2826. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝜓) | ||||||||||||||||||||||||||
Theorem | elabgf2 12987 | One implication of elabgf 2826. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝜓 → 𝐴 ∈ {𝑥 ∣ 𝜑})) | ||||||||||||||||||||||||||
Theorem | elabf1 12988* | One implication of elabf 2827. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝜓) | ||||||||||||||||||||||||||
Theorem | elabf2 12989* | One implication of elabf 2827. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝜓 → 𝐴 ∈ {𝑥 ∣ 𝜑}) | ||||||||||||||||||||||||||
Theorem | elab1 12990* | One implication of elab 2828. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝜓) | ||||||||||||||||||||||||||
Theorem | elab2a 12991* | One implication of elab 2828. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝜓 → 𝐴 ∈ {𝑥 ∣ 𝜑}) | ||||||||||||||||||||||||||
Theorem | elabg2 12992* | One implication of elabg 2830. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → 𝐴 ∈ {𝑥 ∣ 𝜑})) | ||||||||||||||||||||||||||
Theorem | bj-rspgt 12993 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2786 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))) | ||||||||||||||||||||||||||
Theorem | bj-rspg 12994 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2786 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) | ||||||||||||||||||||||||||
Theorem | cbvrald 12995* | Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) | ||||||||||||||||||||||||||
Theorem | bj-intabssel 12996 | Version of intss1 3786 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴)) | ||||||||||||||||||||||||||
Theorem | bj-intabssel1 12997 | Version of intss1 3786 using a class abstraction and implicit substitution. Closed form of intmin3 3798. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴)) | ||||||||||||||||||||||||||
Theorem | bj-elssuniab 12998 | Version of elssuni 3764 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||||||||||||||
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 → 𝐴 ⊆ ∪ {𝑥 ∣ 𝜑})) | ||||||||||||||||||||||||||
Theorem | bj-sseq 12999 | If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ↔ 𝐴 ⊆ 𝐵)) & ⊢ (𝜑 → (𝜒 ↔ 𝐵 ⊆ 𝐴)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝐴 = 𝐵)) | ||||||||||||||||||||||||||
The question of decidability is essential in intuitionistic logic. In intuitionistic set theories, it is natural to define decidability of a set (or class) as decidability of membership in it. One can parameterize this notion with another set (or class) since it is often important to assess decidability of membership in one class among elements of another class. Namely, one will say that "𝐴 is decidable in 𝐵 " if ∀𝑥 ∈ 𝐵DECID 𝑥 ∈ 𝐴 (see df-dcin 13001). Note the similarity with the definition of a bounded class as a class for which membership in it is a bounded proposition (df-bdc 13039). | ||||||||||||||||||||||||||
Syntax | wdcin 13000 | Syntax for decidability of a class in another. | ||||||||||||||||||||||||
wff 𝐴 DECIDin 𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |