HomeTheorem List (p. 475 of 504)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 475 of 504) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31060) |
Hilbert Space Explorer
(31061-32583) |
Users' Mathboxes
(32584-50374) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | natglobalincr 47401* | Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.) |
| ⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1)) & ⊢ 𝑇 ∈ ℤ ⇒ ⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵‘𝑘) < (𝐵‘𝑡) | ||
| Theorem | chnsubseqword 47402 | A subsequence of a chain is a word. (Contributed by Ender Ting, 22-Jan-2026.) |
| ⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴)) & ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊)))) ⇒ ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ Word 𝐴) | ||
| Theorem | chnsubseqwl 47403 | A subsequence of a chain has the same length as its indexing sequence. (Contributed by Ender Ting, 22-Jan-2026.) |
| ⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴)) & ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊)))) ⇒ ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) = (♯‘𝐼)) | ||
| Theorem | chnsubseq 47404 | An order-preserving subsequence of an ordered chain is itself a chain. (Contributed by Ender Ting, 22-Jan-2026.) |
| ⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴)) & ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊)))) & ⊢ (𝜑 → < Po 𝐴) ⇒ ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ ( < Chain 𝐴)) | ||
| Theorem | chnsuslle 47405 | Length of a subsequence is bounded by the length of original chain. (Contributed by Ender Ting, 30-Jan-2026.) |
| ⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴)) & ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊)))) & ⊢ (𝜑 → < Po 𝐴) ⇒ ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) ≤ (♯‘𝑊)) | ||
| Theorem | chnerlem1 47406 | In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub 18630 to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026.) |
| ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) ⇒ ⊢ (𝜑 → (𝐶‘𝐽) ∼ (lastS‘𝐶)) | ||
| Theorem | chnerlem2 47407 | Lemma for chner 47409 where the I-th element comes before the J-th. (Contributed by Ender Ting, 29-Jan-2026.) |
| ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝐽)) → (𝐶‘𝐼) ∼ (𝐶‘𝐽)) | ||
| Theorem | chnerlem3 47408 | Lemma for chner 47409- trichotomy of integers within the word's domain. (Contributed by Ender Ting, 29-Jan-2026.) |
| ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) & ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶))) ⇒ ⊢ (𝜑 → (𝐼 ∈ (0..^𝐽) ∨ 𝐽 ∈ (0..^𝐼) ∨ 𝐼 = 𝐽)) | ||
| Theorem | chner 47409 | Any two elements are equivalent in a chain constructed on an equivalence relation. (Contributed by Ender Ting, 29-Jan-2026.) |
| ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) & ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶))) ⇒ ⊢ (𝜑 → (𝐶‘𝐼) ∼ (𝐶‘𝐽)) | ||
| Theorem | nthrucw 47410* | Some number sets form a chain of proper subsets. This is rephrasing nthruc 16260 as a statement about chains; the hypothesis sets the ordering relation to be "is a proper subset". The theorem talks about singleton 1, natural numbers, natural-or-zero numbers, integers, rational numbers, algebraic reals (the definition includes complex numbers as algebraic so intersection is taken), real numbers and complex numbers, which are proper subsets in order. (Contributed by Ender Ting, 29-Jan-2026.) |
| ⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦} ⇒ ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V) | ||
| Theorem | evenwodadd 47411 | If an integer is multiplied by its sum with an odd number (thus changing its parity), the result is even. (Contributed by Ender Ting, 30-Apr-2025.) |
| ⊢ (𝜑 → 𝑖 ∈ ℤ) & ⊢ (𝜑 → 𝑗 ∈ ℤ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑗) ⇒ ⊢ (𝜑 → 2 ∥ (𝑖 · (𝑖 + 𝑗))) | ||
| Theorem | squeezedltsq 47412 | If a real value is squeezed between two others, its square is less than square of at least one of them. Deduction form. (Contributed by Ender Ting, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ((𝐵 · 𝐵) < (𝐴 · 𝐴) ∨ (𝐵 · 𝐵) < (𝐶 · 𝐶))) | ||
| Theorem | sin3t 47413 | Triple-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 16-Mar-2026.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘(3 · 𝐴)) = ((3 · (sin‘𝐴)) − (4 · ((sin‘𝐴)↑3)))) | ||
| Theorem | cos3t 47414 | Triple-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 16-Mar-2026.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴)))) | ||
| Theorem | sin5tlem1 47415 | Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026.) |
| ⊢ (𝑁 ∈ ℂ → (((3 · 𝑁) − (4 · (𝑁↑3))) · (1 − (2 · (𝑁↑2)))) = (((8 · (𝑁↑5)) − (;10 · (𝑁↑3))) + (3 · 𝑁))) | ||
| Theorem | sin5tlem2 47416 | Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026.) |
| ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · 𝑁) = ((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2))))) | ||
| Theorem | sin5tlem3 47417 | Lemma 3 for quintupled angle sine calculation, multiplicating triple angle cosine by double angle sine. (Contributed by Ender Ting, 16-Apr-2026.) |
| ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = (((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2)))) · (2 · 𝑀))) | ||
| Theorem | sin5tlem4 47418 | Lemma 4 for quintupled angle sine calculation: expanding lemma 3 result to difference of polynomials. (Contributed by Ender Ting, 17-Apr-2026.) |
| ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3))))) | ||
| Theorem | sin5tlem5 47419 | Lemma 5 for quintupled angle sine calculation: sine of triple-angle and double-angle sum, as a polynomial in sine straight. (Contributed by Ender Ting, 17-Apr-2026.) |
| ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀))) | ||
| Theorem | sin5t 47420 | Five-times-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 17-Apr-2026.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘(5 · 𝐴)) = (((;16 · ((sin‘𝐴)↑5)) − (;20 · ((sin‘𝐴)↑3))) + (5 · (sin‘𝐴)))) | ||
| Theorem | cos5t 47421 | Five-times-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 20-Apr-2026.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘(5 · 𝐴)) = (((;16 · ((cos‘𝐴)↑5)) − (;20 · ((cos‘𝐴)↑3))) + (5 · (cos‘𝐴)))) | ||
| Theorem | cos5teq 47422 | Five-times-angle formula for cosine, substitution helper. (Contributed by Ender Ting, 9-May-2026.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 = (5 · 𝐴) ∧ 𝐶 = (cos‘𝐴)) → (cos‘𝐵) = (((;16 · (𝐶↑5)) − (;20 · (𝐶↑3))) + (5 · 𝐶))) | ||
| Theorem | goldrarr 47423 | The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ 𝐹 ∈ ℝ | ||
| Theorem | goldrasin 47424 | Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ 𝐹 = (2 · (sin‘(π · (3 / ;10)))) | ||
| Theorem | goldrapos 47425 | Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ 0 < 𝐹 | ||
| Theorem | goldrarp 47426 | The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ 𝐹 ∈ ℝ+ | ||
| Theorem | goldracos5teq 47427 | Lemma 1 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ (cos‘π) = (((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) + (5 · (𝐹 / 2))) | ||
| Theorem | goldratmolem2 47428 | Lemma 2 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.) |
| ⊢ 𝐹 = (2 · (cos‘(π / 5))) ⇒ ⊢ -1 = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2))) | ||
| Theorem | lambert0 47429 | A value of Lambert W (product logarithm) function at zero. (Contributed by Ender Ting, 13-Nov-2025.) |
| ⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥))) ⇒ ⊢ 0𝑅0 | ||
| Theorem | lamberte 47430 | A value of Lambert W (product logarithm) function at e. (Contributed by Ender Ting, 13-Nov-2025.) |
| ⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥))) ⇒ ⊢ e𝑅1 | ||
| Theorem | cjnpoly 47431 | Complex conjugation operator is not a polynomial with complex coefficients. Indeed; if it was, then multiplying 𝑥 conjugate by 𝑥 itself and adding 1 would yield a nowhere-zero non-constant polynomial, contrary to the fta 27114. (Contributed by Ender Ting, 8-Dec-2025.) |
| ⊢ ¬ ∗ ∈ (Poly‘ℂ) | ||
| Theorem | tannpoly 47432 | The tangent function is not a polynomial with complex coefficients, as it is not defined on the whole complex plane. (Contributed by Ender Ting, 10-Dec-2025.) |
| ⊢ ¬ tan ∈ (Poly‘ℂ) | ||
| Theorem | sinnpoly 47433 | Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 26342. (Contributed by Ender Ting, 10-Dec-2025.) |
| ⊢ ¬ sin ∈ (Poly‘ℂ) | ||
| Theorem | hirstL-ax3 47434 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑)) | ||
| Theorem | ax3h 47435 | Recover ax-3 8 from hirstL-ax3 47434. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
| Theorem | aibandbiaiffaiffb 47436 | A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓)) | ||
| Theorem | aibandbiaiaiffb 47437 | A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)) | ||
| Theorem | notatnand 47438 | Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
| Theorem | aistia 47439 | Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) ⇒ ⊢ 𝜑 | ||
| Theorem | aisfina 47440 | Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | bothtbothsame 47441 | Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
| Theorem | bothfbothsame 47442 | Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
| Theorem | aiffbbtat 47443 | Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ ⊤) | ||
| Theorem | aisbbisfaisf 47444 | Given a is equivalent to b, b is equivalent to ⊥ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | axorbtnotaiffb 47445 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1526 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜓) ⇒ ⊢ ¬ (𝜑 ↔ 𝜓) | ||
| Theorem | aiffnbandciffatnotciffb 47446 | Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ ¬ (𝜒 ↔ 𝜓) | ||
| Theorem | axorbciffatcxorb 47447 | Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ (𝜒 ⊻ 𝜓) | ||
| Theorem | aibnbna 47448 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | aibnbaif 47449 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | aiffbtbat 47450 | Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (⊤ ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ⊤) | ||
| Theorem | astbstanbst 47451 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ ((𝜑 ∧ 𝜓) ↔ ⊤) | ||
| Theorem | aistbistaandb 47452 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ∧ 𝜓) | ||
| Theorem | aisbnaxb 47453 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ (𝜑 ⊻ 𝜓) | ||
| Theorem | atbiffatnnb 47454 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
| Theorem | bisaiaisb 47455 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | ||
| Theorem | atbiffatnnbalt 47456 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
| Theorem | abnotbtaxb 47457 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | abnotataxb 47458 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ¬ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | conimpf 47459 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | conimpfalt 47460 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | aistbisfiaxb 47461 | Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | aisfbistiaxb 47462 | Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | aifftbifffaibif 47463 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ ((𝜑 → 𝜓) ↔ ⊥) | ||
| Theorem | aifftbifffaibifff 47464 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ ((𝜑 ↔ 𝜓) ↔ ⊥) | ||
| Theorem | atnaiana 47465 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)) | ||
| Theorem | ainaiaandna 47466 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))) | ||
| Theorem | abcdta 47467 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜑 | ||
| Theorem | abcdtb 47468 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜓 | ||
| Theorem | abcdtc 47469 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜒 | ||
| Theorem | abcdtd 47470 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜃 | ||
| Theorem | abciffcbatnabciffncba 47471 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
| Theorem | abciffcbatnabciffncbai 47472 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) ⇒ ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
| Theorem | nabctnabc 47473 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒)) | ||
| Theorem | jabtaib 47474 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
| ⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | onenotinotbothi 47475 | From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ ¬ (𝜑 → 𝜓) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
| Theorem | twonotinotbothi 47476 | From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ ¬ (𝜑 → 𝜓) & ⊢ ¬ (𝜒 → 𝜃) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
| Theorem | clifte 47477 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ (𝜑 ∧ ¬ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
| Theorem | cliftet 47478 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ (𝜑 ∧ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
| Theorem | clifteta 47479 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
| Theorem | cliftetb 47480 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
| Theorem | confun 47481 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ 𝜑 & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
| Theorem | confun2 47482 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓))) & ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑)) ⇒ ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑))) | ||
| Theorem | confun3 47483 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ (𝜑 ↔ (𝜒 → 𝜓)) & ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓)) ⇒ ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓))) | ||
| Theorem | confun4 47484 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜓 → 𝜏)) | ||
| Theorem | confun5 47485 | An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜂 ↔ 𝜏)) | ||
| Theorem | plcofph 47486 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
| Theorem | pldofph 47487 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
| Theorem | plvcofph 47488 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 ⇒ ⊢ 𝜂 | ||
| Theorem | plvcofphax 47489 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 & ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏)) ⇒ ⊢ 𝜁 | ||
| Theorem | plvofpos 47490 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂)))) & ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂)))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎)) & ⊢ 𝜁 & ⊢ 𝜎 ⇒ ⊢ 𝜌 | ||
| Theorem | mdandyv0 47491 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv1 47492 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv2 47493 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv3 47494 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv4 47495 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv5 47496 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv6 47497 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv7 47498 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv8 47499 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv9 47500 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |