P. 474 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47301-47400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prelrrx2 47301	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 47302	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 47303	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 47304	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 47305	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 47306*	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 47307	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 47308*	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 47309*	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 47310*	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 47311*	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 47312*	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 47313	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 47314	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.45.23.3  Spheres and lines in real Euclidean spaces
Syntax	cline 47315	Declare the syntax for lines in generalized real Euclidean spaces.
class LineM
Syntax	csph 47316	Declare the syntax for spheres in generalized real Euclidean spaces.
class Sphere
Definition	df-line 47317*	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 47318*	Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 23804, 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 47319*	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 47320*	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 47321*	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 47322*	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 47323*	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 47324*	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 47323. (Contributed by AV, 13-Feb-2023.)
⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝐿 = (LineM‘𝐸)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))})
Theorem	eenglngeehlnmlem1 47325*	Lemma 1 for eenglngeehlnm 47327. (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 47326*	Lemma 2 for eenglngeehlnm 47327. (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 47327	The line definition in the Tarski structure for the Euclidean geometry (see elntg 28222) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 47321). (Contributed by AV, 16-Feb-2023.)
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁)))
Theorem	rrx2line 47328*	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 47329*	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 47330*	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 47331*	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 47332*	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 47333	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 47334*	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 47335*	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 47336*	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 47337*	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 47338*	The sphere around the origin 0 (see rrx0 24896) 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 47339*	Lemma for line2y 47343. 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 47340*	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 47341*	Lemma for line2x 47342. 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 47342*	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 47343*	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 47344	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 47345	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 47346	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 47347	Lemma for itsclc0 47359. 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 47348	Lemma for itsclc0 47359. 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 47349	Lemma for itsclc0 47359. 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 47350	Lemma 1 for itsclc0yqsol 47352. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ 𝑅 ∈ ℂ) → ((𝑇↑2) − (4 · (𝑄 · 𝑈))) = ((4 · (𝐴↑2)) · 𝐷))
Theorem	itsclc0yqsollem2 47351	Lemma 2 for itsclc0yqsol 47352. (Contributed by AV, 6-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))    &   ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷) → (√‘((𝑇↑2) − (4 · (𝑄 · 𝑈)))) = ((2 · (abs‘𝐴)) · (√‘𝐷)))
Theorem	itsclc0yqsol 47352	Lemma for itsclc0 47359. 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 47353	Lemma for itsclc0 47359. 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 47354	Lemma for itsclc0 47359. 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 47355	Lemma for itsclc0 47359. 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 47356	Lemma for itsclc0 47359. 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 47357	Lemma for itsclc0 47359. 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 47358	Lemma for itsclc0 47359. 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 47359*	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 47360*	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 47361	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 47362	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 47363	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 47364*	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 47365*	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 47366	Lemma 1 for 2itscp 47369. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    ⇒   ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2))
Theorem	2itscplem2 47367	Lemma 2 for 2itscp 47369. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    ⇒   ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))
Theorem	2itscplem3 47368	Lemma D for 2itscp 47369. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2))    &   ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))))
Theorem	2itscp 47369	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 47370	Lemma 1 for itscnhlinecirc02p 47373. (Contributed by AV, 6-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))    &   ⊢ (𝜑 → 𝐵 ≠ 𝑌)    ⇒   ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem2 47371	Lemma 2 for itscnhlinecirc02p 47373. (Contributed by AV, 10-Mar-2023.)
⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌))    ⇒   ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem3 47372	Lemma 3 for itscnhlinecirc02p 47373. (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 47373*	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 47374*	Lemma for inlinecirc02p 47375. (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 47375	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 47376*	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.46  Mathbox for Zhi Wang
21.46.1  Propositional calculus
Theorem	pm4.71da 47377	Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 563. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	logic1 47378	Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	logic1a 47379	Variant of logic1 47378. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	logic2 47380	Variant of logic1 47378. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	pm5.32dav 47381	Distribution of implication over biconditional (deduction form). Variant of pm5.32da 580. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))
Theorem	pm5.32dra 47382	Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
Theorem	exp12bd 47383	The import-export theorem (impexp 452) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜏 ∧ 𝜂) → 𝜁)))    ⇒   ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) ↔ (𝜏 → (𝜂 → 𝜁))))
Theorem	mpbiran3d 47384	Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	mpbiran4d 47385	Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
21.46.2  Predicate calculus with equality
21.46.2.1  Axiom scheme ax-5 (Distinctness)
Theorem	dtrucor3 47386*	An example of how ax-5 1914 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5435 in the ZF set theory. axc16nf 2255 and euae 2656 demonstrate that the violation of dtru 5435 leads to a model with only one object assuming its existence (ax-6 1972). The conclusion is also provable in the empty model ( see emptyal 1912). See also nf5 2279 and nf5i 2143 for the relation between unconditional ax-5 1914 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦    &   ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)    ⇒   ⊢ ∀𝑥 𝑥 = 𝑦
21.46.3  ZF Set Theory - start with the Axiom of Extensionality
21.46.3.1  Restricted quantification
Theorem	ralbidb 47387*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 47388 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	ralbidc 47388*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 47387. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	r19.41dv 47389*	A complex deduction form of r19.41v 3189. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))
Theorem	rspceb2dv 47390*	Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒))
Theorem	rmotru 47391	Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑥 ∈ 𝐴 ⊤)
Theorem	reutru 47392	Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
Theorem	reutruALT 47393	Alternate proof for reutru 47392. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
21.46.3.2  The empty set
Theorem	ssdisjd 47394	Subset preserves disjointness. Deduction form of ssdisj 4458. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)
Theorem	ssdisjdr 47395	Subset preserves disjointness. Deduction form of ssdisj 4458. Alternatively this could be proved with ineqcom 4201 in tandem with ssdisjd 47394. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = ∅)
Theorem	disjdifb 47396	Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	predisj 47397	Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝐴))    &   ⊢ (𝜑 → 𝑇 ⊆ (◡𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)
21.46.3.3  Unordered and ordered pairs
Theorem	vsn 47398	The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ {V} = ∅
Theorem	mosn 47399*	"At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mo0 47400*	"At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = ∅ → ∃*𝑥 𝑥 ∈ 𝐴)