![]() |
Metamath
Proof Explorer Theorem List (p. 354 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 | ||
Theorem | dissym1 35301 |
A symmetry with β¨.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β¨ (π β¨ β₯)) β (π β¨ π)) | ||
Theorem | nandsym1 35302 |
A symmetry with βΌ.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π βΌ (π βΌ β₯)) β (π βΌ π)) | ||
Theorem | unisym1 35303 |
A symmetry with β.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | exisym1 35304 |
A symmetry with β.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | unqsym1 35305 |
A symmetry with β!.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 6-Sep-2011.) |
β’ (β!π₯β!π₯β₯ β β!π₯π) | ||
Theorem | amosym1 35306 |
A symmetry with β*.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ (β*π₯β*π₯β₯ β β*π₯π) | ||
Theorem | subsym1 35307 |
A symmetry with [π₯ / π¦].
See negsym1 35297 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) |
β’ ([π¦ / π₯][π¦ / π₯]β₯ β [π¦ / π₯]π) | ||
Theorem | ontopbas 35308 | An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.) |
β’ (π΅ β On β π΅ β TopBases) | ||
Theorem | onsstopbas 35309 | The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.) |
β’ On β TopBases | ||
Theorem | onpsstopbas 35310 | The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.) |
β’ On β TopBases | ||
Theorem | ontgval 35311 | The topology generated from an ordinal number π΅ is suc βͺ π΅. (Contributed by Chen-Pang He, 10-Oct-2015.) |
β’ (π΅ β On β (topGenβπ΅) = suc βͺ π΅) | ||
Theorem | ontgsucval 35312 | The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β (topGenβsuc π΄) = suc π΄) | ||
Theorem | onsuctop 35313 | A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Top) | ||
Theorem | onsuctopon 35314 | One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.) |
β’ (π΄ β On β suc π΄ β (TopOnβπ΄)) | ||
Theorem | ordtoplem 35315 | Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (βͺ π΄ β On β suc βͺ π΄ β π) β β’ (Ord π΄ β (π΄ β βͺ π΄ β π΄ β π)) | ||
Theorem | ordtop 35316 | An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β βͺ π½)) | ||
Theorem | onsucconni 35317 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ π΄ β On β β’ suc π΄ β Conn | ||
Theorem | onsucconn 35318 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Conn) | ||
Theorem | ordtopconn 35319 | An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Conn)) | ||
Theorem | onintopssconn 35320 | An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (On β© Top) β Conn | ||
Theorem | onsuct0 35321 | A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (π΄ β On β suc π΄ β Kol2) | ||
Theorem | ordtopt0 35322 | An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Kol2)) | ||
Theorem | onsucsuccmpi 35323 | The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015.) |
β’ π΄ β On β β’ suc suc π΄ β Comp | ||
Theorem | onsucsuccmp 35324 | The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.) |
β’ (π΄ β On β suc suc π΄ β Comp) | ||
Theorem | limsucncmpi 35325 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ Lim π΄ β β’ Β¬ suc π΄ β Comp | ||
Theorem | limsucncmp 35326 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ (Lim π΄ β Β¬ suc π΄ β Comp) | ||
Theorem | ordcmp 35327 | An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1o. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (Ord π΄ β (π΄ β Comp β (βͺ π΄ = βͺ βͺ π΄ β π΄ = 1o))) | ||
Theorem | ssoninhaus 35328 | The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ {1o, 2o} β (On β© Haus) | ||
Theorem | onint1 35329 | The ordinal T1 spaces are 1o and 2o, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.) |
β’ (On β© Fre) = {1o, 2o} | ||
Theorem | oninhaus 35330 | The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ (On β© Haus) = {1o, 2o} | ||
Theorem | fveleq 35331 | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π΄ = π΅ β ((π β (πΉβπ΄) β π) β (π β (πΉβπ΅) β π))) | ||
Theorem | findfvcl 35332* | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π β (πΉββ ) β π) & β’ (π¦ β Ο β (π β ((πΉβπ¦) β π β (πΉβsuc π¦) β π))) β β’ (π΄ β Ο β (π β (πΉβπ΄) β π)) | ||
Theorem | findreccl 35333* | Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ (πΆ β Ο β (π΄ β π β (rec(πΊ, π΄)βπΆ) β π)) | ||
Theorem | findabrcl 35334* | Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ ((πΆ β Ο β§ π΄ β π) β ((π₯ β V β¦ (rec(πΊ, π΄)βπ₯))βπΆ) β π) | ||
Theorem | nnssi2 35335 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (π΅ β β β π) & β’ ((π΄ β π· β§ π΅ β π· β§ π) β π) β β’ ((π΄ β β β§ π΅ β β) β π) | ||
Theorem | nnssi3 35336 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (πΆ β β β π) & β’ (((π΄ β π· β§ π΅ β π· β§ πΆ β π·) β§ π) β π) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β π) | ||
Theorem | nndivsub 35337 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄ / πΆ) β β β§ π΄ < π΅)) β ((π΅ / πΆ) β β β ((π΅ β π΄) / πΆ) β β)) | ||
Theorem | nndivlub 35338 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ / π΅) β β β π΅ β€ π΄)) | ||
Syntax | cgcdOLD 35339 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (π΄, π΅) | ||
Definition | df-gcdOLD 35340* | gcdOLD (π΄, π΅) is the largest positive integer that evenly divides both π΄ and π΅. (Contributed by Jeff Hoffman, 17-Jun-2008.) (New usage is discouraged.) |
β’ gcdOLD (π΄, π΅) = sup({π₯ β β β£ ((π΄ / π₯) β β β§ (π΅ / π₯) β β)}, β, < ) | ||
Theorem | ee7.2aOLD 35341 | Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as π΄ mod π΅. Here, just one subtraction step is proved to preserve the gcdOLD. The rec function will be used in other proofs for iterated subtraction. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β gcdOLD (π΄, π΅) = gcdOLD (π΄, (π΅ β π΄)))) | ||
Theorem | dnival 35342* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ (π΄ β β β (πβπ΄) = (absβ((ββ(π΄ + (1 / 2))) β π΄))) | ||
Theorem | dnicld1 35343 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β (absβ((ββ(π΄ + (1 / 2))) β π΄)) β β) | ||
Theorem | dnicld2 35344* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) β β’ (π β (πβπ΄) β β) | ||
Theorem | dnif 35345 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π:ββΆβ | ||
Theorem | dnizeq0 35346* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β€) β β’ (π β (πβπ΄) = 0) | ||
Theorem | dnizphlfeqhlf 35347* | The distance to nearest integer is a half for half-integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β€) β β’ (π β (πβ(π΄ + (1 / 2))) = (1 / 2)) | ||
Theorem | rddif2 35348 | Variant of rddif 15286. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 β€ ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) | ||
Theorem | dnibndlem1 35349* | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβ((πβπ΅) β (πβπ΄))) β€ π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ π)) | ||
Theorem | dnibndlem2 35350* | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = (ββ(π΄ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem3 35351 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = ((ββ(π΄ + (1 / 2))) + 1)) β β’ (π β (absβ(π΅ β π΄)) = (absβ((π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2))) + (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)))) | ||
Theorem | dnibndlem4 35352 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΅ β β β 0 β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem5 35353 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 < (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem6 35354 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ (((1 / 2) β (absβ((ββ(π΅ + (1 / 2))) β π΅))) + ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄))))) | ||
Theorem | dnibndlem7 35355 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΅ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΅ + (1 / 2))) β π΅))) β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem8 35356 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄))) β€ (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem9 35357* | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = ((ββ(π΄ + (1 / 2))) + 1)) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem10 35358 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β 1 β€ (π΅ β π΄)) | ||
Theorem | dnibndlem11 35359 | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ (1 / 2)) | ||
Theorem | dnibndlem12 35360* | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem13 35361* | Lemma for dnibnd 35362. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΄ + (1 / 2))) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibnd 35362* | The "distance to nearest integer" function is 1-Lipschitz continuous, i.e., is a short map. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnicn 35363 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π β (ββcnββ) | ||
Theorem | knoppcnlem1 35364* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) = ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄)))) | ||
Theorem | knoppcnlem2 35365* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄))) β β) | ||
Theorem | knoppcnlem3 35366* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) β β) | ||
Theorem | knoppcnlem4 35367* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β (absβ((πΉβπ΄)βπ)) β€ ((π β β0 β¦ ((absβπΆ)βπ))βπ)) | ||
Theorem | knoppcnlem5 35368* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) β β’ (π β (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))):β0βΆ(β βm β)) | ||
Theorem | knoppcnlem6 35369* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) β dom (βπ’ββ)) | ||
Theorem | knoppcnlem7 35370* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π β β0) β β’ (π β (seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π€ β β β¦ (seq0( + , (πΉβπ€))βπ))) | ||
Theorem | knoppcnlem8 35371* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) β β’ (π β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(β βm β)) | ||
Theorem | knoppcnlem9 35372* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) | ||
Theorem | knoppcnlem10 35373* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π β β0) β β’ (π β (π§ β β β¦ ((πΉβπ§)βπ)) β ((topGenβran (,)) Cn (TopOpenββfld))) | ||
Theorem | knoppcnlem11 35374* | Lemma for knoppcn 35375. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) β β’ (π β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(ββcnββ)) | ||
Theorem | knoppcn 35375* | The continuous nowhere differentiable function π ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β π β (ββcnββ)) | ||
Theorem | knoppcld 35376* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β (πβπ΄) β β) | ||
Theorem | unblimceq0lem 35377* | Lemma for unblimceq0 35378. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β βπ β β+ βπ β β+ βπ¦ β π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) | ||
Theorem | unblimceq0 35378* | If πΉ is unbounded near π΄ it has no limit at π΄. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β (πΉ limβ π΄) = β ) | ||
Theorem | unbdqndv1 35379* | If the difference quotient (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄)) is unbounded near π΄ then πΉ is not differentiable at π΄. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ πΊ = (π§ β (π β {π΄}) β¦ (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄))) & β’ (π β π β β) & β’ (π β π β π) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β β+ βπ β β+ βπ₯ β (π β {π΄})((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΊβπ₯)))) β β’ (π β Β¬ π΄ β dom (π D πΉ)) | ||
Theorem | unbdqndv2lem1 35380 | Lemma for unbdqndv2 35382. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β+) & β’ (π β π· β 0) & β’ (π β (2 Β· πΈ) β€ (absβ((π΄ β π΅) / π·))) β β’ (π β ((πΈ Β· (absβπ·)) β€ (absβ(π΄ β πΆ)) β¨ (πΈ Β· (absβπ·)) β€ (absβ(π΅ β πΆ)))) | ||
Theorem | unbdqndv2lem2 35381* | Lemma for unbdqndv2 35382. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ πΊ = (π§ β (π β {π΄}) β¦ (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄))) & β’ π = if((π΅ Β· (π β π)) β€ (absβ((πΉβπ) β (πΉβπ΄))), π, π) & β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β π) & β’ (π β π΅ β β+) & β’ (π β π· β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β€ π΄) & β’ (π β π΄ β€ π) & β’ (π β (π β π) < π·) & β’ (π β (2 Β· π΅) β€ ((absβ((πΉβπ) β (πΉβπ))) / (π β π))) β β’ (π β (π β (π β {π΄}) β§ ((absβ(π β π΄)) < π· β§ π΅ β€ (absβ(πΊβπ))))) | ||
Theorem | unbdqndv2 35382* | Variant of unbdqndv1 35379 with the hypothesis that (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) is unbounded where π₯ β€ π΄ and π΄ β€ π¦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯ β€ π΄ β§ π΄ β€ π¦) β§ ((π¦ β π₯) < π β§ π₯ β π¦) β§ π β€ ((absβ((πΉβπ¦) β (πΉβπ₯))) / (π¦ β π₯)))) β β’ (π β Β¬ π΄ β dom (β D πΉ)) | ||
Theorem | knoppndvlem1 35383 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β π½ β β€) & β’ (π β π β β€) β β’ (π β ((((2 Β· π)β-π½) / 2) Β· π) β β) | ||
Theorem | knoppndvlem2 35384 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β π β β€) & β’ (π β π½ < πΌ) β β’ (π β (((2 Β· π)βπΌ) Β· ((((2 Β· π)β-π½) / 2) Β· π)) β β€) | ||
Theorem | knoppndvlem3 35385 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ (π β πΆ β (-1(,)1)) β β’ (π β (πΆ β β β§ (absβπΆ) < 1)) | ||
Theorem | knoppndvlem4 35386* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π΄ β β) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π β β) β β’ (π β seq0( + , (πΉβπ΄)) β (πβπ΄)) | ||
Theorem | knoppndvlem5 35387* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π β β) β β’ (π β Ξ£π β (0...π½)((πΉβπ΄)βπ) β β) | ||
Theorem | knoppndvlem6 35388* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β (πβπ΄) = Ξ£π β (0...π½)((πΉβπ΄)βπ)) | ||
Theorem | knoppndvlem7 35389* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((πΉβπ΄)βπ½) = ((πΆβπ½) Β· (πβ(π / 2)))) | ||
Theorem | knoppndvlem8 35390* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β 2 β₯ π) β β’ (π β ((πΉβπ΄)βπ½) = 0) | ||
Theorem | knoppndvlem9 35391* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) β β’ (π β ((πΉβπ΄)βπ½) = ((πΆβπ½) / 2)) | ||
Theorem | knoppndvlem10 35392* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ π΅ = ((((2 Β· π)β-π½) / 2) Β· (π + 1)) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β (absβ(((πΉβπ΅)βπ½) β ((πΉβπ΄)βπ½))) = (((absβπΆ)βπ½) / 2)) | ||
Theorem | knoppndvlem11 35393* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 28-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β) β β’ (π β (absβ(Ξ£π β (0...(π½ β 1))((πΉβπ΅)βπ) β Ξ£π β (0...(π½ β 1))((πΉβπ΄)βπ))) β€ ((absβ(π΅ β π΄)) Β· Ξ£π β (0...(π½ β 1))(((2 Β· π) Β· (absβπΆ))βπ))) | ||
Theorem | knoppndvlem12 35394 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 29-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β πΆ β (-1(,)1)) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β (((2 Β· π) Β· (absβπΆ)) β 1 β§ 1 < (((2 Β· π) Β· (absβπΆ)) β 1))) | ||
Theorem | knoppndvlem13 35395 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β πΆ β (-1(,)1)) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β πΆ β 0) | ||
Theorem | knoppndvlem14 35396* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 7-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ π΅ = ((((2 Β· π)β-π½) / 2) Β· (π + 1)) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β (absβ(Ξ£π β (0...(π½ β 1))((πΉβπ΅)βπ) β Ξ£π β (0...(π½ β 1))((πΉβπ΄)βπ))) β€ ((((absβπΆ)βπ½) / 2) Β· (1 / (((2 Β· π) Β· (absβπΆ)) β 1)))) | ||
Theorem | knoppndvlem15 35397* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 6-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ π΅ = ((((2 Β· π)β-π½) / 2) Β· (π + 1)) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β ((((absβπΆ)βπ½) / 2) Β· (1 β (1 / (((2 Β· π) Β· (absβπΆ)) β 1)))) β€ (absβ((πβπ΅) β (πβπ΄)))) | ||
Theorem | knoppndvlem16 35398 | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 19-Jul-2021.) |
β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ π΅ = ((((2 Β· π)β-π½) / 2) Β· (π + 1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β (π΅ β π΄) = (((2 Β· π)β-π½) / 2)) | ||
Theorem | knoppndvlem17 35399* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 12-Aug-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ π΄ = ((((2 Β· π)β-π½) / 2) Β· π) & β’ π΅ = ((((2 Β· π)β-π½) / 2) Β· (π + 1)) & β’ (π β πΆ β (-1(,)1)) & β’ (π β π½ β β0) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β ((((2 Β· π) Β· (absβπΆ))βπ½) Β· (1 β (1 / (((2 Β· π) Β· (absβπΆ)) β 1)))) β€ ((absβ((πβπ΅) β (πβπ΄))) / (π΅ β π΄))) | ||
Theorem | knoppndvlem18 35400* | Lemma for knoppndv 35405. (Contributed by Asger C. Ipsen, 14-Aug-2021.) |
β’ (π β πΆ β (-1(,)1)) & β’ (π β π β β) & β’ (π β π· β β+) & β’ (π β πΈ β β+) & β’ (π β πΊ β β+) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β βπ β β0 ((((2 Β· π)β-π) / 2) < π· β§ πΈ β€ ((((2 Β· π) Β· (absβπΆ))βπ) Β· πΊ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |