![]() |
Metamath
Proof Explorer Theorem List (p. 476 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30606) |
![]() (30607-32129) |
![]() (32130-48006) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itcoval 47501* | The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024.) |
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) | ||
Theorem | itcoval0 47502 | A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.) |
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) | ||
Theorem | itcoval1 47503 | A function iterated once. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) | ||
Theorem | itcoval2 47504 | A function iterated twice. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹)) | ||
Theorem | itcoval3 47505 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) | ||
Theorem | itcoval0mpt 47506* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛)) | ||
Theorem | itcovalsuc 47507* | 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 47508 | 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 47509 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴) | ||
Theorem | itcovalpclem1 47510* | Lemma 1 for itcovalpc 47512: induction basis. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0)))) | ||
Theorem | itcovalpclem2 47511* | Lemma 2 for itcovalpc 47512: induction step. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1)))))) | ||
Theorem | itcovalpc 47512* | 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 47513 | Lemma 1 for itcovalt2lem2 47516. (Contributed by AV, 6-May-2024.) |
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0) | ||
Theorem | itcovalt2lem2lem2 47514 | Lemma 2 for itcovalt2lem2 47516. (Contributed by AV, 7-May-2024.) |
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) | ||
Theorem | itcovalt2lem1 47515* | Lemma 1 for itcovalt2 47517: induction basis. (Contributed by AV, 5-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) | ||
Theorem | itcovalt2lem2 47516* | Lemma 2 for itcovalt2 47517: induction step. (Contributed by AV, 7-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) | ||
Theorem | itcovalt2 47517* | 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 47518* | 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 47519 | 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 47520 | The Ackermann function at 0. (Contributed by AV, 2-May-2024.) |
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)) | ||
Theorem | ackval1 47521 | The Ackermann function at 1. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2)) | ||
Theorem | ackval2 47522 | The Ackermann function at 2. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3)) | ||
Theorem | ackval3 47523 | The Ackermann function at 3. (Contributed by AV, 7-May-2024.) |
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) | ||
Theorem | ackendofnn0 47524 | 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 47525 | 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 47526 | 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 47527 | 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 47528 | 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 47529 | 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 47530 | 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 47531 | 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 47532 | 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 47533 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘0) = ;13 | ||
Theorem | ackval41a 47534 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3) | ||
Theorem | ackval41 47535 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ;;;;65533 | ||
Theorem | ackval42 47536 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3) | ||
Theorem | ackval42a 47537 | 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 47538 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘5)‘0) = ;;;;65533 | ||
Theorem | fv1prop 47539 | 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 47540 | 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 47541 | 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 47542* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) & ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹))) | ||
Theorem | affinecomb2 47543* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | ||
Theorem | affineid 47544 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴) | ||
Theorem | 1subrec1sub 47545 | 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 47546 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ) | ||
Theorem | resum2sqgt0 47547 | 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 47548 | 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 47549 | 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 47550 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶)) | ||
Theorem | rrx2pxel 47551 | 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 47552 | 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 47553 | 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 47554 | 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 47555 | 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 47556 | 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 47557 | 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 47558* | 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 47559 | 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 47560* | 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 47561* | 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 47562* | 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 47563* | 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 47564* | 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 47565 | 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 47566 | An upper bound of the Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 9-May-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑m {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 0 = ({1, 2} × {0}) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝐹𝐷 0 ) < 𝑅 ↔ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) < (𝑅↑2))) | ||
Syntax | cline 47567 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 47568 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 47569* | 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 47570* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24143, 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 47571* | 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 47572* | 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 47573* | 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 47574* | 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 47575* | 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 47576* | 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 47575. (Contributed by AV, 13-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))}) | ||
Theorem | eenglngeehlnmlem1 47577* | Lemma 1 for eenglngeehlnm 47579. (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 47578* | Lemma 2 for eenglngeehlnm 47579. (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 47579 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 28677) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 47573). (Contributed by AV, 16-Feb-2023.) |
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁))) | ||
Theorem | rrx2line 47580* | 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 47581* | 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 47582* | 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 47583* | 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 47584* | 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 47585 | 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 47586* | 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 47587* | 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 47588* | 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 47589* | 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 47590* | The sphere around the origin 0 (see rrx0 25246) 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 47591* | Lemma for line2y 47595. 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 47592* | 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 47593* | Lemma for line2x 47594. 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 47594* | 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 47595* | 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 47596 | 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 47597 | 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 47598 | 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 47599 | Lemma for itsclc0 47611. 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 47600 | Lemma for itsclc0 47611. 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |