![]() |
Metamath
Proof Explorer Theorem List (p. 357 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | meran2 35601 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) | ||
Theorem | meran3 35602 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) | ||
Theorem | waj-ax 35603 | A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ (((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))) βΌ (π βΌ (π βΌ π)))) | ||
Theorem | lukshef-ax2 35604 | A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ ((π βΌ (π βΌ π)) βΌ ((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))))) | ||
Theorem | arg-ax 35605 | A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ ((π βΌ (π βΌ π)) βΌ ((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))))) | ||
Theorem | negsym1 35606 |
In the paper "On Variable Functors of Propositional Arguments",
Lukasiewicz introduced a system that can handle variable connectives.
This was done by introducing a variable, marked with a lowercase delta,
which takes a wff as input. In the system, "delta π "
means that
"something is true of π". The expression "delta
π
" can be
substituted with Β¬ π, π β§ π, βπ₯π, etc.
Later on, Meredith discovered a single axiom, in the form of ( delta delta β₯ β delta π ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus. A symmetry with Β¬. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ (Β¬ Β¬ β₯ β Β¬ π) | ||
Theorem | imsym1 35607 |
A symmetry with β.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | bisym1 35608 |
A symmetry with β.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | consym1 35609 |
A symmetry with β§.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β§ (π β§ β₯)) β (π β§ π)) | ||
Theorem | dissym1 35610 |
A symmetry with β¨.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β¨ (π β¨ β₯)) β (π β¨ π)) | ||
Theorem | nandsym1 35611 |
A symmetry with βΌ.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π βΌ (π βΌ β₯)) β (π βΌ π)) | ||
Theorem | unisym1 35612 |
A symmetry with β.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | exisym1 35613 |
A symmetry with β.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | unqsym1 35614 |
A symmetry with β!.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 6-Sep-2011.) |
β’ (β!π₯β!π₯β₯ β β!π₯π) | ||
Theorem | amosym1 35615 |
A symmetry with β*.
See negsym1 35606 for more information. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ (β*π₯β*π₯β₯ β β*π₯π) | ||
Theorem | subsym1 35616 |
A symmetry with [π₯ / π¦].
See negsym1 35606 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) |
β’ ([π¦ / π₯][π¦ / π₯]β₯ β [π¦ / π₯]π) | ||
Theorem | ontopbas 35617 | An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.) |
β’ (π΅ β On β π΅ β TopBases) | ||
Theorem | onsstopbas 35618 | 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 35619 | 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 35620 | The topology generated from an ordinal number π΅ is suc βͺ π΅. (Contributed by Chen-Pang He, 10-Oct-2015.) |
β’ (π΅ β On β (topGenβπ΅) = suc βͺ π΅) | ||
Theorem | ontgsucval 35621 | The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β (topGenβsuc π΄) = suc π΄) | ||
Theorem | onsuctop 35622 | A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Top) | ||
Theorem | onsuctopon 35623 | One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.) |
β’ (π΄ β On β suc π΄ β (TopOnβπ΄)) | ||
Theorem | ordtoplem 35624 | Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (βͺ π΄ β On β suc βͺ π΄ β π) β β’ (Ord π΄ β (π΄ β βͺ π΄ β π΄ β π)) | ||
Theorem | ordtop 35625 | 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 35626 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ π΄ β On β β’ suc π΄ β Conn | ||
Theorem | onsucconn 35627 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Conn) | ||
Theorem | ordtopconn 35628 | An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Conn)) | ||
Theorem | onintopssconn 35629 | An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (On β© Top) β Conn | ||
Theorem | onsuct0 35630 | A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (π΄ β On β suc π΄ β Kol2) | ||
Theorem | ordtopt0 35631 | An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Kol2)) | ||
Theorem | onsucsuccmpi 35632 | 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 35633 | 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 35634 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ Lim π΄ β β’ Β¬ suc π΄ β Comp | ||
Theorem | limsucncmp 35635 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ (Lim π΄ β Β¬ suc π΄ β Comp) | ||
Theorem | ordcmp 35636 | 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 35637 | The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ {1o, 2o} β (On β© Haus) | ||
Theorem | onint1 35638 | 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 35639 | The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ (On β© Haus) = {1o, 2o} | ||
Theorem | fveleq 35640 | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π΄ = π΅ β ((π β (πΉβπ΄) β π) β (π β (πΉβπ΅) β π))) | ||
Theorem | findfvcl 35641* | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π β (πΉββ ) β π) & β’ (π¦ β Ο β (π β ((πΉβπ¦) β π β (πΉβsuc π¦) β π))) β β’ (π΄ β Ο β (π β (πΉβπ΄) β π)) | ||
Theorem | findreccl 35642* | Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ (πΆ β Ο β (π΄ β π β (rec(πΊ, π΄)βπΆ) β π)) | ||
Theorem | findabrcl 35643* | Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ ((πΆ β Ο β§ π΄ β π) β ((π₯ β V β¦ (rec(πΊ, π΄)βπ₯))βπΆ) β π) | ||
Theorem | nnssi2 35644 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (π΅ β β β π) & β’ ((π΄ β π· β§ π΅ β π· β§ π) β π) β β’ ((π΄ β β β§ π΅ β β) β π) | ||
Theorem | nnssi3 35645 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (πΆ β β β π) & β’ (((π΄ β π· β§ π΅ β π· β§ πΆ β π·) β§ π) β π) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β π) | ||
Theorem | nndivsub 35646 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄ / πΆ) β β β§ π΄ < π΅)) β ((π΅ / πΆ) β β β ((π΅ β π΄) / πΆ) β β)) | ||
Theorem | nndivlub 35647 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ / π΅) β β β π΅ β€ π΄)) | ||
Syntax | cgcdOLD 35648 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (π΄, π΅) | ||
Definition | df-gcdOLD 35649* | 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 35650 | 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 35651* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ (π΄ β β β (πβπ΄) = (absβ((ββ(π΄ + (1 / 2))) β π΄))) | ||
Theorem | dnicld1 35652 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β (absβ((ββ(π΄ + (1 / 2))) β π΄)) β β) | ||
Theorem | dnicld2 35653* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) β β’ (π β (πβπ΄) β β) | ||
Theorem | dnif 35654 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π:ββΆβ | ||
Theorem | dnizeq0 35655* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β€) β β’ (π β (πβπ΄) = 0) | ||
Theorem | dnizphlfeqhlf 35656* | 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 35657 | Variant of rddif 15292. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 β€ ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) | ||
Theorem | dnibndlem1 35658* | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβ((πβπ΅) β (πβπ΄))) β€ π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ π)) | ||
Theorem | dnibndlem2 35659* | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = (ββ(π΄ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem3 35660 | Lemma for dnibnd 35671. (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 35661 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΅ β β β 0 β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem5 35662 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 < (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem6 35663 | Lemma for dnibnd 35671. (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 35664 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΅ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΅ + (1 / 2))) β π΅))) β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem8 35665 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄))) β€ (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem9 35666* | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = ((ββ(π΄ + (1 / 2))) + 1)) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem10 35667 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β 1 β€ (π΅ β π΄)) | ||
Theorem | dnibndlem11 35668 | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ (1 / 2)) | ||
Theorem | dnibndlem12 35669* | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem13 35670* | Lemma for dnibnd 35671. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΄ + (1 / 2))) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibnd 35671* | 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 35672 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π β (ββcnββ) | ||
Theorem | knoppcnlem1 35673* | Lemma for knoppcn 35684. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) = ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄)))) | ||
Theorem | knoppcnlem2 35674* | Lemma for knoppcn 35684. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄))) β β) | ||
Theorem | knoppcnlem3 35675* | Lemma for knoppcn 35684. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) β β) | ||
Theorem | knoppcnlem4 35676* | Lemma for knoppcn 35684. (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 35677* | Lemma for knoppcn 35684. (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 35678* | Lemma for knoppcn 35684. (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 35679* | Lemma for knoppcn 35684. (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 35680* | Lemma for knoppcn 35684. (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 35681* | Lemma for knoppcn 35684. (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 35682* | Lemma for knoppcn 35684. (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 35683* | Lemma for knoppcn 35684. (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 35684* | 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 35685* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β (πβπ΄) β β) | ||
Theorem | unblimceq0lem 35686* | Lemma for unblimceq0 35687. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β βπ β β+ βπ β β+ βπ¦ β π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) | ||
Theorem | unblimceq0 35687* | If πΉ is unbounded near π΄ it has no limit at π΄. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β (πΉ limβ π΄) = β ) | ||
Theorem | unbdqndv1 35688* | 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 35689 | Lemma for unbdqndv2 35691. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β+) & β’ (π β π· β 0) & β’ (π β (2 Β· πΈ) β€ (absβ((π΄ β π΅) / π·))) β β’ (π β ((πΈ Β· (absβπ·)) β€ (absβ(π΄ β πΆ)) β¨ (πΈ Β· (absβπ·)) β€ (absβ(π΅ β πΆ)))) | ||
Theorem | unbdqndv2lem2 35690* | Lemma for unbdqndv2 35691. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ πΊ = (π§ β (π β {π΄}) β¦ (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄))) & β’ π = if((π΅ Β· (π β π)) β€ (absβ((πΉβπ) β (πΉβπ΄))), π, π) & β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β π) & β’ (π β π΅ β β+) & β’ (π β π· β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β€ π΄) & β’ (π β π΄ β€ π) & β’ (π β (π β π) < π·) & β’ (π β (2 Β· π΅) β€ ((absβ((πΉβπ) β (πΉβπ))) / (π β π))) β β’ (π β (π β (π β {π΄}) β§ ((absβ(π β π΄)) < π· β§ π΅ β€ (absβ(πΊβπ))))) | ||
Theorem | unbdqndv2 35691* | Variant of unbdqndv1 35688 with the hypothesis that (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) is unbounded where π₯ β€ π΄ and π΄ β€ π¦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯ β€ π΄ β§ π΄ β€ π¦) β§ ((π¦ β π₯) < π β§ π₯ β π¦) β§ π β€ ((absβ((πΉβπ¦) β (πΉβπ₯))) / (π¦ β π₯)))) β β’ (π β Β¬ π΄ β dom (β D πΉ)) | ||
Theorem | knoppndvlem1 35692 | Lemma for knoppndv 35714. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β π½ β β€) & β’ (π β π β β€) β β’ (π β ((((2 Β· π)β-π½) / 2) Β· π) β β) | ||
Theorem | knoppndvlem2 35693 | Lemma for knoppndv 35714. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β π β β€) & β’ (π β π½ < πΌ) β β’ (π β (((2 Β· π)βπΌ) Β· ((((2 Β· π)β-π½) / 2) Β· π)) β β€) | ||
Theorem | knoppndvlem3 35694 | Lemma for knoppndv 35714. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ (π β πΆ β (-1(,)1)) β β’ (π β (πΆ β β β§ (absβπΆ) < 1)) | ||
Theorem | knoppndvlem4 35695* | Lemma for knoppndv 35714. (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 35696* | Lemma for knoppndv 35714. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π β β) β β’ (π β Ξ£π β (0...π½)((πΉβπ΄)βπ) β β) | ||
Theorem | knoppndvlem6 35697* | Lemma for knoppndv 35714. (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 35698* | Lemma for knoppndv 35714. (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 35699* | Lemma for knoppndv 35714. (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 35700* | Lemma for knoppndv 35714. (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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |