P. 507 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50601-50625   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfralseu2 50601	The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 50568. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
Theorem	alseuals 50602	"All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 50616 is proved. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∀∃𝑥(𝜑 → 𝜓))
Theorem	ralseurals 50603	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 50602. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓))
Theorem	alseud 50604	Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 50606 and alseu2d 50607 taken together. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃!𝑥𝜓)    ⇒   ⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))
Theorem	ralseud 50605	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 50608 and ralseu2d 50609 taken together. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))
Theorem	alseu1d 50606	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
Theorem	alseu2d 50607	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃!𝑥𝜓)
Theorem	ralseu1d 50608	Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
Theorem	ralseu2d 50609	Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent 𝜓, not merely be a member of 𝐴. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	alseubii 50610	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 50578. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ ∀∃!𝑥(𝜒 → 𝜃))
Theorem	ralseubii 50611	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 50579. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥 ∈ 𝐴(𝜒 → 𝜃))
Theorem	nfalseu 50612*	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 50581. Unlike nfals 50581 it requires 𝑥 and 𝑦 to be disjoint, because the corresponding builder for ∃! is nfeuw 2621, which requires it; the version without that requirement, nfeu 2622, depends on ax-13 2404 and its use is discouraged. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃!𝑦(𝜑 → 𝜓)
Theorem	nfralseu 50613*	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 50582. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃!𝑦 ∈ 𝐴(𝜑 → 𝜓)
Theorem	dfalseu2 50614	An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one 𝑥 satisfies both 𝜑 and 𝜓. In other words, given ∀𝑥(𝜑 → 𝜓), requiring exactly one 𝑥 to satisfy 𝜑, which is what df-alseu 50599 requires, and requiring exactly one 𝑥 to satisfy (𝜑 ∧ 𝜓) come to the same thing. Read 𝜑 as "is a king" and 𝜓 as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry". The universal conjunct is what makes that work, and it cannot be dropped. ∃!𝑥(𝜑 ∧ 𝜓) on its own is strictly weaker than ∀∃!𝑥(𝜑 → 𝜓), since it is satisfied when many things are 𝜑 and just one of those is 𝜓, as in a region with five kings exactly one of whom is hungry; see alseueu 50615 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥(𝜑 ∧ 𝜓)))
Theorem	alseueu 50615	"The 𝜑 is 𝜓 " implies that exactly one thing is both 𝜑 and 𝜓. This is the half of dfalseu2 50614 that drops the universal conjunct; it does not reverse, so ∃!𝑥(𝜑 ∧ 𝜓) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∃!𝑥(𝜑 ∧ 𝜓))
Theorem	alseu-no-surprise 50616	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 50584 by alseuals 50602. For a contrast, see alimp-surprise 50558. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ ¬ (∀∃!𝑥(𝜑 → 𝜓) ∧ ∀∃!𝑥(𝜑 → ¬ 𝜓))
21.52.14  Miscellaneous Miscellaneous proofs.
Theorem	5m4e1 50617	Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.)
⊢ (5 − 4) = 1
Theorem	2p2ne5 50618	Prove that 2 + 2 ≠ 5. In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase 2 + 2 = 5 has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.)
⊢ (2 + 2) ≠ 5
Theorem	resolution 50619	Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒))
Theorem	testable 50620	In classical logic all wffs are testable, that is, it is always true that (¬ 𝜑 ∨ ¬ ¬ 𝜑). This is not necessarily true in intuitionistic logic. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is testable. The proof is trivial because it's simply a special case of the law of the excluded middle, which is true in classical logic but not necessarily true in intuitionisic logic. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ (¬ 𝜑 ∨ ¬ ¬ 𝜑)
21.52.15  Theorems about algebraic numbers
Theorem	aacllem 50621*	Lemma for other theorems about 𝔸. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝔸)
21.53  Mathbox for Kunhao Zheng
21.53.1  Weighted AM-GM inequality
Theorem	amgmwlem 50622	Weighted version of amgmlem 27154. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 50623	Alternate proof of amgmlem 27154 using amgmwlem 50622. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 50624	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 44924). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 50625	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 50624. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >