![]() |
Metamath
Proof Explorer Theorem List (p. 452 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ackvalsuc0val 45101 | The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1)) | ||
Theorem | ackvalsucsucval 45102 | The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁))) | ||
Theorem | ackval0012 45103 | The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024.) |
⊢ 〈((Ack‘0)‘0), ((Ack‘0)‘1), ((Ack‘0)‘2)〉 = 〈1, 2, 3〉 | ||
Theorem | ackval1012 45104 | The Ackermann function at (1,0), (1,1), (1,2). (Contributed by AV, 4-May-2024.) |
⊢ 〈((Ack‘1)‘0), ((Ack‘1)‘1), ((Ack‘1)‘2)〉 = 〈2, 3, 4〉 | ||
Theorem | ackval2012 45105 | The Ackermann function at (2,0), (2,1), (2,2). (Contributed by AV, 4-May-2024.) |
⊢ 〈((Ack‘2)‘0), ((Ack‘2)‘1), ((Ack‘2)‘2)〉 = 〈3, 5, 7〉 | ||
Theorem | ackval3012 45106 | The Ackermann function at (3,0), (3,1), (3,2). (Contributed by AV, 7-May-2024.) |
⊢ 〈((Ack‘3)‘0), ((Ack‘3)‘1), ((Ack‘3)‘2)〉 = 〈5, ;13, ;29〉 | ||
Theorem | ackval40 45107 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘0) = ;13 | ||
Theorem | ackval41a 45108 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3) | ||
Theorem | ackval41 45109 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ;;;;65533 | ||
Theorem | ackval42 45110 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3) | ||
Theorem | ackval42a 45111 | The Ackermann function at (4,2), expressed with powers of 2. (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑(2↑(2↑(2↑2)))) − 3) | ||
Theorem | ackval50 45112 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘5)‘0) = ;;;;65533 | ||
Theorem | fv1prop 45113 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ({〈1, 𝐴〉, 〈2, 𝐵〉}‘1) = 𝐴) | ||
Theorem | fv2prop 45114 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
⊢ (𝐵 ∈ 𝑉 → ({〈1, 𝐴〉, 〈2, 𝐵〉}‘2) = 𝐵) | ||
Theorem | submuladdmuld 45115 | Transformation of a sum of a product of a difference and a product with the subtrahend of the difference. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵) · 𝐶) + (𝐵 · 𝐷)) = ((𝐴 · 𝐶) + (𝐵 · (𝐷 − 𝐶)))) | ||
Theorem | affinecomb1 45116* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) & ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹))) | ||
Theorem | affinecomb2 45117* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | ||
Theorem | affineid 45118 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴) | ||
Theorem | 1subrec1sub 45119 | 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 45120 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ) | ||
Theorem | resum2sqgt0 45121 | 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 45122 | 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 45123 | 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 45124 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶)) | ||
Theorem | rrx2pxel 45125 | 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 45126 | 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 45127 | 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 45128 | 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 45129 | 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 45130 | 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 45131 | 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 45132* | 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 45133 | 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 45134* | 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 45135* | 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 45136* | 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 45137* | 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 45138* | 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 45139 | 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 45140 | 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 45141 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 45142 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 45143* | 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 45144* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 22923, 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 45145* | 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 45146* | 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 45147* | 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 45148* | 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 45149* | 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 45150* | 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 45149. (Contributed by AV, 13-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))}) | ||
Theorem | eenglngeehlnmlem1 45151* | Lemma 1 for eenglngeehlnm 45153. (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 45152* | Lemma 2 for eenglngeehlnm 45153. (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 45153 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 26778) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 45147). (Contributed by AV, 16-Feb-2023.) |
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁))) | ||
Theorem | rrx2line 45154* | 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 45155* | 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 45156* | 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 45157* | 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 45158* | 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 45159 | 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 45160* | 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 45161* | 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 45162* | 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 45163* | 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 45164* | The sphere around the origin 0 (see rrx0 24001) 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 45165* | Lemma for line2y 45169. 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 45166* | 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 45167* | Lemma for line2x 45168. 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 45168* | 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 45169* | 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 45170 | 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 45171 | 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 45172 | 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 45173 | Lemma for itsclc0 45185. 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 45174 | Lemma for itsclc0 45185. 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 45175 | Lemma for itsclc0 45185. 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 45176 | Lemma 1 for itsclc0yqsol 45178. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷)) | ||
Theorem | itsclc0yqsollem2 45177 | Lemma 2 for itsclc0yqsol 45178. (Contributed by AV, 6-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷))) | ||
Theorem | itsclc0yqsol 45178 | Lemma for itsclc0 45185. 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 45179 | Lemma for itsclc0 45185. 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 45180 | Lemma for itsclc0 45185. 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 45181 | Lemma for itsclc0 45185. 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 45182 | Lemma for itsclc0 45185. 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 45183 | Lemma for itsclc0 45185. 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 45184 | Lemma for itsclc0 45185. 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 45185* | 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 45186* | 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 45187 | 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 45188 | 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 45189 | 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 45190* | 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 45191* | 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 45192 | Lemma 1 for 2itscp 45195. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) ⇒ ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2)) | ||
Theorem | 2itscplem2 45193 | Lemma 2 for 2itscp 45195. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) ⇒ ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) | ||
Theorem | 2itscplem3 45194 | Lemma D for 2itscp 45195. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | ||
Theorem | 2itscp 45195 | 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 45196 | Lemma 1 for itscnhlinecirc02p 45199. (Contributed by AV, 6-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → 𝐵 ≠ 𝑌) ⇒ ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem2 45197 | Lemma 2 for itscnhlinecirc02p 45199. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem3 45198 | Lemma 3 for itscnhlinecirc02p 45199. (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 45199* | 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 45200* | Lemma for inlinecirc02p 45201. (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 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |