P. 497 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49601-49700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ackval0val 49601	The Ackermann function at 0 (for the first argument). This is the first equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.)
⊢ (𝑀 ∈ ℕ0 → ((Ack‘0)‘𝑀) = (𝑀 + 1))
Theorem	ackvalsuc0val 49602	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 49603	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 49604	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 49605	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 49606	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 49607	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 49608	The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘0) = ;13
Theorem	ackval41a 49609	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3)
Theorem	ackval41 49610	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ;;;;65533
Theorem	ackval42 49611	The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3)
Theorem	ackval42a 49612	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 49613	The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘5)‘0) = ;;;;65533
21.50.23  Elementary geometry (extension)
21.50.23.1  Auxiliary theorems
Theorem	fv1prop 49614	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 49615	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 49616	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 49617*	Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    &   ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹)))
Theorem	affinecomb2 49618*	Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))))
Theorem	affineid 49619	Identity of an affine combination. (Contributed by AV, 2-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴)
Theorem	1subrec1sub 49620	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 49621	The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
Theorem	resum2sqgt0 49622	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 49623	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 49624	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 49625	Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶))
21.50.23.2  Real euclidean space of dimension 2
Theorem	rrx2pxel 49626	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 49627	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 49628	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 49629	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 49630	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 49631	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 49632	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 49633*	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 49634	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 49635*	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 49636*	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 49637*	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 49638*	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 49639*	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 49640	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 49641	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)))
21.50.23.3  Spheres and lines in real Euclidean spaces
Syntax	cline 49642	Declare the syntax for lines in generalized real Euclidean spaces.
class LineM
Syntax	csph 49643	Declare the syntax for spheres in generalized real Euclidean spaces.
class Sphere
Definition	df-line 49644*	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 49645*	Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24541, 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 49646*	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 49647*	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 49648*	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 49649*	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 49650*	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 49651*	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 49650. (Contributed by AV, 13-Feb-2023.)
⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝐿 = (LineM‘𝐸)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))})
Theorem	eenglngeehlnmlem1 49652*	Lemma 1 for eenglngeehlnm 49654. (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 49653*	Lemma 2 for eenglngeehlnm 49654. (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 49654	The line definition in the Tarski structure for the Euclidean geometry (see elntg 29425) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 49648). (Contributed by AV, 16-Feb-2023.)
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁)))
Theorem	rrx2line 49655*	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 49656*	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 49657*	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 49658*	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 49659*	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 49660	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 49661*	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 49662*	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 49663*	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 49664*	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 49665*	The sphere around the origin 0 (see rrx0 25624) 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 49666*	Lemma for line2y 49670. This proof is based on counterexamples for the following cases: 1. 𝐶 ≠ 0: p = (0,0) (LHS of biconditional is false, RHS is true); 2. 𝐶 = 0 ∧ 𝐵 ≠ 0: p = (1,-A/B) (LHS of biconditional is true, RHS is false); 3. 𝐴 = 𝐵 = 𝐶 = 0: p = (1,1) (LHS of biconditional is true, RHS is false). (Contributed by AV, 4-Feb-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
Theorem	line2 49667*	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 49668*	Lemma for line2x 49669. 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 49669*	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 49670*	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 49671	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 49672	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 49673	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 49674	Lemma for itsclc0 49686. 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 49675	Lemma for itsclc0 49686. 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 49676	Lemma for itsclc0 49686. 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 49677	Lemma 1 for itsclc0yqsol 49679. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷))
Theorem	itsclc0yqsollem2 49678	Lemma 2 for itsclc0yqsol 49679. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷)))
Theorem	itsclc0yqsol 49679	Lemma for itsclc0 49686. 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 49680	Lemma for itsclc0 49686. 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 49681	Lemma for itsclc0 49686. 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 49682	Lemma for itsclc0 49686. 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 49683	Lemma for itsclc0 49686. 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 49684	Lemma for itsclc0 49686. 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 49685	Lemma for itsclc0 49686. 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 49686*	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 49687*	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 49688	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 49689	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 49690	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 49691*	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 49692*	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 49693	Lemma 1 for 2itscp 49696. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    ⇒   ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2))
Theorem	2itscplem2 49694	Lemma 2 for 2itscp 49696. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    ⇒   ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))
Theorem	2itscplem3 49695	Lemma D for 2itscp 49696. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2))    &   ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))))
Theorem	2itscp 49696	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 49697	Lemma 1 for itscnhlinecirc02p 49700. (Contributed by AV, 6-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))    &   ⊢ (𝜑 → 𝐵 ≠ 𝑌)    ⇒   ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem2 49698	Lemma 2 for itscnhlinecirc02p 49700. (Contributed by AV, 10-Mar-2023.)
⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌))    ⇒   ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem3 49699	Lemma 3 for itscnhlinecirc02p 49700. (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 49700*	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 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌))))