![]() |
Metamath
Proof Explorer Theorem List (p. 478 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1subrec1sub 47701 | 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 47702 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ ((π΄ β β β§ π΅ β β) β π β β) | ||
Theorem | resum2sqgt0 47703 | 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 47704 | 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 47705 | 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 47706 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πΆ < π΄ β¨ πΆ β (π΄[,]π΅) β¨ π΅ < πΆ)) | ||
Theorem | rrx2pxel 47707 | 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 47708 | 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 47709 | 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 47710 | 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 47711 | 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 47712 | 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 47713 | 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 47714* | 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 47715 | 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 47716* | 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 47717* | 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 47718* | 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 47719* | 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 47720* | 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 47721 | 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 47722 | 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 47723 | Declare the syntax for lines in generalized real Euclidean spaces. |
class LineM | ||
Syntax | csph 47724 | Declare the syntax for spheres in generalized real Euclidean spaces. |
class Sphere | ||
Definition | df-line 47725* | 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 47726* | Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 24209, 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 47727* | 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 47728* | 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 47729* | 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 47730* | 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 47731* | 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 47732* | 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 47731. (Contributed by AV, 13-Feb-2023.) |
β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ πΏ = (LineMβπΈ) β β’ ((πΌ β Fin β§ (π β π β§ π β π β§ π β π)) β (ππΏπ) = {π β π β£ βπ‘ β β βπ β πΌ (πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (πβπ)))}) | ||
Theorem | eenglngeehlnmlem1 47733* | Lemma 1 for eenglngeehlnm 47735. (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 47734* | Lemma 2 for eenglngeehlnm 47735. (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 47735 | The line definition in the Tarski structure for the Euclidean geometry (see elntg 28782) corresponds to the definition of lines passing through two different points in a left module (see rrxlines 47729). (Contributed by AV, 16-Feb-2023.) |
β’ (π β β β (LineGβ(EEGβπ)) = (LineMβ(πΌhilβπ))) | ||
Theorem | rrx2line 47736* | 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 47737* | 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 47738* | 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 47739* | 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 47740* | 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 47741 | 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 47742* | 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 47743* | 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 47744* | 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 47745* | 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 47746* | The sphere around the origin 0 (see rrx0 25312) 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 47747* | Lemma for line2y 47751. 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 47748* | 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 47749* | Lemma for line2x 47750. 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 47750* | 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 47751* | 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 47752 | 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 47753 | 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 47754 | 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 47755 | Lemma for itsclc0 47767. 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 47756 | Lemma for itsclc0 47767. 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 47757 | Lemma for itsclc0 47767. 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 47758 | Lemma 1 for itsclc0yqsol 47760. (Contributed by AV, 6-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π β β) β ((πβ2) β (4 Β· (π Β· π))) = ((4 Β· (π΄β2)) Β· π·)) | ||
Theorem | itsclc0yqsollem2 47759 | Lemma 2 for itsclc0yqsol 47760. (Contributed by AV, 6-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π β β β§ 0 β€ π·) β (ββ((πβ2) β (4 Β· (π Β· π)))) = ((2 Β· (absβπ΄)) Β· (ββπ·))) | ||
Theorem | itsclc0yqsol 47760 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0)) β§ (π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β)) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β (π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π) β¨ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))) | ||
Theorem | itscnhlc0xyqsol 47761 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a nonhorizontal line and a circle. (Contributed by AV, 8-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β§ (π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β)) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β ((π = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ (π = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itschlc0xyqsol1 47762 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ = 0 β§ π΅ β 0)) β§ (π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β)) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β (π = (πΆ / π΅) β§ (π = -((ββπ·) / π΅) β¨ π = ((ββπ·) / π΅))))) | ||
Theorem | itschlc0xyqsol 47763 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 8-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ = 0 β§ π΅ β 0)) β§ (π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β)) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β ((π = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ (π = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itsclc0xyqsol 47764 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 25-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0)) β§ (π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β)) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β ((π = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ (π = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itsclc0xyqsolr 47765 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π β β+ β§ 0 β€ π·)) β (((π = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ (π = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))) β (((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ))) | ||
Theorem | itsclc0xyqsolb 47766 | Lemma for itsclc0 47767. Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) β β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0)) β§ ((π β β+ β§ 0 β€ π·) β§ (π β β β§ π β β))) β ((((πβ2) + (πβ2)) = (π β2) β§ ((π΄ Β· π) + (π΅ Β· π)) = πΆ) β ((π = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ (π = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ π = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itsclc0 47767* | The intersection points of a line πΏ and a circle around the origin. (Contributed by AV, 25-Feb-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ πΏ = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π β β+ β§ 0 β€ π·)) β ((π β ( 0 ππ ) β§ π β πΏ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itsclc0b 47768* | The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ πΏ = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π β β+ β§ 0 β€ π·)) β ((π β ( 0 ππ ) β§ π β πΏ) β (π β π β§ (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) | ||
Theorem | itsclinecirc0 47769 | The intersection points of a line through two different points π and π and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 25-Feb-2023.) (Proof shortened by AV, 16-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ πΏ = (LineMβπΈ) & β’ π΄ = ((πβ2) β (πβ2)) & β’ π΅ = ((πβ1) β (πβ1)) & β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ 0 β€ π·)) β ((π β ( 0 ππ ) β§ π β (ππΏπ)) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) | ||
Theorem | itsclinecirc0b 47770 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ πΏ = (LineMβπΈ) & β’ π΄ = ((πβ2) β (πβ2)) & β’ π΅ = ((πβ1) β (πβ1)) & β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ 0 β€ π·)) β ((π β ( 0 ππ ) β§ π β (ππΏπ)) β (π β π β§ (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) | ||
Theorem | itsclinecirc0in 47771 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023.) (Revised by AV, 14-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ πΏ = (LineMβπΈ) & β’ π΄ = ((πβ2) β (πβ2)) & β’ π΅ = ((πβ1) β (πβ1)) & β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ 0 β€ π·)) β (( 0 ππ ) β© (ππΏπ)) = {{β¨1, (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)β©}, {β¨1, (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)β©}}) | ||
Theorem | itsclquadb 47772* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) β β’ ((((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β§ π β β+ β§ π β β) β (βπ₯ β β (((π₯β2) + (πβ2)) = (π β2) β§ ((π΄ Β· π₯) + (π΅ Β· π)) = πΆ) β ((π Β· (πβ2)) + ((π Β· π) + π)) = 0)) | ||
Theorem | itsclquadeu 47773* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 23-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) & β’ π = -(2 Β· (π΅ Β· πΆ)) & β’ π = ((πΆβ2) β ((π΄β2) Β· (π β2))) β β’ ((((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β§ π β β+ β§ π β β) β (β!π₯ β β (((π₯β2) + (πβ2)) = (π β2) β§ ((π΄ Β· π₯) + (π΅ Β· π)) = πΆ) β ((π Β· (πβ2)) + ((π Β· π) + π)) = 0)) | ||
Theorem | 2itscplem1 47774 | Lemma 1 for 2itscp 47777. (Contributed by AV, 4-Mar-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) β β’ (π β ((((πΈβ2) Β· (π΅β2)) + ((π·β2) Β· (π΄β2))) β (2 Β· ((π· Β· π΄) Β· (πΈ Β· π΅)))) = (((π· Β· π΄) β (πΈ Β· π΅))β2)) | ||
Theorem | 2itscplem2 47775 | Lemma 2 for 2itscp 47777. (Contributed by AV, 4-Mar-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) & β’ πΆ = ((π· Β· π΅) + (πΈ Β· π΄)) β β’ (π β (πΆβ2) = ((((π·β2) Β· (π΅β2)) + (2 Β· ((π· Β· π΄) Β· (πΈ Β· π΅)))) + ((πΈβ2) Β· (π΄β2)))) | ||
Theorem | 2itscplem3 47776 | Lemma D for 2itscp 47777. (Contributed by AV, 4-Mar-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) & β’ πΆ = ((π· Β· π΅) + (πΈ Β· π΄)) & β’ (π β π β β) & β’ π = ((πΈβ2) + (π·β2)) & β’ π = (((π β2) Β· π) β (πΆβ2)) β β’ (π β π = ((((πΈβ2) Β· ((π β2) β (π΄β2))) + ((π·β2) Β· ((π β2) β (π΅β2)))) β (2 Β· ((π· Β· π΄) Β· (πΈ Β· π΅))))) | ||
Theorem | 2itscp 47777 | A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023.) (Revised by AV, 16-May-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) & β’ πΆ = ((π· Β· π΅) + (πΈ Β· π΄)) & β’ (π β π β β) & β’ (π β ((π΄β2) + (π΅β2)) < (π β2)) & β’ (π β (π΅ β π β¨ π΄ β π)) & β’ π = ((πΈβ2) + (π·β2)) & β’ π = (((π β2) Β· π) β (πΆβ2)) β β’ (π β 0 < π) | ||
Theorem | itscnhlinecirc02plem1 47778 | Lemma 1 for itscnhlinecirc02p 47781. (Contributed by AV, 6-Mar-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) & β’ πΆ = ((π· Β· π΅) + (πΈ Β· π΄)) & β’ (π β π β β) & β’ (π β ((π΄β2) + (π΅β2)) < (π β2)) & β’ (π β π΅ β π) β β’ (π β 0 < ((-(2 Β· (π· Β· πΆ))β2) β (4 Β· (((πΈβ2) + (π·β2)) Β· ((πΆβ2) β ((πΈβ2) Β· (π β2))))))) | ||
Theorem | itscnhlinecirc02plem2 47779 | Lemma 2 for itscnhlinecirc02p 47781. (Contributed by AV, 10-Mar-2023.) |
β’ π· = (π β π΄) & β’ πΈ = (π΅ β π) & β’ πΆ = ((π΅ Β· π) β (π΄ Β· π)) β β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β) β§ π΅ β π) β§ (π β β β§ ((π΄β2) + (π΅β2)) < (π β2))) β 0 < ((-(2 Β· (π· Β· πΆ))β2) β (4 Β· (((πΈβ2) + (π·β2)) Β· ((πΆβ2) β ((πΈβ2) Β· (π β2))))))) | ||
Theorem | itscnhlinecirc02plem3 47780 | Lemma 3 for itscnhlinecirc02p 47781. (Contributed by AV, 10-Mar-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ πΏ = (LineMβπΈ) & β’ π· = (distβπΈ) β β’ (((π β π β§ π β π β§ (πβ2) β (πβ2)) β§ (π β β+ β§ (ππ· 0 ) < π )) β 0 < ((-(2 Β· (((πβ1) β (πβ1)) Β· (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))))β2) β (4 Β· (((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2)) Β· (((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))β2) β ((((πβ2) β (πβ2))β2) Β· (π β2))))))) | ||
Theorem | itscnhlinecirc02p 47781* | Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ πΏ = (LineMβπΈ) & β’ π· = (distβπΈ) & β’ π = {β¨1, π₯β©, β¨2, π¦β©} β β’ (((π β π β§ π β π β§ (πβ2) β (πβ2)) β§ (π β β+ β§ (ππ· 0 ) < π )) β β!π β π« β((β―βπ ) = 2 β§ βπ¦ β π β!π₯ β β (π β ( 0 ππ ) β§ π β (ππΏπ)))) | ||
Theorem | inlinecirc02plem 47782* | Lemma for inlinecirc02p 47783. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ πΏ = (LineMβπΈ) & β’ π = ((π΄β2) + (π΅β2)) & β’ π· = (((π β2) Β· π) β (πΆβ2)) & β’ π΄ = ((πβ2) β (πβ2)) & β’ π΅ = ((πβ1) β (πβ1)) & β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ 0 < π·)) β βπ β π βπ β π ((( 0 ππ ) β© (ππΏπ)) = {π, π} β§ π β π)) | ||
Theorem | inlinecirc02p 47783 | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 9-May-2023.) (Revised by AV, 16-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ πΏ = (LineMβπΈ) & β’ π· = (distβπΈ) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ (ππ· 0 ) < π )) β (( 0 ππ ) β© (ππΏπ)) β (Pairsproperβπ)) | ||
Theorem | inlinecirc02preu 47784* | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023.) |
β’ πΌ = {1, 2} & β’ πΈ = (β^βπΌ) & β’ π = (β βm πΌ) & β’ π = (SphereβπΈ) & β’ 0 = (πΌ Γ {0}) & β’ πΏ = (LineMβπΈ) & β’ π· = (distβπΈ) β β’ (((π β π β§ π β π β§ π β π) β§ (π β β+ β§ (ππ· 0 ) < π )) β β!π β π« π((β―βπ) = 2 β§ π = (( 0 ππ ) β© (ππΏπ)))) | ||
Theorem | pm4.71da 47785 | Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 561. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β (π β π)) β β’ (π β (π β (π β§ π))) | ||
Theorem | logic1 47786 | Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β (π β π)) & β’ (π β (π β (π β π))) β β’ (π β ((π β π) β (π β π))) | ||
Theorem | logic1a 47787 | Variant of logic1 47786. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β (π β π)) & β’ ((π β§ π) β (π β π)) β β’ (π β ((π β π) β (π β π))) | ||
Theorem | logic2 47788 | Variant of logic1 47786. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β (π β π)) & β’ (π β ((π β§ π) β (π β π))) β β’ (π β ((π β π) β (π β π))) | ||
Theorem | pm5.32dav 47789 | Distribution of implication over biconditional (deduction form). Variant of pm5.32da 578. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ ((π β§ π) β (π β π)) β β’ (π β ((π β§ π) β (π β§ π))) | ||
Theorem | pm5.32dra 47790 | Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.) |
β’ (π β ((π β§ π) β (π β§ π))) β β’ ((π β§ π) β (π β π)) | ||
Theorem | exp12bd 47791 | The import-export theorem (impexp 450) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.) |
β’ (π β (((π β§ π) β π) β ((π β§ π) β π))) β β’ (π β ((π β (π β π)) β (π β (π β π)))) | ||
Theorem | mpbiran3d 47792 | Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 24-Sep-2024.) |
β’ (π β (π β (π β§ π))) & β’ ((π β§ π) β π) β β’ (π β (π β π)) | ||
Theorem | mpbiran4d 47793 | Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 27-Sep-2024.) |
β’ (π β (π β (π β§ π))) & β’ ((π β§ π) β π) β β’ (π β (π β π)) | ||
Theorem | dtrucor3 47794* | An example of how ax-5 1906 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5432 in the ZF set theory. axc16nf 2247 and euae 2650 demonstrate that the violation of dtru 5432 leads to a model with only one object assuming its existence (ax-6 1964). The conclusion is also provable in the empty model ( see emptyal 1904). See also nf5 2271 and nf5i 2135 for the relation between unconditional ax-5 1906 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.) |
β’ Β¬ βπ₯ π₯ = π¦ & β’ (π₯ = π¦ β βπ₯ π₯ = π¦) β β’ βπ₯ π₯ = π¦ | ||
Theorem | ralbidb 47795* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 47796 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.) |
β’ (π β (π₯ β π΄ β (π₯ β π΅ β§ π))) & β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ (π β π))) | ||
Theorem | ralbidc 47796* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 47795. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β (π₯ β π΄ β (π₯ β π΅ β§ π))) & β’ (π β ((π₯ β π΄ β§ (π₯ β π΅ β§ π)) β (π β π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ (π β π))) | ||
Theorem | r19.41dv 47797* | A complex deduction form of r19.41v 3183. (Contributed by Zhi Wang, 6-Sep-2024.) |
β’ (π β βπ₯ β π΄ π) β β’ ((π β§ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | rmotru 47798 | Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.) |
β’ (β*π₯ π₯ β π΄ β β*π₯ β π΄ β€) | ||
Theorem | reutru 47799 | Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.) |
β’ (β!π₯ π₯ β π΄ β β!π₯ β π΄ β€) | ||
Theorem | reutruALT 47800 | Alternate proof for reutru 47799. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (β!π₯ π₯ β π΄ β β!π₯ β π΄ β€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |