![]() |
Metamath
Proof Explorer Theorem List (p. 486 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2arymaptf 48501* | The mapping of binary (endo)functions is a function into the set of binary operations. (Contributed by AV, 21-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptf1 48502* | The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–1-1→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptfo 48503* | The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptf1o 48504* | The mapping of binary (endo)functions is a one-to-one function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–1-1-onto→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2aryenef 48505 | The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.) |
⊢ (2-aryF 𝑋) ≈ (𝑋 ↑m (𝑋 × 𝑋)) | ||
According to Wikipedia ("Ackermann function", 8-May-2024, https://en.wikipedia.org/wiki/Ackermann_function): "In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. ... One common version is the two-argument Ackermann-Péter function developed by Rózsa Péter and Raphael Robinson. Its value grows very rapidly; for example, A(4,2) results in 2^65536-3 [see ackval42 48545)], an integer of 19,729 decimal digits." In the following, the Ackermann function is defined as iterated 1-ary function (also mentioned in Wikipedia), see df-ack 48509, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 48508. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 48514). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 48509: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 48509 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 48535: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 48536: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 48537: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 48538: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 48539: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 48540: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 48541: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29. | ||
Syntax | citco 48506 | Extend the definition of a class to include iterated functions. |
class IterComp | ||
Syntax | cack 48507 | Extend the definition of a class to include the Ackermann function operator. |
class Ack | ||
Definition | df-itco 48508* | Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
⊢ IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))) | ||
Definition | df-ack 48509* | Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
⊢ Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))) | ||
Theorem | itcoval 48510* | 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 48511 | A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.) |
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) | ||
Theorem | itcoval1 48512 | A function iterated once. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) | ||
Theorem | itcoval2 48513 | A function iterated twice. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹)) | ||
Theorem | itcoval3 48514 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) | ||
Theorem | itcoval0mpt 48515* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛)) | ||
Theorem | itcovalsuc 48516* | 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 48517 | 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 48518 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴) | ||
Theorem | itcovalpclem1 48519* | Lemma 1 for itcovalpc 48521: induction basis. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0)))) | ||
Theorem | itcovalpclem2 48520* | Lemma 2 for itcovalpc 48521: induction step. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1)))))) | ||
Theorem | itcovalpc 48521* | 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 48522 | Lemma 1 for itcovalt2lem2 48525. (Contributed by AV, 6-May-2024.) |
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0) | ||
Theorem | itcovalt2lem2lem2 48523 | Lemma 2 for itcovalt2lem2 48525. (Contributed by AV, 7-May-2024.) |
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) | ||
Theorem | itcovalt2lem1 48524* | Lemma 1 for itcovalt2 48526: induction basis. (Contributed by AV, 5-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) | ||
Theorem | itcovalt2lem2 48525* | Lemma 2 for itcovalt2 48526: induction step. (Contributed by AV, 7-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) | ||
Theorem | itcovalt2 48526* | 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 48527* | 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 48528 | 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 48529 | The Ackermann function at 0. (Contributed by AV, 2-May-2024.) |
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)) | ||
Theorem | ackval1 48530 | The Ackermann function at 1. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2)) | ||
Theorem | ackval2 48531 | The Ackermann function at 2. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3)) | ||
Theorem | ackval3 48532 | The Ackermann function at 3. (Contributed by AV, 7-May-2024.) |
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) | ||
Theorem | ackendofnn0 48533 | 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 48534 | 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 48535 | 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 48536 | 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 48537 | 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 48538 | 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 48539 | 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 48540 | 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 48541 | 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 48542 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘0) = ;13 | ||
Theorem | ackval41a 48543 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3) | ||
Theorem | ackval41 48544 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ;;;;65533 | ||
Theorem | ackval42 48545 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3) | ||
Theorem | ackval42a 48546 | 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 48547 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘5)‘0) = ;;;;65533 | ||
Theorem | fv1prop 48548 | 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 48549 | 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 48550 | 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 48551* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) & ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹))) | ||
Theorem | affinecomb2 48552* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | ||
Theorem | affineid 48553 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴) | ||
Theorem | 1subrec1sub 48554 | 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 48555 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ) | ||
Theorem | resum2sqgt0 48556 | 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 48557 | 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 48558 | 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 48559 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶)) | ||
Theorem | rrx2pxel 48560 | 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 48561 | 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 48562 | 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 48563 | 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 48564 | 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 48565 | 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 48566 | 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 48567* | 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 48568 | 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 48569* | 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 48570* | 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 48571* | 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 48572* | 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 48573* | 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 48574 | 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 48575 | 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 48576 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 48577 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 48578* | 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 48579* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24341, 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 48580* | 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 48581* | 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 48582* | 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 48583* | 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 48584* | 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 48585* | 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 48584. (Contributed by AV, 13-Feb-2023.) |
⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝐿 = (LineM‘𝐸) ⇒ ⊢ ((𝐼 ∈ Fin ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑡) · (𝑋‘𝑖)) + (𝑡 · (𝑌‘𝑖)))}) | ||
Theorem | eenglngeehlnmlem1 48586* | Lemma 1 for eenglngeehlnm 48588. (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 48587* | Lemma 2 for eenglngeehlnm 48588. (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 48588 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 29013) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 48582). (Contributed by AV, 16-Feb-2023.) |
⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (LineM‘(𝔼hil‘𝑁))) | ||
Theorem | rrx2line 48589* | 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 48590* | 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 48591* | 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 48592* | 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 48593* | 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 48594 | 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 48595* | 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 48596* | 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 48597* | 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 48598* | 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 48599* | The sphere around the origin 0 (see rrx0 25444) 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 48600* | Lemma for line2y 48604. 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))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |