![]() |
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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | arg-ax 35301 | 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 35302 |
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 35303 |
A symmetry with β.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | bisym1 35304 |
A symmetry with β.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | consym1 35305 |
A symmetry with β§.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β§ (π β§ β₯)) β (π β§ π)) | ||
Theorem | dissym1 35306 |
A symmetry with β¨.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β¨ (π β¨ β₯)) β (π β¨ π)) | ||
Theorem | nandsym1 35307 |
A symmetry with βΌ.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π βΌ (π βΌ β₯)) β (π βΌ π)) | ||
Theorem | unisym1 35308 |
A symmetry with β.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | exisym1 35309 |
A symmetry with β.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ (βπ₯βπ₯β₯ β βπ₯π) | ||
Theorem | unqsym1 35310 |
A symmetry with β!.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 6-Sep-2011.) |
β’ (β!π₯β!π₯β₯ β β!π₯π) | ||
Theorem | amosym1 35311 |
A symmetry with β*.
See negsym1 35302 for more information. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ (β*π₯β*π₯β₯ β β*π₯π) | ||
Theorem | subsym1 35312 |
A symmetry with [π₯ / π¦].
See negsym1 35302 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) |
β’ ([π¦ / π₯][π¦ / π₯]β₯ β [π¦ / π₯]π) | ||
Theorem | ontopbas 35313 | An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.) |
β’ (π΅ β On β π΅ β TopBases) | ||
Theorem | onsstopbas 35314 | 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 35315 | 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 35316 | The topology generated from an ordinal number π΅ is suc βͺ π΅. (Contributed by Chen-Pang He, 10-Oct-2015.) |
β’ (π΅ β On β (topGenβπ΅) = suc βͺ π΅) | ||
Theorem | ontgsucval 35317 | The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β (topGenβsuc π΄) = suc π΄) | ||
Theorem | onsuctop 35318 | A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Top) | ||
Theorem | onsuctopon 35319 | One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.) |
β’ (π΄ β On β suc π΄ β (TopOnβπ΄)) | ||
Theorem | ordtoplem 35320 | Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (βͺ π΄ β On β suc βͺ π΄ β π) β β’ (Ord π΄ β (π΄ β βͺ π΄ β π΄ β π)) | ||
Theorem | ordtop 35321 | 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 35322 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ π΄ β On β β’ suc π΄ β Conn | ||
Theorem | onsucconn 35323 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (π΄ β On β suc π΄ β Conn) | ||
Theorem | ordtopconn 35324 | An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Conn)) | ||
Theorem | onintopssconn 35325 | An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.) |
β’ (On β© Top) β Conn | ||
Theorem | onsuct0 35326 | A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (π΄ β On β suc π΄ β Kol2) | ||
Theorem | ordtopt0 35327 | An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.) |
β’ (Ord π½ β (π½ β Top β π½ β Kol2)) | ||
Theorem | onsucsuccmpi 35328 | 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 35329 | 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 35330 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ Lim π΄ β β’ Β¬ suc π΄ β Comp | ||
Theorem | limsucncmp 35331 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
β’ (Lim π΄ β Β¬ suc π΄ β Comp) | ||
Theorem | ordcmp 35332 | 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 35333 | The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ {1o, 2o} β (On β© Haus) | ||
Theorem | onint1 35334 | 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 35335 | The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.) |
β’ (On β© Haus) = {1o, 2o} | ||
Theorem | fveleq 35336 | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π΄ = π΅ β ((π β (πΉβπ΄) β π) β (π β (πΉβπ΅) β π))) | ||
Theorem | findfvcl 35337* | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
β’ (π β (πΉββ ) β π) & β’ (π¦ β Ο β (π β ((πΉβπ¦) β π β (πΉβsuc π¦) β π))) β β’ (π΄ β Ο β (π β (πΉβπ΄) β π)) | ||
Theorem | findreccl 35338* | Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ (πΆ β Ο β (π΄ β π β (rec(πΊ, π΄)βπΆ) β π)) | ||
Theorem | findabrcl 35339* | Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ (π§ β π β (πΊβπ§) β π) β β’ ((πΆ β Ο β§ π΄ β π) β ((π₯ β V β¦ (rec(πΊ, π΄)βπ₯))βπΆ) β π) | ||
Theorem | nnssi2 35340 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (π΅ β β β π) & β’ ((π΄ β π· β§ π΅ β π· β§ π) β π) β β’ ((π΄ β β β§ π΅ β β) β π) | ||
Theorem | nnssi3 35341 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ β β π· & β’ (πΆ β β β π) & β’ (((π΄ β π· β§ π΅ β π· β§ πΆ β π·) β§ π) β π) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β π) | ||
Theorem | nndivsub 35342 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄ / πΆ) β β β§ π΄ < π΅)) β ((π΅ / πΆ) β β β ((π΅ β π΄) / πΆ) β β)) | ||
Theorem | nndivlub 35343 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ / π΅) β β β π΅ β€ π΄)) | ||
Syntax | cgcdOLD 35344 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (π΄, π΅) | ||
Definition | df-gcdOLD 35345* | 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 35346 | 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 35347* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ (π΄ β β β (πβπ΄) = (absβ((ββ(π΄ + (1 / 2))) β π΄))) | ||
Theorem | dnicld1 35348 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β (absβ((ββ(π΄ + (1 / 2))) β π΄)) β β) | ||
Theorem | dnicld2 35349* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) β β’ (π β (πβπ΄) β β) | ||
Theorem | dnif 35350 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π:ββΆβ | ||
Theorem | dnizeq0 35351* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β€) β β’ (π β (πβπ΄) = 0) | ||
Theorem | dnizphlfeqhlf 35352* | 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 35353 | Variant of rddif 15287. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 β€ ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) | ||
Theorem | dnibndlem1 35354* | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβ((πβπ΅) β (πβπ΄))) β€ π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ π)) | ||
Theorem | dnibndlem2 35355* | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = (ββ(π΄ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem3 35356 | Lemma for dnibnd 35367. (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 35357 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΅ β β β 0 β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem5 35358 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π΄ β β β 0 < (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem6 35359 | Lemma for dnibnd 35367. (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 35360 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΅ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΅ + (1 / 2))) β π΅))) β€ (π΅ β ((ββ(π΅ + (1 / 2))) β (1 / 2)))) | ||
Theorem | dnibndlem8 35361 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) β β’ (π β ((1 / 2) β (absβ((ββ(π΄ + (1 / 2))) β π΄))) β€ (((ββ(π΄ + (1 / 2))) + (1 / 2)) β π΄)) | ||
Theorem | dnibndlem9 35362* | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΅ + (1 / 2))) = ((ββ(π΄ + (1 / 2))) + 1)) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem10 35363 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β 1 β€ (π΅ β π΄)) | ||
Theorem | dnibndlem11 35364 | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβ((ββ(π΅ + (1 / 2))) β π΅)) β (absβ((ββ(π΄ + (1 / 2))) β π΄)))) β€ (1 / 2)) | ||
Theorem | dnibndlem12 35365* | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((ββ(π΄ + (1 / 2))) + 2) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibndlem13 35366* | Lemma for dnibnd 35367. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (ββ(π΄ + (1 / 2))) β€ (ββ(π΅ + (1 / 2)))) β β’ (π β (absβ((πβπ΅) β (πβπ΄))) β€ (absβ(π΅ β π΄))) | ||
Theorem | dnibnd 35367* | 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 35368 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) β β’ π β (ββcnββ) | ||
Theorem | knoppcnlem1 35369* | Lemma for knoppcn 35380. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) = ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄)))) | ||
Theorem | knoppcnlem2 35370* | Lemma for knoppcn 35380. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π΄))) β β) | ||
Theorem | knoppcnlem3 35371* | Lemma for knoppcn 35380. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((πΉβπ΄)βπ) β β) | ||
Theorem | knoppcnlem4 35372* | Lemma for knoppcn 35380. (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 35373* | Lemma for knoppcn 35380. (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 35374* | Lemma for knoppcn 35380. (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 35375* | Lemma for knoppcn 35380. (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 35376* | Lemma for knoppcn 35380. (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 35377* | Lemma for knoppcn 35380. (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 35378* | Lemma for knoppcn 35380. (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 35379* | Lemma for knoppcn 35380. (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 35380* | 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 35381* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) & β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β πΆ β β) & β’ (π β (absβπΆ) < 1) β β’ (π β (πβπ΄) β β) | ||
Theorem | unblimceq0lem 35382* | Lemma for unblimceq0 35383. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β βπ β β+ βπ β β+ βπ¦ β π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) | ||
Theorem | unblimceq0 35383* | If πΉ is unbounded near π΄ it has no limit at π΄. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) β β’ (π β (πΉ limβ π΄) = β ) | ||
Theorem | unbdqndv1 35384* | 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 35385 | Lemma for unbdqndv2 35387. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β+) & β’ (π β π· β 0) & β’ (π β (2 Β· πΈ) β€ (absβ((π΄ β π΅) / π·))) β β’ (π β ((πΈ Β· (absβπ·)) β€ (absβ(π΄ β πΆ)) β¨ (πΈ Β· (absβπ·)) β€ (absβ(π΅ β πΆ)))) | ||
Theorem | unbdqndv2lem2 35386* | Lemma for unbdqndv2 35387. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ πΊ = (π§ β (π β {π΄}) β¦ (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄))) & β’ π = if((π΅ Β· (π β π)) β€ (absβ((πΉβπ) β (πΉβπ΄))), π, π) & β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β π) & β’ (π β π΅ β β+) & β’ (π β π· β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β€ π΄) & β’ (π β π΄ β€ π) & β’ (π β (π β π) < π·) & β’ (π β (2 Β· π΅) β€ ((absβ((πΉβπ) β (πΉβπ))) / (π β π))) β β’ (π β (π β (π β {π΄}) β§ ((absβ(π β π΄)) < π· β§ π΅ β€ (absβ(πΊβπ))))) | ||
Theorem | unbdqndv2 35387* | Variant of unbdqndv1 35384 with the hypothesis that (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) is unbounded where π₯ β€ π΄ and π΄ β€ π¦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯ β€ π΄ β§ π΄ β€ π¦) β§ ((π¦ β π₯) < π β§ π₯ β π¦) β§ π β€ ((absβ((πΉβπ¦) β (πΉβπ₯))) / (π¦ β π₯)))) β β’ (π β Β¬ π΄ β dom (β D πΉ)) | ||
Theorem | knoppndvlem1 35388 | Lemma for knoppndv 35410. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β π½ β β€) & β’ (π β π β β€) β β’ (π β ((((2 Β· π)β-π½) / 2) Β· π) β β) | ||
Theorem | knoppndvlem2 35389 | Lemma for knoppndv 35410. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β π β β€) & β’ (π β π½ < πΌ) β β’ (π β (((2 Β· π)βπΌ) Β· ((((2 Β· π)β-π½) / 2) Β· π)) β β€) | ||
Theorem | knoppndvlem3 35390 | Lemma for knoppndv 35410. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
β’ (π β πΆ β (-1(,)1)) β β’ (π β (πΆ β β β§ (absβπΆ) < 1)) | ||
Theorem | knoppndvlem4 35391* | Lemma for knoppndv 35410. (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 35392* | Lemma for knoppndv 35410. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ π = (π₯ β β β¦ (absβ((ββ(π₯ + (1 / 2))) β π₯))) & β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π β β) β β’ (π β Ξ£π β (0...π½)((πΉβπ΄)βπ) β β) | ||
Theorem | knoppndvlem6 35393* | Lemma for knoppndv 35410. (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 35394* | Lemma for knoppndv 35410. (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 35395* | Lemma for knoppndv 35410. (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 35396* | Lemma for knoppndv 35410. (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 35397* | Lemma for knoppndv 35410. (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 35398* | Lemma for knoppndv 35410. (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 35399 | Lemma for knoppndv 35410. (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 35400 | Lemma for knoppndv 35410. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
β’ (π β πΆ β (-1(,)1)) & β’ (π β π β β) & β’ (π β 1 < (π Β· (absβπΆ))) β β’ (π β πΆ β 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |