![]() |
Metamath
Proof Explorer Theorem List (p. 487 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 | line2 48601* | Example for a line 𝐺 passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} & ⊢ 𝑋 = {〈1, 0〉, 〈2, (𝐶 / 𝐵)〉} & ⊢ 𝑌 = {〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉} ⇒ ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = (𝑋𝐿𝑌)) | ||
Theorem | line2xlem 48602* | Lemma for line2x 48603. This proof is based on counterexamples for the following cases: 1. 𝑀 ≠ (𝐶 / 𝐵): p = (0,C/B) (LHS of biconditional is true, RHS is false); 2. 𝐴 ≠ 0 ∧ 𝑀 = (𝐶 / 𝐵): p = (1,C/B) (LHS of biconditional is false, RHS is true). (Contributed by AV, 4-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} & ⊢ 𝑋 = {〈1, 0〉, 〈2, 𝑀〉} & ⊢ 𝑌 = {〈1, 1〉, 〈2, 𝑀〉} ⇒ ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)))) | ||
Theorem | line2x 48603* | Example for a horizontal line 𝐺 passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} & ⊢ 𝑋 = {〈1, 0〉, 〈2, 𝑀〉} & ⊢ 𝑌 = {〈1, 1〉, 〈2, 𝑀〉} ⇒ ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)))) | ||
Theorem | line2y 48604* | Example for a vertical line 𝐺 passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} & ⊢ 𝑋 = {〈1, 0〉, 〈2, 𝑀〉} & ⊢ 𝑌 = {〈1, 0〉, 〈2, 𝑁〉} ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0))) | ||
Theorem | itsclc0lem1 48605 | Lemma for theorems about intersections of lines and circles in a real Euclidean space of dimension 2 . (Contributed by AV, 2-May-2023.) |
⊢ (((𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ (𝑊 ∈ ℝ ∧ 𝑊 ≠ 0)) → (((𝑆 · 𝑈) + (𝑇 · (√‘𝑉))) / 𝑊) ∈ ℝ) | ||
Theorem | itsclc0lem2 48606 | Lemma for theorems about intersections of lines and circles in a real Euclidean space of dimension 2 . (Contributed by AV, 3-May-2023.) |
⊢ (((𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ (𝑊 ∈ ℝ ∧ 𝑊 ≠ 0)) → (((𝑆 · 𝑈) − (𝑇 · (√‘𝑉))) / 𝑊) ∈ ℝ) | ||
Theorem | itsclc0lem3 48607 | Lemma for theorems about intersections of lines and circles in a real Euclidean space of dimension 2 . (Contributed by AV, 2-May-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ) | ||
Theorem | itscnhlc0yqe 48608 | Lemma for itsclc0 48620. Quadratic equation for the y-coordinate of the intersection points of a nonhorizontal line and a circle. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | itschlc0yqe 48609 | Lemma for itsclc0 48620. Quadratic equation for the y-coordinate of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | itsclc0yqe 48610 | Lemma for itsclc0 48620. Quadratic equation for the y-coordinate of the intersection points of an arbitrary line and a circle. This theorem holds even for degenerate lines (𝐴 = 𝐵 = 0). (Contributed by AV, 25-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | itsclc0yqsollem1 48611 | Lemma 1 for itsclc0yqsol 48613. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷)) | ||
Theorem | itsclc0yqsollem2 48612 | Lemma 2 for itsclc0yqsol 48613. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷))) | ||
Theorem | itsclc0yqsol 48613 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))) | ||
Theorem | itscnhlc0xyqsol 48614 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a nonhorizontal line and a circle. (Contributed by AV, 8-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itschlc0xyqsol1 48615 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (𝐶 / 𝐵) ∧ (𝑋 = -((√‘𝐷) / 𝐵) ∨ 𝑋 = ((√‘𝐷) / 𝐵))))) | ||
Theorem | itschlc0xyqsol 48616 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 8-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itsclc0xyqsol 48617 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 25-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itsclc0xyqsolr 48618 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶))) | ||
Theorem | itsclc0xyqsolb 48619 | Lemma for itsclc0 48620. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ ((𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ))) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itsclc0 48620* | The intersection points of a line 𝐿 and a circle around the origin. (Contributed by AV, 25-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ 𝐿) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itsclc0b 48621* | The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ 𝐿) ↔ (𝑋 ∈ 𝑃 ∧ (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) | ||
Theorem | itsclinecirc0 48622 | The intersection points of a line through two different points 𝑌 and 𝑍 and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 25-Feb-2023.) (Proof shortened by AV, 16-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑌‘2) − (𝑍‘2)) & ⊢ 𝐵 = ((𝑍‘1) − (𝑌‘1)) & ⊢ 𝐶 = (((𝑌‘2) · (𝑍‘1)) − ((𝑌‘1) · (𝑍‘2))) ⇒ ⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ (𝑌𝐿𝑍)) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | ||
Theorem | itsclinecirc0b 48623 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ (𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑍‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) | ||
Theorem | itsclinecirc0in 48624 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) | ||
Theorem | itsclquadb 48625* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (∃𝑥 ∈ ℝ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | itsclquadeu 48626* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 23-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | 2itscplem1 48627 | Lemma 1 for 2itscp 48630. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) ⇒ ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2)) | ||
Theorem | 2itscplem2 48628 | Lemma 2 for 2itscp 48630. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) ⇒ ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) | ||
Theorem | 2itscplem3 48629 | Lemma D for 2itscp 48630. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | ||
Theorem | 2itscp 48630 | A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023.) (Revised by AV, 16-May-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → (𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋)) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 0 < 𝑆) | ||
Theorem | itscnhlinecirc02plem1 48631 | Lemma 1 for itscnhlinecirc02p 48634. (Contributed by AV, 6-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → 𝐵 ≠ 𝑌) ⇒ ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem2 48632 | Lemma 2 for itscnhlinecirc02p 48634. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem3 48633 | Lemma 3 for itscnhlinecirc02p 48634. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 0 < ((-(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))↑2) − (4 · (((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02p 48634* | Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 𝑍 = {〈1, 𝑥〉, 〈2, 𝑦〉} ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)))) | ||
Theorem | inlinecirc02plem 48635* | Lemma for inlinecirc02p 48636. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) | ||
Theorem | inlinecirc02p 48636 | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 9-May-2023.) (Revised by AV, 16-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ∈ (Pairsproper‘𝑃)) | ||
Theorem | inlinecirc02preu 48637* | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑝 ∈ 𝒫 𝑃((♯‘𝑝) = 2 ∧ 𝑝 = (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)))) | ||
Theorem | pm4.71da 48638 | Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 561. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | logic1 48639 | Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic1a 48640 | Variant of logic1 48639. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic2 48641 | Variant of logic1 48639. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | pm5.32dav 48642 | Distribution of implication over biconditional (deduction form). Variant of pm5.32da 579. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) | ||
Theorem | pm5.32dra 48643 | Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | ||
Theorem | exp12bd 48644 | The import-export theorem (impexp 450) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜏 ∧ 𝜂) → 𝜁))) ⇒ ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) ↔ (𝜏 → (𝜂 → 𝜁)))) | ||
Theorem | mpbiran3d 48645 | Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | mpbiran4d 48646 | Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 27-Sep-2024.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | dtrucor3 48647* | An example of how ax-5 1907 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5446 in the ZF set theory. axc16nf 2260 and euae 2657 demonstrate that the violation of dtru 5446 leads to a model with only one object assuming its existence (ax-6 1964). The conclusion is also provable in the empty model ( see emptyal 1905). See also nf5 2280 and nf5i 2143 for the relation between unconditional ax-5 1907 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 & ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦) ⇒ ⊢ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | ralbidb 48648* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 48649 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | ralbidc 48649* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 48648. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | r19.41dv 48650* | A complex deduction form of r19.41v 3186. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) | ||
Theorem | rmotru 48651 | Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑥 ∈ 𝐴 ⊤) | ||
Theorem | reutru 48652 | Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤) | ||
Theorem | reutruALT 48653 | Alternate proof for reutru 48652. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤) | ||
Theorem | reuxfr1dd 48654* | Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Simplifies reuxfr1d 3758. (Contributed by Zhi Wang, 20-Sep-2025.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ssdisjd 48655 | Subset preserves disjointness. Deduction form of ssdisj 4465. (Contributed by Zhi Wang, 7-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | ssdisjdr 48656 | Subset preserves disjointness. Deduction form of ssdisj 4465. Alternatively this could be proved with ineqcom 4217 in tandem with ssdisjd 48655. (Contributed by Zhi Wang, 7-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝐶 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = ∅) | ||
Theorem | disjdifb 48657 | Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.) |
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | predisj 48658 | Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝐴)) & ⊢ (𝜑 → 𝑇 ⊆ (◡𝐹 “ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) | ||
Theorem | vsn 48659 | The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ {V} = ∅ | ||
Theorem | mosn 48660* | "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐴 = {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mo0 48661* | "At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐴 = ∅ → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mosssn 48662* | "At most one" element in a subclass of a singleton. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (𝐴 ⊆ {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mo0sn 48663* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑦 𝐴 = {𝑦})) | ||
Theorem | mosssn2 48664* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝐴 ⊆ {𝑦}) | ||
Theorem | unilbss 48665* | Superclass of the greatest lower bound. A dual statement of ssintub 4970. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐴 | ||
Theorem | inpw 48666* | Two ways of expressing a collection of subsets as seen in df-ntr 23043, unimax 4948, and others (Contributed by Zhi Wang, 27-Sep-2024.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝐵}) | ||
Theorem | mof0 48667 | There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ ∃*𝑓 𝑓:𝐴⟶∅ | ||
Theorem | mof02 48668* | A variant of mof0 48667. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝐵 = ∅ → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mof0ALT 48669* | Alternate proof for mof0 48667 with stronger requirements on distinct variables. Uses mo4 2563. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃*𝑓 𝑓:𝐴⟶∅ | ||
Theorem | eufsnlem 48670* | There is exactly one function into a singleton. For a simpler hypothesis, see eufsn 48671 assuming ax-rep 5284, or eufsn2 48672 assuming ax-pow 5370 and ax-un 7753. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | eufsn 48671* | There is exactly one function into a singleton, assuming ax-rep 5284. See eufsn2 48672 for different axiom requirements. If existence is not needed, use mofsn 48673 or mofsn2 48674 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | eufsn2 48672* | There is exactly one function into a singleton, assuming ax-pow 5370 and ax-un 7753. Variant of eufsn 48671. If existence is not needed, use mofsn 48673 or mofsn2 48674 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | mofsn 48673* | There is at most one function into a singleton, with fewer axioms than eufsn 48671 and eufsn2 48672. See also mofsn2 48674. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐵 ∈ 𝑉 → ∃*𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | mofsn2 48674* | There is at most one function into a singleton. An unconditional variant of mofsn 48673, i.e., the singleton could be empty if 𝑌 is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐵 = {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mofsssn 48675* | There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝐵 ⊆ {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mofmo 48676* | There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐵 → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mofeu 48677* | The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐺 = (𝐴 × 𝐵) & ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅)) & ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹 = 𝐺)) | ||
Theorem | elfvne0 48678 | If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024.) |
⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐹 ≠ ∅) | ||
Theorem | fdomne0 48679 | A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ≠ ∅) → (𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅)) | ||
Theorem | f1sn2g 48680 | A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:{𝐴}⟶𝐵) → 𝐹:{𝐴}–1-1→𝐵) | ||
Theorem | f102g 48681 | A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ ((𝐴 = ∅ ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | f1mo 48682* | A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | f002 48683 | A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅)) | ||
Theorem | map0cor 48684* | A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝐵 = ∅ → 𝐴 = ∅) ↔ ∃𝑓 𝑓:𝐴⟶𝐵)) | ||
Theorem | fvconstr 48685 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌)) | ||
Theorem | fvconstrn0 48686 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅)) | ||
Theorem | fvconstr2 48687 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵)) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐵) | ||
Theorem | fvconst0ci 48688 | A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ 𝐵 ∈ V & ⊢ 𝑌 = ((𝐴 × {𝐵})‘𝑋) ⇒ ⊢ (𝑌 = ∅ ∨ 𝑌 = 𝐵) | ||
Theorem | fvconstdomi 48689 | A constant function's value is dominated by the constant. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 × {𝐵})‘𝑋) ≼ 𝐵 | ||
Theorem | f1omo 48690* | There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi 48689 assuming ax-un 7753 (see f1omoALT 48691). (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝐴 × {1o})) ⇒ ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋)) | ||
Theorem | f1omoALT 48691* | There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Use f1omo 48690 without assuming ax-un 7753. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 = (𝐴 × {1o})) ⇒ ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋)) | ||
Theorem | iccin 48692 | Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | iccdisj2 48693 | If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅) | ||
Theorem | iccdisj 48694 | If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅) | ||
Theorem | mreuniss 48695 | The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → ∪ 𝑆 ⊆ 𝑋) | ||
Additional contents for topology. | ||
Theorem | clduni 48696 | The union of closed sets is the underlying set of the topology (the union of open sets). (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝐽 ∈ Top → ∪ (Clsd‘𝐽) = ∪ 𝐽) | ||
Theorem | opncldeqv 48697* | Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑥 = (∪ 𝐽 ∖ 𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐽 𝜓 ↔ ∀𝑦 ∈ (Clsd‘𝐽)𝜒)) | ||
Theorem | opndisj 48698 | Two ways of saying that two open sets are disjoint, if 𝐽 is a topology and 𝑋 is an open set. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ (𝐽 ∩ 𝒫 𝑍) ↔ (𝑌 ∈ 𝐽 ∧ (𝑋 ∩ 𝑌) = ∅))) | ||
Theorem | clddisj 48699 | Two ways of saying that two closed sets are disjoint, if 𝐽 is a topology and 𝑋 is a closed set. An alternative proof is similar to that of opndisj 48698 with elssuni 4941 replaced by the combination of cldss 23052 and eqid 2734. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑍) ↔ (𝑌 ∈ (Clsd‘𝐽) ∧ (𝑋 ∩ 𝑌) = ∅))) | ||
Theorem | neircl 48700 | Reverse closure of the neighborhood operation. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by Zhi Wang, 16-Sep-2024.) |
⊢ (𝑁 ∈ ((nei‘𝐽)‘𝑆) → 𝐽 ∈ Top) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |