P. 502 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50101-50117   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-alsc 50101	Define "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴 and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))
Theorem	alsconv 50102	There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.)
⊢ (∀!𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀!𝑥 ∈ 𝐴𝜑)
Theorem	alsi1d 50103	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
Theorem	alsi2d 50104	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	alsc1d 50105	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	alsc2d 50106	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	alscn0d 50107*	Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.)
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	alsi-no-surprise 50108	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-alsi 50100; the proof itself builds on alimp-no-surprise 50093. For a contrast, see alimp-surprise 50092. (Contributed by David A. Wheeler, 27-Oct-2018.)
⊢ ¬ (∀!𝑥(𝜑 → 𝜓) ∧ ∀!𝑥(𝜑 → ¬ 𝜓))
21.51.13  Miscellaneous Miscellaneous proofs.
Theorem	5m4e1 50109	Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.)
⊢ (5 − 4) = 1
Theorem	2p2ne5 50110	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 50111	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 50112	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.51.14  Theorems about algebraic numbers
Theorem	aacllem 50113*	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.52  Mathbox for Kunhao Zheng
21.52.1  Weighted AM-GM inequality
Theorem	amgmwlem 50114	Weighted version of amgmlem 26960. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 50115	Alternate proof of amgmlem 26960 using amgmwlem 50114. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 50116	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 44506). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 50117	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 50116. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >