P. 509 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50801-50805   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	veroquaddetzerod 50801*	The Veronese matrix of six points satisfying a common nonzero homogeneous quadratic equation has determinant zero. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0)    &   ⊢ (𝜑 → 𝐾 ≠ ((1...6) × {0}))    ⇒   ⊢ (𝜑 → (((1...6) maDet ℝfld)‘𝑉) = 0)
21.56  Mathbox for Kunhao Zheng
21.56.1  Weighted AM-GM inequality
Theorem	amgmwlem 50802	Weighted version of amgmlem 27222. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 50803	Alternate proof of amgmlem 27222 using amgmwlem 50802. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 50804	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 45023). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 50805	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 50804. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >