Home | Metamath
Proof Explorer Theorem List (p. 466 of 470) | < 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: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itcoval3 46501 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
β’ ((Rel πΉ β§ πΉ β π) β ((IterCompβπΉ)β3) = (πΉ β (πΉ β πΉ))) | ||
Theorem | itcoval0mpt 46502* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β π΄ β¦ π΅) β β’ ((π΄ β π β§ βπ β π΄ π΅ β π) β ((IterCompβπΉ)β0) = (π β π΄ β¦ π)) | ||
Theorem | itcovalsuc 46503* | 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 46504 | 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 46505 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΄) & β’ (π β π β β0) β β’ (π β ((IterCompβπΉ)βπ):π΄βΆπ΄) | ||
Theorem | itcovalpclem1 46506* | Lemma 1 for itcovalpc 46508: induction basis. (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β β0 β¦ (π + πΆ)) β β’ (πΆ β β0 β ((IterCompβπΉ)β0) = (π β β0 β¦ (π + (πΆ Β· 0)))) | ||
Theorem | itcovalpclem2 46507* | Lemma 2 for itcovalpc 46508: induction step. (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β β0 β¦ (π + πΆ)) β β’ ((π¦ β β0 β§ πΆ β β0) β (((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦))) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1)))))) | ||
Theorem | itcovalpc 46508* | 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 46509 | Lemma 1 for itcovalt2lem2 46512. (Contributed by AV, 6-May-2024.) |
β’ (((π β β β§ πΆ β β0) β§ π β β0) β (((π + πΆ) Β· π) β πΆ) β β0) | ||
Theorem | itcovalt2lem2lem2 46510 | Lemma 2 for itcovalt2lem2 46512. (Contributed by AV, 7-May-2024.) |
β’ (((π β β0 β§ πΆ β β0) β§ π β β0) β ((2 Β· (((π + πΆ) Β· (2βπ)) β πΆ)) + πΆ) = (((π + πΆ) Β· (2β(π + 1))) β πΆ)) | ||
Theorem | itcovalt2lem1 46511* | Lemma 1 for itcovalt2 46513: induction basis. (Contributed by AV, 5-May-2024.) |
β’ πΉ = (π β β0 β¦ ((2 Β· π) + πΆ)) β β’ (πΆ β β0 β ((IterCompβπΉ)β0) = (π β β0 β¦ (((π + πΆ) Β· (2β0)) β πΆ))) | ||
Theorem | itcovalt2lem2 46512* | Lemma 2 for itcovalt2 46513: induction step. (Contributed by AV, 7-May-2024.) |
β’ πΉ = (π β β0 β¦ ((2 Β· π) + πΆ)) β β’ ((π¦ β β0 β§ πΆ β β0) β (((IterCompβπΉ)βπ¦) = (π β β0 β¦ (((π + πΆ) Β· (2βπ¦)) β πΆ)) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (((π + πΆ) Β· (2β(π¦ + 1))) β πΆ)))) | ||
Theorem | itcovalt2 46513* | 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 46514* | 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 46515 | 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 46516 | The Ackermann function at 0. (Contributed by AV, 2-May-2024.) |
β’ (Ackβ0) = (π β β0 β¦ (π + 1)) | ||
Theorem | ackval1 46517 | The Ackermann function at 1. (Contributed by AV, 4-May-2024.) |
β’ (Ackβ1) = (π β β0 β¦ (π + 2)) | ||
Theorem | ackval2 46518 | The Ackermann function at 2. (Contributed by AV, 4-May-2024.) |
β’ (Ackβ2) = (π β β0 β¦ ((2 Β· π) + 3)) | ||
Theorem | ackval3 46519 | The Ackermann function at 3. (Contributed by AV, 7-May-2024.) |
β’ (Ackβ3) = (π β β0 β¦ ((2β(π + 3)) β 3)) | ||
Theorem | ackendofnn0 46520 | 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 46521 | 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 46522 | 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 46523 | 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 46524 | 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 46525 | 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 46526 | 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 46527 | 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 46528 | 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 46529 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β0) = ;13 | ||
Theorem | ackval41a 46530 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β1) = ((2β;16) β 3) | ||
Theorem | ackval41 46531 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β1) = ;;;;65533 | ||
Theorem | ackval42 46532 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β2) = ((2β;;;;65536) β 3) | ||
Theorem | ackval42a 46533 | 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 46534 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ5)β0) = ;;;;65533 | ||
Theorem | fv1prop 46535 | 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 46536 | 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 46537 | 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 46538* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β πΊ β β) & β’ π = ((πΊ β πΉ) / (πΆ β π΅)) β β’ (π β (βπ‘ β β (π΄ = (((1 β π‘) Β· π΅) + (π‘ Β· πΆ)) β§ πΈ = (((1 β π‘) Β· πΉ) + (π‘ Β· πΊ))) β πΈ = ((π Β· (π΄ β π΅)) + πΉ))) | ||
Theorem | affinecomb2 46539* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β πΊ β β) β β’ (π β (βπ‘ β β (π΄ = (((1 β π‘) Β· π΅) + (π‘ Β· πΆ)) β§ πΈ = (((1 β π‘) Β· πΉ) + (π‘ Β· πΊ))) β ((πΆ β π΅) Β· πΈ) = (((πΊ β πΉ) Β· π΄) + ((πΉ Β· πΆ) β (π΅ Β· πΊ))))) | ||
Theorem | affineid 46540 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β (((1 β π) Β· π΄) + (π Β· π΄)) = π΄) | ||
Theorem | 1subrec1sub 46541 | 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 46542 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ ((π΄ β β β§ π΅ β β) β π β β) | ||
Theorem | resum2sqgt0 46543 | 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 46544 | 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 46545 | 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 46546 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πΆ < π΄ β¨ πΆ β (π΄[,]π΅) β¨ π΅ < πΆ)) | ||
Theorem | rrx2pxel 46547 | 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 46548 | 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 46549 | 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 46550 | 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 46551 | 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 46552 | 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 46553 | 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 46554* | 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 46555 | 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 46556* | 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 46557* | 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 46558* | 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 46559* | 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 46560* | 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 46561 | 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 46562 | 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 46563 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 46564 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 46565* | 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 46566* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 23592, 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 46567* | 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 46568* | 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 46569* | 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 46570* | 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 46571* | 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 46572* | 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 46571. (Contributed by AV, 13-Feb-2023.) |
β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ πΏ = (LineMβπΈ) β β’ ((πΌ β Fin β§ (π β π β§ π β π β§ π β π)) β (ππΏπ) = {π β π β£ βπ‘ β β βπ β πΌ (πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (πβπ)))}) | ||
Theorem | eenglngeehlnmlem1 46573* | Lemma 1 for eenglngeehlnm 46575. (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 46574* | Lemma 2 for eenglngeehlnm 46575. (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 46575 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 27732) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 46569). (Contributed by AV, 16-Feb-2023.) |
β’ (π β β β (LineGβ(EEGβπ)) = (LineMβ(πΌhilβπ))) | ||
Theorem | rrx2line 46576* | 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 46577* | 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 46578* | 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 46579* | 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 46580* | 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 46581 | 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 46582* | 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 46583* | 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 46584* | 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 46585* | 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 46586* | The sphere around the origin 0 (see rrx0 24684) 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 46587* | Lemma for line2y 46591. 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 46588* | 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 46589* | Lemma for line2x 46590. 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 46590* | 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 46591* | 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 46592 | 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 46593 | 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 46594 | 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 46595 | Lemma for itsclc0 46607. 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 46596 | Lemma for itsclc0 46607. 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 46597 | Lemma for itsclc0 46607. 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 46598 | Lemma 1 for itsclc0yqsol 46600. (Contributed by AV, 6-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π β β) β ((πβ2) β (4 Β· (π Β· π))) = ((4 Β· (π΄β2)) Β· π·)) | ||
Theorem | itsclc0yqsollem2 46599 | Lemma 2 for itsclc0yqsol 46600. (Contributed by AV, 6-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π β β β§ 0 β€ π·) β (ββ((πβ2) β (4 Β· (π Β· π)))) = ((2 Β· (absβπ΄)) Β· (ββπ·))) | ||
Theorem | itsclc0yqsol 46600 | Lemma for itsclc0 46607. 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) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β (π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π) β¨ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |