![]() |
Metamath
Proof Explorer Theorem List (p. 472 of 476) | < 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-30098) |
![]() (30099-31621) |
![]() (31622-47564) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | affinecomb2 47101* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | ||
Theorem | affineid 47102 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴) | ||
Theorem | 1subrec1sub 47103 | Subtract the reciprocal of 1 minus a number from 1 results in the number divided by the number minus 1. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 1) → (1 − (1 / (1 − 𝐴))) = (𝐴 / (𝐴 − 1))) | ||
Theorem | resum2sqcl 47104 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ) | ||
Theorem | resum2sqgt0 47105 | The sum of the square of a nonzero real number and the square of another real number is greater than zero. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 0 < 𝑄) | ||
Theorem | resum2sqrp 47106 | The sum of the square of a nonzero real number and the square of another real number is a positive real number. (Contributed by AV, 2-May-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ+) | ||
Theorem | resum2sqorgt0 47107 | The sum of the square of two real numbers is greater than zero if at least one of the real numbers is nonzero. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄) | ||
Theorem | reorelicc 47108 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶)) | ||
Theorem | rrx2pxel 47109 | The x-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) | ||
Theorem | rrx2pyel 47110 | The y-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) | ||
Theorem | prelrrx2 47111 | An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2. (Contributed by AV, 4-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {〈1, 𝐴〉, 〈2, 𝐵〉} ∈ 𝑃) | ||
Theorem | prelrrx2b 47112 | An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = 𝐴 ∧ (𝑍‘2) = 𝐵) ∨ ((𝑍‘1) = 𝑋 ∧ (𝑍‘2) = 𝑌))) ↔ 𝑍 ∈ {{〈1, 𝐴〉, 〈2, 𝐵〉}, {〈1, 𝑋〉, 〈2, 𝑌〉}})) | ||
Theorem | rrx2pnecoorneor 47113 | If two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 are different, then they are different at least at one coordinate. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑋‘1) ≠ (𝑌‘1) ∨ (𝑋‘2) ≠ (𝑌‘2))) | ||
Theorem | rrx2pnedifcoorneor 47114 | If two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐴 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐵 = ((𝑌‘2) − (𝑋‘2)) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | ||
Theorem | rrx2pnedifcoorneorr 47115 | If two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐴 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐵 = ((𝑋‘2) − (𝑌‘2)) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | ||
Theorem | rrx2xpref1o 47116* | There is a bijection between the set of ordered pairs of real numbers (the cartesian product of the real numbers) and the set of points in the two dimensional Euclidean plane (represented as mappings from {1, 2} to the real numbers). (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑅 = (ℝ ↑m {1, 2}) & ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) ⇒ ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→𝑅 | ||
Theorem | rrx2xpreen 47117 | The set of points in the two dimensional Euclidean plane and the set of ordered pairs of real numbers (the cartesian product of the real numbers) are equinumerous. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑅 = (ℝ ↑m {1, 2}) ⇒ ⊢ 𝑅 ≈ (ℝ × ℝ) | ||
Theorem | rrx2plord 47118* | The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point iff its first coordinate is less than the first coordinate of the other point, or the first coordinates of both points are equal and the second coordinate of the first point is less than the second coordinate of the other point: 〈𝑎, 𝑏〉 ≤ 〈𝑥, 𝑦〉 iff (𝑎 < 𝑥 ∨ (𝑎 = 𝑥 ∧ 𝑏 ≤ 𝑦)). (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} ⇒ ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝑂𝑌 ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) | ||
Theorem | rrx2plord1 47119* | The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point if its first coordinate is less than the first coordinate of the other point. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} ⇒ ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) < (𝑌‘1)) → 𝑋𝑂𝑌) | ||
Theorem | rrx2plord2 47120* | The lexicographical ordering for points in the two dimensional Euclidean plane: if the first coordinates of two points are equal, a point is less than another point iff the second coordinate of the point is less than the second coordinate of the other point. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} & ⊢ 𝑅 = (ℝ ↑m {1, 2}) ⇒ ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋𝑂𝑌 ↔ (𝑋‘2) < (𝑌‘2))) | ||
Theorem | rrx2plordisom 47121* | The set of points in the two dimensional Euclidean plane with the lexicographical ordering is isomorphic to the cartesian product of the real numbers with the lexicographical ordering implied by the ordering of the real numbers. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} & ⊢ 𝑅 = (ℝ ↑m {1, 2}) & ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ × ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) < (2nd ‘𝑦))))} ⇒ ⊢ 𝐹 Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) | ||
Theorem | rrx2plordso 47122* | The lexicographical ordering for points in the two dimensional Euclidean plane is a strict total ordering. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} & ⊢ 𝑅 = (ℝ ↑m {1, 2}) ⇒ ⊢ 𝑂 Or 𝑅 | ||
Theorem | ehl2eudisval0 47123 | The Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑m {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 0 = ({1, 2} × {0}) ⇒ ⊢ (𝐹 ∈ 𝑋 → (𝐹𝐷 0 ) = (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) | ||
Theorem | ehl2eudis0lt 47124 | An upper bound of the Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 9-May-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑m {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 0 = ({1, 2} × {0}) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝐹𝐷 0 ) < 𝑅 ↔ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) < (𝑅↑2))) | ||
Syntax | cline 47125 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 47126 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 47127* | Definition of lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023.) |
⊢ LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))})) | ||
Definition | df-sph 47128* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 23753, or even in any extended structure having a base set and a distance function into the real numbers. (Contributed by AV, 14-Jan-2023.) |
⊢ Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟})) | ||
Theorem | lines 47129* | The lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐿 = (LineM‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ (𝑊 ∈ 𝑉 → 𝐿 = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) | ||
Theorem | line 47130* | The line passing through the two different points 𝑋 and 𝑌 in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐿 = (LineM‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝑊 ∈ 𝑉 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑋) + (𝑡 · 𝑌))}) | ||
Theorem | rrxlines 47131* | Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ · = ( ·𝑠 ‘𝐸) & ⊢ + = (+g‘𝐸) ⇒ ⊢ (𝐼 ∈ Fin → 𝐿 = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ 𝑝 = (((1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) | ||
Theorem | rrxline 47132* | The line passing through the two different points 𝑋 and 𝑌 in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ · = ( ·𝑠 ‘𝐸) & ⊢ + = (+g‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ 𝑝 = (((1 − 𝑡) · 𝑋) + (𝑡 · 𝑌))}) | ||
Theorem | rrxlinesc 47133* | Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension, expressed by their coordinates. (Contributed by AV, 13-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ (𝐼 ∈ Fin → 𝐿 = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))})) | ||
Theorem | rrxlinec 47134* | The line passing through the two different points 𝑋 and 𝑌 in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc 47133. (Contributed by AV, 13-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))}) | ||
Theorem | eenglngeehlnmlem1 47135* | Lemma 1 for eenglngeehlnm 47137. (Contributed by AV, 15-Feb-2023.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → ((∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))) → ∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))) | ||
Theorem | eenglngeehlnmlem2 47136* | Lemma 2 for eenglngeehlnm 47137. (Contributed by AV, 15-Feb-2023.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → (∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) | ||
Theorem | eenglngeehlnm 47137 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 28171) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 47131). (Contributed by AV, 16-Feb-2023.) |
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁))) | ||
Theorem | rrx2line 47138* | The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023.) (Proof shortened by AV, 13-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ((𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1))) ∧ (𝑝‘2) = (((1 − 𝑡) · (𝑋‘2)) + (𝑡 · (𝑌‘2))))}) | ||
Theorem | rrx2vlinest 47139* | The vertical line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 in "standard form". (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)}) | ||
Theorem | rrx2linest 47140* | The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 in "standard form". (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐵 = ((𝑌‘2) − (𝑋‘2)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘2)) = ((𝐵 · (𝑝‘1)) + 𝐶)}) | ||
Theorem | rrx2linesl 47141* | The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2, expressed by the slope 𝑆 between the two points ("point-slope form"), sometimes also written as ((𝑝‘2) − (𝑋‘2)) = (𝑆 · ((𝑝‘1) − (𝑋‘1))). (Contributed by AV, 22-Jan-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝑆 = (((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘2) = ((𝑆 · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2))}) | ||
Theorem | rrx2linest2 47142* | The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 in another "standard form" (usually with (𝑝‘1) = 𝑥 and (𝑝‘2) = 𝑦). (Contributed by AV, 23-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) | ||
Theorem | elrrx2linest2 47143 | The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 in another "standard form" (usually with (𝑝‘1) = 𝑥 and (𝑝‘2) = 𝑦). (Contributed by AV, 23-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐺 ∈ (𝑋𝐿𝑌) ↔ (𝐺 ∈ 𝑃 ∧ ((𝐴 · (𝐺‘1)) + (𝐵 · (𝐺‘2))) = 𝐶))) | ||
Theorem | spheres 47144* | The spheres for given centers and radii in a metric space (or any extensible structure having a base set and a distance function). (Contributed by AV, 22-Jan-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Sphere‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑉 → 𝑆 = (𝑥 ∈ 𝐵, 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ 𝐵 ∣ (𝑝𝐷𝑥) = 𝑟})) | ||
Theorem | sphere 47145* | A sphere with center 𝑋 and radius 𝑅 in a metric space (or any extensible structure having a base set and a distance function). (Contributed by AV, 22-Jan-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Sphere‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ (0[,]+∞)) → (𝑋𝑆𝑅) = {𝑝 ∈ 𝐵 ∣ (𝑝𝐷𝑋) = 𝑅}) | ||
Theorem | rrxsphere 47146* | The sphere with center 𝑀 and radius 𝑅 in a generalized real Euclidean space of finite dimension. Remark: this theorem holds also for the degenerate case 𝑅 < 0 (negative radius): in this case, (𝑀𝑆𝑅) is empty. (Contributed by AV, 5-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 𝑆 = (Sphere‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝𝐷𝑀) = 𝑅}) | ||
Theorem | 2sphere 47147* | The sphere with center 𝑀 and radius 𝑅 in a two dimensional Euclidean space is a circle. (Contributed by AV, 5-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 𝐶 = {𝑝 ∈ 𝑃 ∣ ((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2)} ⇒ ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = 𝐶) | ||
Theorem | 2sphere0 47148* | The sphere around the origin 0 (see rrx0 24845) with radius 𝑅 in a two dimensional Euclidean space is a circle. (Contributed by AV, 5-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐶 = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ⇒ ⊢ (𝑅 ∈ (0[,)+∞) → ( 0 𝑆𝑅) = 𝐶) | ||
Theorem | line2ylem 47149* | Lemma for line2y 47153. This proof is based on counterexamples for the following cases: 1. 𝐶 ≠ 0: p = (0,0) (LHS of bicondional is false, RHS is true); 2. 𝐶 = 0 ∧ 𝐵 ≠ 0: p = (1,-A/B) (LHS of bicondional is true, RHS is false); 3. 𝐴 = 𝐵 = 𝐶 = 0: p = (1,1) (LHS of bicondional is true, RHS is false). (Contributed by AV, 4-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0))) | ||
Theorem | line2 47150* | 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 47151* | Lemma for line2x 47152. This proof is based on counterexamples for the following cases: 1. 𝑀 ≠ (𝐶 / 𝐵): p = (0,C/B) (LHS of bicondional is true, RHS is false); 2. 𝐴 ≠ 0 ∧ 𝑀 = (𝐶 / 𝐵): p = (1,C/B) (LHS of bicondional 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 47152* | 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 47153* | 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 47154 | 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 47155 | 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 47156 | 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 47157 | Lemma for itsclc0 47169. 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 47158 | Lemma for itsclc0 47169. 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 47159 | Lemma for itsclc0 47169. 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 47160 | Lemma 1 for itsclc0yqsol 47162. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷)) | ||
Theorem | itsclc0yqsollem2 47161 | Lemma 2 for itsclc0yqsol 47162. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷))) | ||
Theorem | itsclc0yqsol 47162 | Lemma for itsclc0 47169. 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 47163 | Lemma for itsclc0 47169. 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 47164 | Lemma for itsclc0 47169. 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 47165 | Lemma for itsclc0 47169. 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 47166 | Lemma for itsclc0 47169. 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 47167 | Lemma for itsclc0 47169. 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 47168 | Lemma for itsclc0 47169. 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 47169* | 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 47170* | 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 47171 | 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 47172 | 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 47173 | 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 47174* | 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 47175* | 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 47176 | Lemma 1 for 2itscp 47179. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) ⇒ ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2)) | ||
Theorem | 2itscplem2 47177 | Lemma 2 for 2itscp 47179. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) ⇒ ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) | ||
Theorem | 2itscplem3 47178 | Lemma D for 2itscp 47179. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | ||
Theorem | 2itscp 47179 | 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 47180 | Lemma 1 for itscnhlinecirc02p 47183. (Contributed by AV, 6-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → 𝐵 ≠ 𝑌) ⇒ ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem2 47181 | Lemma 2 for itscnhlinecirc02p 47183. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem3 47182 | Lemma 3 for itscnhlinecirc02p 47183. (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 47183* | 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 47184* | Lemma for inlinecirc02p 47185. (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 47185 | 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 47186* | 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 47187 | Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 562. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | logic1 47188 | Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic1a 47189 | Variant of logic1 47188. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic2 47190 | Variant of logic1 47188. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | pm5.32dav 47191 | Distribution of implication over biconditional (deduction form). Variant of pm5.32da 579. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) | ||
Theorem | pm5.32dra 47192 | Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | ||
Theorem | exp12bd 47193 | The import-export theorem (impexp 451) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜏 ∧ 𝜂) → 𝜁))) ⇒ ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) ↔ (𝜏 → (𝜂 → 𝜁)))) | ||
Theorem | mpbiran3d 47194 | 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 47195 | 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 47196* | An example of how ax-5 1913 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5430 in the ZF set theory. axc16nf 2254 and euae 2655 demonstrate that the violation of dtru 5430 leads to a model with only one object assuming its existence (ax-6 1971). The conclusion is also provable in the empty model ( see emptyal 1911). See also nf5 2278 and nf5i 2142 for the relation between unconditional ax-5 1913 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 & ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦) ⇒ ⊢ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | ralbidb 47197* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 47198 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | ralbidc 47198* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 47197. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | r19.41dv 47199* | A complex deduction form of r19.41v 3188. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) | ||
Theorem | rspceb2dv 47200* | Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 → 𝜒)) & ⊢ ((𝜑 ∧ 𝜒) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |