![]() |
Metamath
Proof Explorer Theorem List (p. 352 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cline2 35101 | Declare the constant for the line function. |
class Line | ||
Syntax | cray 35102 | Declare the constant for the ray function. |
class Ray | ||
Syntax | clines2 35103 | Declare the constant for the set of all lines. |
class LinesEE | ||
Definition | df-line2 35104* | 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 35105* | 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 35106 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 35119 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
β’ LinesEE = ran Line | ||
Theorem | funray 35107 | 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 35108* | 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 35109 | 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 35110 | 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 35111* | 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 35112 | 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 35113* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π΄, π΅β©}) | ||
Theorem | lineunray 35114 | 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 35115 | 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 35116 | 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 35117 | 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 35118 | 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 35119* | 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 35120 | 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 35121* | 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 35122* | 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 35123* | 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 35124* | 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 35125 | Declare the syntax for the forward difference operator. |
class β³ | ||
Definition | df-fwddif 35126* | 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 35127 | Declare the syntax for the nth forward difference operator. |
class
β³ | ||
Definition | df-fwddifn 35128* | 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 35129 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) & β’ (π β (π + 1) β π΄) β β’ (π β (( β³ βπΉ)βπ) = ((πΉβ(π + 1)) β (πΉβπ))) | ||
Theorem | fwddifnval 35130* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...π)) β (π + π) β π΄) β β’ (π β ((π β³ | ||
Theorem | fwddifn0 35131 | 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 35132* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...(π + 1))) β (π + π) β π΄) β β’ (π β (((π + 1) β³ | ||
Theorem | rankung 35133 | The rank of the union of two sets. Closed form of rankun 9850. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (rankβ(π΄ βͺ π΅)) = ((rankβπ΄) βͺ (rankβπ΅))) | ||
Theorem | ranksng 35134 | The rank of a singleton. Closed form of ranksn 9848. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (rankβ{π΄}) = suc (rankβπ΄)) | ||
Theorem | rankelg 35135 | The membership relation is inherited by the rank function. Closed form of rankel 9833. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β (rankβπ΄) β (rankβπ΅)) | ||
Theorem | rankpwg 35136 | The rank of a power set. Closed form of rankpw 9837. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β π β (rankβπ« π΄) = suc (rankβπ΄)) | ||
Theorem | rank0 35137 | The rank of the empty set is β . (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ (rankββ ) = β | ||
Theorem | rankeq1o 35138 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ ((rankβπ΄) = 1o β π΄ = {β }) | ||
Syntax | chf 35139 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 35140 | 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 35141* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ (π΄ β Hf β βπ₯ β Ο π΄ β (π 1βπ₯)) | ||
Theorem | elhf2 35142 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
β’ π΄ β V β β’ (π΄ β Hf β (rankβπ΄) β Ο) | ||
Theorem | elhf2g 35143 | Hereditarily finiteness via rank. Closed form of elhf2 35142. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (π΄ β Hf β (rankβπ΄) β Ο)) | ||
Theorem | 0hf 35144 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ β β Hf | ||
Theorem | hfun 35145 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ π΅) β Hf ) | ||
Theorem | hfsn 35146 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β Hf β {π΄} β Hf ) | ||
Theorem | hfadj 35147 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ {π΅}) β Hf ) | ||
Theorem | hfelhf 35148 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β π΅ β§ π΅ β Hf ) β π΄ β Hf ) | ||
Theorem | hftr 35149 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Tr Hf | ||
Theorem | hfext 35150* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ = π΅ β βπ₯ β Hf (π₯ β π΄ β π₯ β π΅))) | ||
Theorem | hfuni 35151 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β βͺ π΄ β Hf ) | ||
Theorem | hfpw 35152 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β π« π΄ β Hf ) | ||
Theorem | hfninf 35153 | Ο is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Β¬ Ο β Hf | ||
Theorem | mpomulf 35154* | Multiplication is an operation on complex numbers. Version of ax-mulf 11189 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11171. (Contributed by GG, 16-Mar-2025.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)):(β Γ β)βΆβ | ||
Theorem | ovmul 35155* | Multiplication of complex numbers produces the same value as multiplication expressed in maps-to notation of the same complex numbers. (Contributed by GG, 16-Mar-2025.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π΅) = (π΄ Β· π΅)) | ||
Theorem | mpomulex 35156* | The multiplication operation is a set. Version of mulex 12972 using maps-to notation , which does not require ax-mulf 11189. (Contributed by GG, 16-Mar-2024.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) β V | ||
Theorem | mpomulcn 35157* | Complex number multiplication is a continuous function. Version of mulcn 24382 using maps-to notation, which does not require ax-mulf 11189. (Contributed by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) β ((π½ Γt π½) Cn π½) | ||
Theorem | gg-divcn 35158 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt (β β {0})) β β’ / β ((π½ Γt πΎ) Cn π½) | ||
Theorem | gg-expcn 35159* | The power function on complex numbers, for fixed exponent π, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (π½ Cn π½)) | ||
Theorem | gg-divccn 35160* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β β¦ (π₯ / π΄)) β (π½ Cn π½)) | ||
Theorem | gg-negcncf 35161* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ πΉ = (π₯ β π΄ β¦ -π₯) β β’ (π΄ β β β πΉ β (π΄βcnββ)) | ||
Theorem | gg-iihalf1cn 35162 | The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = ((topGenβran (,)) βΎt (0[,](1 / 2))) β β’ (π₯ β (0[,](1 / 2)) β¦ (2 Β· π₯)) β (π½ Cn II) | ||
Theorem | gg-iihalf2cn 35163 | The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = ((topGenβran (,)) βΎt ((1 / 2)[,]1)) β β’ (π₯ β ((1 / 2)[,]1) β¦ ((2 Β· π₯) β 1)) β (π½ Cn II) | ||
Theorem | gg-iimulcn 35164* | Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (π₯ Β· π¦)) β ((II Γt II) Cn II) | ||
Theorem | gg-icchmeo 35165* | The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [π΄, π΅] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) & β’ πΉ = (π₯ β (0[,]1) β¦ ((π₯ Β· π΅) + ((1 β π₯) Β· π΄))) β β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β πΉ β (IIHomeo(π½ βΎt (π΄[,]π΅)))) | ||
Theorem | gg-cnrehmeo 35166* | The canonical bijection from (β Γ β) to β described in cnref1o 12968 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if (β Γ β) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π½ = (topGenβran (,)) & β’ πΎ = (TopOpenββfld) β β’ πΉ β ((π½ Γt π½)HomeoπΎ) | ||
Theorem | gg-reparphti 35167* | Lemma for reparpht 24513. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) & β’ π» = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβ(((1 β π¦) Β· (πΊβπ₯)) + (π¦ Β· π₯)))) β β’ (π β π» β ((πΉ β πΊ)(PHtpyβπ½)πΉ)) | ||
Theorem | gg-mulcncf 35168* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) | ||
Theorem | gg-dvcnp2 35169 | A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (πΎ βΎt π΄) & β’ πΎ = (TopOpenββfld) β β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΉ β ((π½ CnP πΎ)βπ΅)) | ||
Theorem | gg-dvmulbr 35170 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25457. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β πΆ(π D πΉ)πΎ) & β’ (π β πΆ(π D πΊ)πΏ) & β’ π½ = (TopOpenββfld) β β’ (π β πΆ(π D (πΉ βf Β· πΊ))((πΎ Β· (πΊβπΆ)) + (πΏ Β· (πΉβπΆ)))) | ||
Theorem | gg-dvcobr 35171 | The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 25463. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆπ) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β (πΊβπΆ)(π D πΉ)πΎ) & β’ (π β πΆ(π D πΊ)πΏ) & β’ π½ = (TopOpenββfld) β β’ (π β πΆ(π D (πΉ β πΊ))(πΎ Β· πΏ)) | ||
Theorem | gg-plycn 35172 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) | ||
Theorem | gg-psercn2 35173* | Since by pserulm 25933 the series converges uniformly, it is also continuous by ulmcn 25910. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) & β’ (π β π β β) & β’ (π β π < π ) & β’ (π β π β (β‘abs β (0[,]π))) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | gg-rmulccn 35174* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11189. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (topGenβran (,)) & β’ (π β πΆ β β) β β’ (π β (π₯ β β β¦ (π₯ Β· πΆ)) β (π½ Cn π½)) | ||
Theorem | gg-cnfldex 35175 | The field of complex numbers is a set. Alternative proof of cnfldex 20946. This version direcly uses df-cnfld 20944, which is discouraged, however it saves all complex numbers axioms and ax-pow 5363. (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-cmvth 35176* | 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.) Use mpomulcn 35157 instead of mulcn 24382 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) β β’ (π β βπ₯ β (π΄(,)π΅)(((πΉβπ΅) β (πΉβπ΄)) Β· ((β D πΊ)βπ₯)) = (((πΊβπ΅) β (πΊβπ΄)) Β· ((β D πΉ)βπ₯))) | ||
Theorem | gg-dvfsumle 35177* | 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 35157 instead of mulcn 24382 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) β β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) | ||
Theorem | gg-dvfsumlem2 35178* | Lemma for dvfsumrlim 25547. (Contributed by Mario Carneiro, 17-May-2016.) Use mpomulcn 35157 instead of mulcn 24382 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | gg-cxpcn 35179* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) Use mpomulcn 35157 instead of mulcn 24382 as direct dependency. (Revised by GG, 16-Mar-2025.) |
β’ π· = (β β (-β(,]0)) & β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π·) β β’ (π₯ β π·, π¦ β β β¦ (π₯βππ¦)) β ((πΎ Γt π½) Cn π½) | ||
Theorem | a1i14 35180 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | a1i24 35181 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | exp5d 35182 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5g 35183 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ π) β (((π β§ π) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5k 35184 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (π β (((π β§ (π β§ π)) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp56 35185 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((((π β§ π) β§ π) β§ (π β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp58 35186 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ ((π β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp510 35187 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ (((π β§ π) β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp511 35188 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ (π β§ π)) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp512 35189 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ π) β§ (π β§ π))) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | 3com12d 35190 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
β’ (π β (π β§ π β§ π)) β β’ (π β (π β§ π β§ π)) | ||
Theorem | imp5p 35191 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ (π β (π β ((π β§ π β§ π) β π))) | ||
Theorem | imp5q 35192 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) | ||
Theorem | ecase13d 35193 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
β’ (π β Β¬ π) & β’ (π β Β¬ π) & β’ (π β (π β¨ π β¨ π)) β β’ (π β π) | ||
Theorem | subtr 35194 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β π = π) & β’ (π₯ = π΅ β π = π) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β π = π)) | ||
Theorem | subtr2 35195 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β (π β π))) | ||
Theorem | trer 35196* | A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ (βπβπβπ((π β€ π β§ π β€ π) β π β€ π) β ( β€ β© β‘ β€ ) Er dom ( β€ β© β‘ β€ )) | ||
Theorem | elicc3 35197 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ π΅ β§ (πΆ = π΄ β¨ (π΄ < πΆ β§ πΆ < π΅) β¨ πΆ = π΅)))) | ||
Theorem | finminlem 35198* | A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.) |
β’ (π₯ = π¦ β (π β π)) β β’ (βπ₯ β Fin π β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) | ||
Theorem | gtinf 35199* | Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) (Revised by AV, 10-Oct-2021.) |
β’ (((π β β β§ π β β β§ βπ₯ β β βπ¦ β π π₯ β€ π¦) β§ (π΄ β β β§ inf(π, β, < ) < π΄)) β βπ§ β π π§ < π΄) | ||
Theorem | opnrebl 35200* | A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.) |
β’ (π΄ β (topGenβran (,)) β (π΄ β β β§ βπ₯ β π΄ βπ¦ β β+ ((π₯ β π¦)(,)(π₯ + π¦)) β π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |