P. 488 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48701-48800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ackval1012 48701	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 48702	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 48703	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 48704	The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘0) = ;13
Theorem	ackval41a 48705	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3)
Theorem	ackval41 48706	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ;;;;65533
Theorem	ackval42 48707	The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3)
Theorem	ackval42a 48708	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 48709	The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘5)‘0) = ;;;;65533
21.48.22  Elementary geometry (extension)
21.48.22.1  Auxiliary theorems
Theorem	fv1prop 48710	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 48711	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 48712	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 48713*	Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    &   ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹)))
Theorem	affinecomb2 48714*	Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))))
Theorem	affineid 48715	Identity of an affine combination. (Contributed by AV, 2-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴)
Theorem	1subrec1sub 48716	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 48717	The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
Theorem	resum2sqgt0 48718	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 48719	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 48720	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 48721	Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶))
21.48.22.2  Real euclidean space of dimension 2
Theorem	rrx2pxel 48722	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 48723	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 48724	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 48725	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 48726	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 48727	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 48728	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 48729*	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 48730	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 48731*	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 48732*	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 48733*	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 48734*	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 48735*	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 48736	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 48737	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.48.22.3  Spheres and lines in real Euclidean spaces
Syntax	cline 48738	Declare the syntax for lines in generalized real Euclidean spaces.
class LineM
Syntax	csph 48739	Declare the syntax for spheres in generalized real Euclidean spaces.
class Sphere
Definition	df-line 48740*	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 48741*	Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24224, 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 48742*	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 48743*	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 48744*	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 48745*	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 48746*	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 48747*	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 48746. (Contributed by AV, 13-Feb-2023.)
⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝐿 = (LineM‘𝐸)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))})
Theorem	eenglngeehlnmlem1 48748*	Lemma 1 for eenglngeehlnm 48750. (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 48749*	Lemma 2 for eenglngeehlnm 48750. (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 48750	The line definition in the Tarski structure for the Euclidean geometry (see elntg 28955) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 48744). (Contributed by AV, 16-Feb-2023.)
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁)))
Theorem	rrx2line 48751*	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 48752*	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 48753*	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 48754*	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 48755*	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 48756	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 48757*	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 48758*	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 48759*	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 48760*	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 48761*	The sphere around the origin 0 (see rrx0 25317) 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 48762*	Lemma for line2y 48766. 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 48763*	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 48764*	Lemma for line2x 48765. 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 48765*	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 48766*	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 48767	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 48768	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 48769	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 48770	Lemma for itsclc0 48782. 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 48771	Lemma for itsclc0 48782. 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 48772	Lemma for itsclc0 48782. 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 48773	Lemma 1 for itsclc0yqsol 48775. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷))
Theorem	itsclc0yqsollem2 48774	Lemma 2 for itsclc0yqsol 48775. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷)))
Theorem	itsclc0yqsol 48775	Lemma for itsclc0 48782. 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 48776	Lemma for itsclc0 48782. 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 48777	Lemma for itsclc0 48782. 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 48778	Lemma for itsclc0 48782. 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 48779	Lemma for itsclc0 48782. 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 48780	Lemma for itsclc0 48782. 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 48781	Lemma for itsclc0 48782. 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 48782*	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 48783*	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 48784	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 48785	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 48786	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 48787*	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 48788*	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 48789	Lemma 1 for 2itscp 48792. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    ⇒   ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2))
Theorem	2itscplem2 48790	Lemma 2 for 2itscp 48792. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    ⇒   ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))
Theorem	2itscplem3 48791	Lemma D for 2itscp 48792. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2))    &   ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))))
Theorem	2itscp 48792	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 48793	Lemma 1 for itscnhlinecirc02p 48796. (Contributed by AV, 6-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))    &   ⊢ (𝜑 → 𝐵 ≠ 𝑌)    ⇒   ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem2 48794	Lemma 2 for itscnhlinecirc02p 48796. (Contributed by AV, 10-Mar-2023.)
⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌))    ⇒   ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem3 48795	Lemma 3 for itscnhlinecirc02p 48796. (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 48796*	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 48797*	Lemma for inlinecirc02p 48798. (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 48798	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 48799*	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 𝑆𝑅) ∩ (𝑋𝐿𝑌))))
21.49  Mathbox for Zhi Wang
21.49.1  Propositional calculus
Theorem	pm4.71da 48800	Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 561. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))