![]() |
Metamath
Proof Explorer Theorem List (p. 469 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | finfdm 46801* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 46773. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) ⇒ ⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) | ||
Theorem | finfdm2 46802* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 46773. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) ⇒ ⊢ (𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) | ||
Theorem | smfinfdmmbllem 46803* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)})) ⇒ ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) | ||
Theorem | smfinfdmmbl 46804* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) | ||
Theorem | sigarval 46805* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵))) | ||
Theorem | sigarim 46806* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) ∈ ℝ) | ||
Theorem | sigarac 46807* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴)) | ||
Theorem | sigaraf 46808* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) + (𝐶𝐺𝐵))) | ||
Theorem | sigarmf 46809* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) − (𝐶𝐺𝐵))) | ||
Theorem | sigaras 46810* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 + 𝐶)) = ((𝐴𝐺𝐵) + (𝐴𝐺𝐶))) | ||
Theorem | sigarms 46811* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶))) | ||
Theorem | sigarls 46812* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) → (𝐴𝐺(𝐵 · 𝐶)) = ((𝐴𝐺𝐵) · 𝐶)) | ||
Theorem | sigarid 46813* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ (𝐴 ∈ ℂ → (𝐴𝐺𝐴) = 0) | ||
Theorem | sigarexp 46814* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = (((𝐴𝐺𝐵) − (𝐴𝐺𝐶)) − (𝐶𝐺𝐵))) | ||
Theorem | sigarperm 46815* | Signed area (𝐴 − 𝐶)𝐺(𝐵 − 𝐶) acts as a double area of a triangle 𝐴𝐵𝐶. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴))) | ||
Theorem | sigardiv 46816* | If signed area between vectors 𝐵 − 𝐴 and 𝐶 − 𝐴 is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → ¬ 𝐶 = 𝐴) & ⊢ (𝜑 → ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)) = 0) ⇒ ⊢ (𝜑 → ((𝐵 − 𝐴) / (𝐶 − 𝐴)) ∈ ℝ) | ||
Theorem | sigarimcd 46817* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ⇒ ⊢ (𝜑 → (𝐴𝐺𝐵) ∈ ℂ) | ||
Theorem | sigariz 46818* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) & ⊢ (𝜑 → (𝐴𝐺𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵𝐺𝐴) = 0) | ||
Theorem | sigarcol 46819* | Given three points 𝐴, 𝐵 and 𝐶 such that ¬ 𝐴 = 𝐵, the point 𝐶 lies on the line going through 𝐴 and 𝐵 iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = 0 ↔ ∃𝑡 ∈ ℝ 𝐶 = (𝐵 + (𝑡 · (𝐴 − 𝐵))))) | ||
Theorem | sharhght 46820* | Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷))) | ||
Theorem | sigaradd 46821* | Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶))) | ||
Theorem | cevathlem1 46822 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) & ⊢ (𝜑 → (𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0)) & ⊢ (𝜑 → ((𝐴 · 𝐵) = (𝐶 · 𝐷) ∧ (𝐸 · 𝐹) = (𝐴 · 𝐺) ∧ (𝐶 · 𝐻) = (𝐸 · 𝐾))) ⇒ ⊢ (𝜑 → ((𝐵 · 𝐹) · 𝐻) = ((𝐷 · 𝐺) · 𝐾)) | ||
Theorem | cevathlem2 46823* | Ceva's theorem second lemma. Relate (doubled) areas of triangles 𝐶𝐴𝑂 and 𝐴𝐵𝑂 with of segments 𝐵𝐷 and 𝐷𝐶. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) · (𝐵 − 𝐷)) = (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) · (𝐷 − 𝐶))) | ||
Theorem | cevath 46824* |
Ceva's theorem. Let 𝐴𝐵𝐶 be a triangle and let points 𝐹,
𝐷 and 𝐸 lie on sides 𝐴𝐵, 𝐵𝐶, 𝐶𝐴
correspondingly. Suppose that cevians 𝐴𝐷, 𝐵𝐸 and 𝐶𝐹
intersect at one point 𝑂. Then triangle's sides are
partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 46823 three times and then using cevathlem1 46822 to multiply obtained identities and prove the theorem. In the theorem statement we are using function 𝐺 as a collinearity indicator. For justification of that use, see sigarcol 46819. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶))) | ||
Theorem | simpcntrab 46825 | The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (𝑍 = { 0 } ∨ 𝐺 ∈ Abel)) | ||
Theorem | et-ltneverrefl 46826 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11367. (New usage is discouraged.) |
⊢ ¬ 𝐴 < 𝐴 | ||
Theorem | et-equeucl 46827 | Alternative proof that equality is left-Euclidean, using ax7 2012 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦)) | ||
Theorem | et-sqrtnegnre 46828 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → ¬ (√‘𝐴) ∈ ℝ) | ||
Theorem | natlocalincr 46829* | Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024.) |
⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘) < (𝐵‘𝑡)) ⇒ ⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1)) | ||
Theorem | natglobalincr 46830* | Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.) |
⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1)) & ⊢ 𝑇 ∈ ℤ ⇒ ⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵‘𝑘) < (𝐵‘𝑡) | ||
Syntax | cupword 46831 | Extend class notation to include the set of strictly increasing sequences. |
class UpWord 𝑆 | ||
Definition | df-upword 46832* | Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024.) |
⊢ UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))} | ||
Theorem | upwordnul 46833 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
⊢ ∅ ∈ UpWord 𝑆 | ||
Theorem | upwordisword 46834 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
⊢ (𝐴 ∈ UpWord 𝑆 → 𝐴 ∈ Word 𝑆) | ||
Theorem | singoutnword 46835 | Singleton with character out of range 𝑉 is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (¬ 𝐴 ∈ 𝑉 → ¬ 〈“𝐴”〉 ∈ Word 𝑉) | ||
Theorem | singoutnupword 46836 | Singleton with character out of range 𝑆 is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (¬ 𝐴 ∈ 𝑆 → ¬ 〈“𝐴”〉 ∈ UpWord 𝑆) | ||
Theorem | upwordsing 46837 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
⊢ 𝐴 ∈ 𝑆 ⇒ ⊢ 〈“𝐴”〉 ∈ UpWord 𝑆 | ||
Theorem | upwordsseti 46838 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
⊢ 𝑆 ∈ V ⇒ ⊢ UpWord 𝑆 ∈ V | ||
Theorem | tworepnotupword 46839 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ¬ (〈“𝐴”〉 ++ 〈“𝐴”〉) ∈ UpWord 𝑆 | ||
Theorem | upwrdfi 46840* | There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024.) |
⊢ (𝑆 ∈ Fin → {𝑎 ∈ UpWord 𝑆 ∣ (♯‘𝑎) = 𝑇} ∈ Fin) | ||
Theorem | hirstL-ax3 46841 | 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 46842 | Recover ax-3 8 from hirstL-ax3 46841. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | aibandbiaiffaiffb 46843 | 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 46844 | 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 46845 | 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 46846 | Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊤) ⇒ ⊢ 𝜑 | ||
Theorem | aisfina 46847 | Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊥) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bothtbothsame 46848 | 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 46849 | 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 46850 | 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 46851 | 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 46852 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1508 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜓) ⇒ ⊢ ¬ (𝜑 ↔ 𝜓) | ||
Theorem | aiffnbandciffatnotciffb 46853 | 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 46854 | 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 46855 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | aibnbaif 46856 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
Theorem | aiffbtbat 46857 | 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 46858 | 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 46859 | 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 46860 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ (𝜑 ⊻ 𝜓) | ||
Theorem | atbiffatnnb 46861 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | bisaiaisb 46862 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | ||
Theorem | atbiffatnnbalt 46863 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | abnotbtaxb 46864 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | abnotataxb 46865 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ¬ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | conimpf 46866 | 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 46867 | 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 46868 | 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 46869 | 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 46870 | 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 46871 | 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 46872 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)) | ||
Theorem | ainaiaandna 46873 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))) | ||
Theorem | abcdta 46874 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜑 | ||
Theorem | abcdtb 46875 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜓 | ||
Theorem | abcdtc 46876 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜒 | ||
Theorem | abcdtd 46877 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | abciffcbatnabciffncba 46878 | 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 46879 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) ⇒ ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
Theorem | nabctnabc 46880 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jabtaib 46881 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | onenotinotbothi 46882 | 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 46883 | 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 46884 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ ¬ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftet 46885 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | clifteta 46886 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftetb 46887 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | confun 46888 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | confun2 46889 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓))) & ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑)) ⇒ ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑))) | ||
Theorem | confun3 46890 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜑 ↔ (𝜒 → 𝜓)) & ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓)) ⇒ ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓))) | ||
Theorem | confun4 46891 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜓 → 𝜏)) | ||
Theorem | confun5 46892 | 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 46893 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
Theorem | pldofph 46894 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | plvcofph 46895 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 ⇒ ⊢ 𝜂 | ||
Theorem | plvcofphax 46896 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 & ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏)) ⇒ ⊢ 𝜁 | ||
Theorem | plvofpos 46897 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂)))) & ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂)))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎)) & ⊢ 𝜁 & ⊢ 𝜎 ⇒ ⊢ 𝜌 | ||
Theorem | mdandyv0 46898 | 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 46899 | 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 46900 | 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 > |