P. 496 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49501-49600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itcoval0 49501	A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.)
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹))
Theorem	itcoval1 49502	A function iterated once. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹)
Theorem	itcoval2 49503	A function iterated twice. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹))
Theorem	itcoval3 49504	A function iterated three times. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹)))
Theorem	itcoval0mpt 49505*	A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛))
Theorem	itcovalsuc 49506*	The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹))
Theorem	itcovalsucov 49507	The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐹 ∘ 𝐺))
Theorem	itcovalendof 49508	The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴)
Theorem	itcovalpclem1 49509*	Lemma 1 for itcovalpc 49511: induction basis. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0))))
Theorem	itcovalpclem2 49510*	Lemma 2 for itcovalpc 49511: induction step. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))))
Theorem	itcovalpc 49511*	The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ ((𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝐼))))
Theorem	itcovalt2lem2lem1 49512	Lemma 1 for itcovalt2lem2 49515. (Contributed by AV, 6-May-2024.)
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0)
Theorem	itcovalt2lem2lem2 49513	Lemma 2 for itcovalt2lem2 49515. (Contributed by AV, 7-May-2024.)
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶))
Theorem	itcovalt2lem1 49514*	Lemma 1 for itcovalt2 49516: induction basis. (Contributed by AV, 5-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶)))
Theorem	itcovalt2lem2 49515*	Lemma 2 for itcovalt2 49516: induction step. (Contributed by AV, 7-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))
Theorem	itcovalt2 49516*	The value of the function that returns the n-th iterate of the "times 2 plus a constant" function with regard to composition. (Contributed by AV, 7-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ ((𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶)))
Theorem	ackvalsuc1mpt 49517*	The Ackermann function at a successor of the first argument as a mapping of the second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.)
⊢ (𝑀 ∈ ℕ0 → (Ack‘(𝑀 + 1)) = (𝑛 ∈ ℕ0 ↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1)))
Theorem	ackvalsuc1 49518	The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1))
Theorem	ackval0 49519	The Ackermann function at 0. (Contributed by AV, 2-May-2024.)
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
Theorem	ackval1 49520	The Ackermann function at 1. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2))
Theorem	ackval2 49521	The Ackermann function at 2. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3))
Theorem	ackval3 49522	The Ackermann function at 3. (Contributed by AV, 7-May-2024.)
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3))
Theorem	ackendofnn0 49523	The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024.)
⊢ (𝑀 ∈ ℕ0 → (Ack‘𝑀):ℕ0⟶ℕ0)
Theorem	ackfnnn0 49524	The Ackermann function at any nonnegative integer is a function on the nonnegative integers. (Contributed by AV, 4-May-2024.) (Proof shortened by AV, 8-May-2024.)
⊢ (𝑀 ∈ ℕ0 → (Ack‘𝑀) Fn ℕ0)
Theorem	ackval0val 49525	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 49526	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 49527	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 49528	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 49529	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 49530	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 49531	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 49532	The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘0) = ;13
Theorem	ackval41a 49533	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3)
Theorem	ackval41 49534	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ;;;;65533
Theorem	ackval42 49535	The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3)
Theorem	ackval42a 49536	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 49537	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 49538	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 49539	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 49540	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 49541*	Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    &   ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹)))
Theorem	affinecomb2 49542*	Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))))
Theorem	affineid 49543	Identity of an affine combination. (Contributed by AV, 2-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴)
Theorem	1subrec1sub 49544	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 49545	The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
Theorem	resum2sqgt0 49546	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 49547	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 49548	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 49549	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 49550	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 49551	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 49552	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 49553	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 49554	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 49555	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 49556	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 49557*	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 49558	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 49559*	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 49560*	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 49561*	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 49562*	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 49563*	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 49564	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 49565	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 49566	Declare the syntax for lines in generalized real Euclidean spaces.
class LineM
Syntax	csph 49567	Declare the syntax for spheres in generalized real Euclidean spaces.
class Sphere
Definition	df-line 49568*	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 49569*	Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24526, 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 49570*	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 49571*	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 49572*	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 49573*	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 49574*	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 49575*	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 49574. (Contributed by AV, 13-Feb-2023.)
⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝐿 = (LineM‘𝐸)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))})
Theorem	eenglngeehlnmlem1 49576*	Lemma 1 for eenglngeehlnm 49578. (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 49577*	Lemma 2 for eenglngeehlnm 49578. (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 49578	The line definition in the Tarski structure for the Euclidean geometry (see elntg 29391) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 49572). (Contributed by AV, 16-Feb-2023.)
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁)))
Theorem	rrx2line 49579*	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 49580*	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 49581*	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 49582*	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 49583*	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 49584	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 49585*	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 49586*	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 49587*	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 49588*	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 49589*	The sphere around the origin 0 (see rrx0 25609) 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 49590*	Lemma for line2y 49594. 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 49591*	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 49592*	Lemma for line2x 49593. 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 49593*	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 49594*	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 49595	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 49596	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 49597	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 49598	Lemma for itsclc0 49610. 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 49599	Lemma for itsclc0 49610. 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 49600	Lemma for itsclc0 49610. 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))