![]() |
Metamath
Proof Explorer Theorem List (p. 355 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | btwnoutside 35401 | A principle linking outsideness to betweenness. Theorem 6.2 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π Btwn β¨π΄, πΆβ©) β (π Btwn β¨π΅, πΆβ© β πOutsideOfβ¨π΄, π΅β©))) | ||
Theorem | broutsideof3 35402* | Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) | ||
Theorem | outsideofrflx 35403 | Reflexivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π β (πΌβπ) β§ π΄ β (πΌβπ)) β (π΄ β π β πOutsideOfβ¨π΄, π΄β©)) | ||
Theorem | outsideofcom 35404 | Commutativity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β πOutsideOfβ¨π΅, π΄β©)) | ||
Theorem | outsideoftr 35405 | Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((πOutsideOfβ¨π΄, π΅β© β§ πOutsideOfβ¨π΅, πΆβ©) β πOutsideOfβ¨π΄, πΆβ©)) | ||
Theorem | outsideofeq 35406 | Uniqueness law for OutsideOf. Analogue of segconeq 35286. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄OutsideOfβ¨π, π β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π, π β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π = π)) | ||
Theorem | outsideofeu 35407* | Given a nondegenerate ray, there is a unique point congruent to the segment π΅πΆ lying on the ray π΄π . Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π β π΄ β§ π΅ β πΆ) β β!π₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) | ||
Theorem | outsidele 35408 | Relate OutsideOf to Segβ€. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©))) | ||
Theorem | outsideofcol 35409 | Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (πOutsideOfβ¨π, π β© β π Colinear β¨π, π β©) | ||
Syntax | cline2 35410 | Declare the constant for the line function. |
class Line | ||
Syntax | cray 35411 | Declare the constant for the ray function. |
class Ray | ||
Syntax | clines2 35412 | Declare the constant for the set of all lines. |
class LinesEE | ||
Definition | df-line2 35413* | Define the Line function. This function generates the line passing through the distinct points π and π. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.) |
β’ Line = {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} | ||
Definition | df-ray 35414* | Define the Ray function. This function generates the set of all points that lie on the ray starting at π and passing through π. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.) |
β’ Ray = {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} | ||
Definition | df-lines2 35415 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 35428 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
β’ LinesEE = ran Line | ||
Theorem | funray 35416 | Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Ray | ||
Theorem | fvray 35417* | Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π β π΄)) β (πRayπ΄) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π΄, π₯β©}) | ||
Theorem | funline 35418 | Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Line | ||
Theorem | linedegen 35419 | When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄Lineπ΄) = β | ||
Theorem | fvline 35420* | Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β£ π₯ Colinear β¨π΄, π΅β©}) | ||
Theorem | liness 35421 | A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) β (πΌβπ)) | ||
Theorem | fvline2 35422* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π΄, π΅β©}) | ||
Theorem | lineunray 35423 | A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ (π β π β§ π β π )) β (π Btwn β¨π, π β© β (πLineπ) = (((πRayπ) βͺ {π}) βͺ (πRayπ )))) | ||
Theorem | lineelsb2 35424 | If π lies on ππ, then ππ = ππ. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ (π β (πΌβπ) β§ π β π)) β (π β (πLineπ) β (πLineπ) = (πLineπ))) | ||
Theorem | linerflx1 35425 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β π β (πLineπ)) | ||
Theorem | linecom 35426 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β (πLineπ) = (πLineπ)) | ||
Theorem | linerflx2 35427 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β π β (πLineπ)) | ||
Theorem | ellines 35428* | Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄ β LinesEE β βπ β β βπ β (πΌβπ)βπ β (πΌβπ)(π β π β§ π΄ = (πLineπ))) | ||
Theorem | linethru 35429 | If π΄ is a line containing two distinct points π and π, then π΄ is the line through π and π. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β LinesEE β§ (π β π΄ β§ π β π΄) β§ π β π) β π΄ = (πLineπ)) | ||
Theorem | hilbert1.1 35430* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β βπ₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | hilbert1.2 35431* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
β’ (π β π β β*π₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | linethrueu 35432* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β β!π₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | lineintmo 35433* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β LinesEE β§ π΅ β LinesEE β§ π΄ β π΅) β β*π₯(π₯ β π΄ β§ π₯ β π΅)) | ||
Syntax | cfwddif 35434 | Declare the syntax for the forward difference operator. |
class β³ | ||
Definition | df-fwddif 35435* | Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.) |
β’ β³ = (π β (β βpm β) β¦ (π₯ β {π¦ β dom π β£ (π¦ + 1) β dom π} β¦ ((πβ(π₯ + 1)) β (πβπ₯)))) | ||
Syntax | cfwddifn 35436 | Declare the syntax for the nth forward difference operator. |
class
β³ | ||
Definition | df-fwddifn 35437* | Define the nth forward difference operator. This works out to be the forward difference operator iterated π times. (Contributed by Scott Fenton, 28-May-2020.) |
β’
β³ | ||
Theorem | fwddifval 35438 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) & β’ (π β (π + 1) β π΄) β β’ (π β (( β³ βπΉ)βπ) = ((πΉβ(π + 1)) β (πΉβπ))) | ||
Theorem | fwddifnval 35439* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...π)) β (π + π) β π΄) β β’ (π β ((π β³ | ||
Theorem | fwddifn0 35440 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) β β’ (π β ((0 β³ | ||
Theorem | fwddifnp1 35441* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...(π + 1))) β (π + π) β π΄) β β’ (π β (((π + 1) β³ | ||
Theorem | rankung 35442 | The rank of the union of two sets. Closed form of rankun 9853. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (rankβ(π΄ βͺ π΅)) = ((rankβπ΄) βͺ (rankβπ΅))) | ||
Theorem | ranksng 35443 | The rank of a singleton. Closed form of ranksn 9851. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (rankβ{π΄}) = suc (rankβπ΄)) | ||
Theorem | rankelg 35444 | The membership relation is inherited by the rank function. Closed form of rankel 9836. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β (rankβπ΄) β (rankβπ΅)) | ||
Theorem | rankpwg 35445 | The rank of a power set. Closed form of rankpw 9840. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β π β (rankβπ« π΄) = suc (rankβπ΄)) | ||
Theorem | rank0 35446 | The rank of the empty set is β . (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ (rankββ ) = β | ||
Theorem | rankeq1o 35447 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ ((rankβπ΄) = 1o β π΄ = {β }) | ||
Syntax | chf 35448 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 35449 | Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ Hf = βͺ (π 1 β Ο) | ||
Theorem | elhf 35450* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ (π΄ β Hf β βπ₯ β Ο π΄ β (π 1βπ₯)) | ||
Theorem | elhf2 35451 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
β’ π΄ β V β β’ (π΄ β Hf β (rankβπ΄) β Ο) | ||
Theorem | elhf2g 35452 | Hereditarily finiteness via rank. Closed form of elhf2 35451. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (π΄ β Hf β (rankβπ΄) β Ο)) | ||
Theorem | 0hf 35453 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ β β Hf | ||
Theorem | hfun 35454 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ π΅) β Hf ) | ||
Theorem | hfsn 35455 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β Hf β {π΄} β Hf ) | ||
Theorem | hfadj 35456 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ {π΅}) β Hf ) | ||
Theorem | hfelhf 35457 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β π΅ β§ π΅ β Hf ) β π΄ β Hf ) | ||
Theorem | hftr 35458 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Tr Hf | ||
Theorem | hfext 35459* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ = π΅ β βπ₯ β Hf (π₯ β π΄ β π₯ β π΅))) | ||
Theorem | hfuni 35460 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β βͺ π΄ β Hf ) | ||
Theorem | hfpw 35461 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β π« π΄ β Hf ) | ||
Theorem | hfninf 35462 | Ο is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Β¬ Ο β Hf | ||
Theorem | mpomulex 35463* | The multiplication operation is a set. Version of mulex 12977 using maps-to notation , which does not require ax-mulf 11192. (Contributed by GG, 16-Mar-2024.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) β V | ||
Theorem | gg-psercn2 35464* | Since by pserulm 26170 the series converges uniformly, it is also continuous by ulmcn 26147. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11192. (Revised by GG, 16-Mar-2025.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) & β’ (π β π β β) & β’ (π β π < π ) & β’ (π β π β (β‘abs β (0[,]π))) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | gg-rmulccn 35465* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11192. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (topGenβran (,)) & β’ (π β πΆ β β) β β’ (π β (π₯ β β β¦ (π₯ Β· πΆ)) β (π½ Cn π½)) | ||
Theorem | gg-cmvth 35466* | Cauchy's Mean Value Theorem. If πΉ, πΊ are real continuous functions on [π΄, π΅] differentiable on (π΄, π΅), then there is some π₯ β (π΄, π΅) such that πΉ' (π₯) / πΊ' (π₯) = (πΉ(π΄) β πΉ(π΅)) / (πΊ(π΄) β πΊ(π΅)). (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016.) Avoid ax-mulf 11192. (Revised by GG, 16-Mar-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) β β’ (π β βπ₯ β (π΄(,)π΅)(((πΉβπ΅) β (πΉβπ΄)) Β· ((β D πΊ)βπ₯)) = (((πΊβπ΅) β (πΊβπ΄)) Β· ((β D πΉ)βπ₯))) | ||
Theorem | gg-cnfldex 35467 | The field of complex numbers is a set. Alternative proof of cnfldex 21147. This version directly uses df-cnfld 21145, which is discouraged, however it saves all complex numbers axioms and ax-pow 5362. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 16-Mar-2025.) |
β’ βfld β V | ||
Theorem | gg-dvfsumle 35468* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.) Use mpomulcn 24605 instead of mulcn 24603 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) β β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) | ||
Theorem | gg-dvfsumlem2 35469* | Lemma for dvfsumrlim 25783. (Contributed by Mario Carneiro, 17-May-2016.) Use mpomulcn 24605 instead of mulcn 24603 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | gg-cxpcn 35470* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) Use mpomulcn 24605 instead of mulcn 24603 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ π· = (β β (-β(,]0)) & β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π·) β β’ (π₯ β π·, π¦ β β β¦ (π₯βππ¦)) β ((πΎ Γt π½) Cn π½) | ||
Theorem | mpoaddf 35471* | Addition is an operation on complex numbers. Version of ax-addf 11191 using maps-to notation, proved from the axioms of set theory and ax-addcl 11172. (Contributed by GG, 31-Mar-2025.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ + π¦)):(β Γ β)βΆβ | ||
Theorem | mpoaddex 35472* | The addition operation is a set. Version of addex 12976 using maps-to notation , which does not require ax-addf 11191. (Contributed by GG, 31-Mar-2024.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ + π¦)) β V | ||
Theorem | gg-dfcnfld 35473* | Alternative definition of the field of complex numbers. Equivalent to df-cnfld 21145. (Contributed by GG, 31-Mar-2025.) |
β’ βfld = (({β¨(Baseβndx), ββ©, β¨(+gβndx), (π₯ β β, π¦ β β β¦ (π₯ + π¦))β©, β¨(.rβndx), (π₯ β β, π¦ β β β¦ (π₯ Β· π¦))β©} βͺ {β¨(*πβndx), ββ©}) βͺ ({β¨(TopSetβndx), (MetOpenβ(abs β β ))β©, β¨(leβndx), β€ β©, β¨(distβndx), (abs β β )β©} βͺ {β¨(UnifSetβndx), (metUnifβ(abs β β ))β©})) | ||
Theorem | gg-cnfldstr 35474 | The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ βfld Struct β¨1, ;13β© | ||
Theorem | gg-cnfldbas 35475 | The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ β = (Baseββfld) | ||
Theorem | mpocnfldadd 35476* | The addition operation of the field of complex numbers. Version of cnfldadd 21149 using maps-to notation. (Contributed by GG, 31-Mar-2025.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ + π¦)) = (+gββfld) | ||
Theorem | mpocnfldmul 35477* | The multiplication operation of the field of complex numbers. Version of cnfldmul 21150 using maps-to notation. (Contributed by GG, 31-Mar-2025.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) = (.rββfld) | ||
Theorem | gg-cnfldcj 35478 | The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ β = (*πββfld) | ||
Theorem | gg-cnfldtset 35479 | The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ (MetOpenβ(abs β β )) = (TopSetββfld) | ||
Theorem | gg-cnfldle 35480 | The ordering of the field of complex numbers. Note that this is not actually an ordering on β, but we put it in the structure anyway because restricting to β does not affect this component, so that (βfld βΎs β) is an ordered field even though βfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ β€ = (leββfld) | ||
Theorem | gg-cnfldds 35481 | The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ (abs β β ) = (distββfld) | ||
Theorem | gg-cnfldunif 35482 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ (metUnifβ(abs β β )) = (UnifSetββfld) | ||
Theorem | gg-cnfldfun 35483 | The field of complex numbers is a function. The proof is much shorter than the proof of gg-cnfldfunALT 35484 by using cnfldstr 21146 and structn0fun 17088: in addition, it must be shown that β β βfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ Fun βfld | ||
Theorem | gg-cnfldfunALT 35484 | The field of complex numbers is a function. Alternate proof of cnfldfun 21156 not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ Fun βfld | ||
Theorem | gg-cffldtocusgr 35485* | The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Nov-2021.) Revise df-cnfld 21145. (Revised by GG, 31-Mar-2025.) |
β’ π = {π₯ β π« β β£ (β―βπ₯) = 2} & β’ πΊ = (βfld sSet β¨(.efβndx), ( I βΎ π)β©) β β’ πΊ β ComplUSGraph | ||
Theorem | gg-cncrng 35486 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) Use mpocnfldmul 35477. (Revised by GG, 31-Mar-2025.) |
β’ βfld β CRing | ||
Theorem | gg-cnfld1 35487 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) Use mpocnfldmul 35477. (Revised by GG, 31-Mar-2025.) |
β’ 1 = (1rββfld) | ||
Theorem | a1i14 35488 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | a1i24 35489 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | exp5d 35490 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5g 35491 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ π) β (((π β§ π) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5k 35492 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (π β (((π β§ (π β§ π)) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp56 35493 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((((π β§ π) β§ π) β§ (π β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp58 35494 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ ((π β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp510 35495 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ (((π β§ π) β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp511 35496 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ (π β§ π)) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp512 35497 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ π) β§ (π β§ π))) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | 3com12d 35498 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
β’ (π β (π β§ π β§ π)) β β’ (π β (π β§ π β§ π)) | ||
Theorem | imp5p 35499 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ (π β (π β ((π β§ π β§ π) β π))) | ||
Theorem | imp5q 35500 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |