P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ttcsnexg 37401	If the transitive closure of a class is a set, then its singleton transitive closure is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ {𝐴} ∈ V)
Theorem	ttcsnexbig 37402	The transitive closure of a set is a set iff its singleton transitive closure is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → (TC+ 𝐴 ∈ V ↔ TC+ {𝐴} ∈ V))
Theorem	ttcsntrsucg 37403	The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ Tr 𝐴) → TC+ {𝐴} = suc 𝐴)
Theorem	dfttc3gw 37404	If the transitive closure of 𝐴 is a set, then its value is (TC‘𝐴). If we assume Transitive Containment, then we can weaken the hypothesis to 𝐴 ∈ 𝑉, see dfttc3g 37415. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttcwf 37405	A set is well-founded iff its transitive closure is well-founded. As a corollary, the transitive closure of any well-founded set is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ TC+ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttcwf2 37406	If a transitive closure class is a set, then it is well-founded, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttcwf3 37407	The sets whose transitive closures are sets are precisely the well-founded sets, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ V ↔ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttc0elw 37408	If a transitive closure is a set, then it contains ∅ as an element iff it is nonempty, assuming Regularity. If we also assume Transitive Containment, then we can remove the TC+ 𝐴 ∈ 𝑉 hypothesis, see ttc0el 37416. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴))
Theorem	dfttc4lem1 37409*	Lemma for dfttc4 37411. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∩ 𝐶) ≠ ∅ ∧ ∀𝑧 ∈ 𝐶 ((𝑧 ∩ 𝐶) = ∅ → 𝑧 = 𝐷)) → 𝐷 ∈ 𝐵)
Theorem	dfttc4lem2 37410*	Lemma for dfttc4 37411. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    ⇒   ⊢ (𝐴 ⊆ 𝐵 ∧ Tr 𝐵)
Theorem	dfttc4 37411*	An alternative expression for the transitive closure of a class, assuming Regularity. A set 𝑥 is contained in the transitive closure of 𝐴 iff we can construct an ∈-chain from 𝑥 to an element of 𝐴. This weak definition is primarily useful for proving elttcirr 37412. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}
Theorem	elttcirr 37412	Irreflexivity of 𝐴 ∈ TC+ 𝐵 relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 37411 to construct a set in which 𝐴 is both ∈-minimal and not ∈-minimal. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ¬ 𝐴 ∈ TC+ 𝐴
Theorem	ttcexg 37413	The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V)
Theorem	ttcexbi 37414	A class is a set iff its transitive closure is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ V ↔ TC+ 𝐴 ∈ V)
Theorem	dfttc3g 37415	The transitive closure of a set 𝐴 is (TC‘𝐴), assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttc0el 37416	A transitive closure contains ∅ as an element iff it is nonempty, assuming Regularity and Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴)
21.18.4  Stronger axioms of regularity This section contains some experiments related to the Axiom of Regularity ax-reg 9590. As written, ax-reg 9590 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9643 / ax-inf2 9646; in particular, ax-reg 9590 alone is insufficient to assert that every set has a transitive closure (tz9.1 9734), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9590 requires a witness set to detect non-well-foundedness, but if all sets are hereditarily finite, then there may be no such witness set for an infinite descending ∈-chain. The question is, how can we strengthen ax-reg 9590 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9643 / ax-inf2 9646 (e.g., so that we can prove unir1 9825 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9590 into ax-regs 35851, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9590 and add ax-tco 37353, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9590 with a set-induction axiom mh-setind 37417. Fourth, we can take unir1 9825 as an axiom and derive everything from that. This list is far from exhaustive. In this section, we prove that these four listed principles are equivalent. We see that ax-regs 35851 implies the other three principles: ax-reg 9590 + ax-tco 37353 via axreg 35852 + tz9.1regs 35859, mh-setind 37417 via setindregs 35855, and unir1 9825 via unir1regs 35860. So we just have to show that ax-regs 35851 is implied by each of the other three. Some questions: When expanded to primitives, what is the shortest single axiom equivalent to these, over ZF minus ax-reg 9590 and ax-inf 9643 / ax-inf2 9646? One candidate is mh-setind 37417, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9590 + ax-tco 37353, expanded using mh-regprimbi 37426 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 37417*	Principle of set induction setind 9752, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 37418	A version of mh-setind 37417 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)
Theorem	regsfromregtco 37419*	Derivation of ax-regs 35851 from ax-reg 9590 + ax-tco 37353. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∃𝑦 𝑦 ∈ 𝑤 → ∃𝑦(𝑦 ∈ 𝑤 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤)))    &   ⊢ ∃𝑢(𝑣 ∈ 𝑢 ∧ ∀𝑡(𝑡 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢)))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromsetind 37420*	Derivation of ax-regs 35851 from mh-setind 37417. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) → ¬ 𝜑)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromunir1 37421*	Derivation of ax-regs 35851 from unir1 9825. (Contributed by Matthew House, 4-Mar-2026.)
⊢ ∪ (𝑅1 “ On) = V    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.18.5  Short axioms written in primitive symbols
Theorem	mh-inf3f1 37422	A variant of inf3 9640. If 𝐹 is a one-to-one function from 𝐴 into itself, and 𝐵 is an element outside its range, then (rec(𝐹, 𝐵) ↾ ω) is a one-to-one function yielding an infinite sequence of distinct elements from 𝐴. If 𝐴 is a set, we can use this theorem to prove ω ∈ V via f1dmex 7970. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)
Theorem	mh-inf3sn 37423*	Version of inf3 9640 for the set of Zermelo ordinals ∅, {∅}, {{∅}}, {{{∅}}}, etc., where the successor of 𝑦 is {𝑦}. Unlike inf3 9640, the proof does not require ax-reg 9590, since the singleton properties snnz 4733 and sneqr 4794 are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	mh-prprimbi 37424*	Shortest possible version of ax-pr 5390 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑧(𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧))
Theorem	mh-unprimbi 37425*	Shortest possible version of ax-un 7752 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	mh-regprimbi 37426*	Shortest possible version of ax-reg 9590 in primitive symbols. The equivalence is nontrivial, but it still follows solely from the axioms of predicate calculus. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ((∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) ↔ ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim1bi 37427*	Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf 9643 or ax-inf2 9646 from this axiom requires ax-ext 2732, ax-rep 5231, and ax-reg 9590, see inf3 9640 and inf0 9626. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim2bi 37428*	Shortest possible axiom of infinity in primitive symbols not requiring ax-reg 9590. Deriving ax-inf 9643 or ax-inf2 9646 from this axiom requires ax-ext 2732 and ax-rep 5231, see mh-inf3sn 37423 and inf0 9626. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑦 → ¬ (𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧)) → 𝑦 ∈ 𝑥))
Theorem	mh-infprim3bi 37429*	An axiom of infinity in primitive symbols not requiring ax-reg 9590. This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines 9590. It directly implies ax-inf 9643, but deriving ax-inf2 9646 requires ax-ext 2732 and ax-rep 5231, see mh-inf3sn 37423. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 {𝑧} ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ¬ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧 ¬ ¬ (𝑧 ∈ 𝑦 → ¬ ∀𝑦 ¬ ((𝑦 ∈ 𝑧 → 𝑦 = 𝑥) → ¬ (𝑦 = 𝑥 → 𝑦 ∈ 𝑧))))))
21.19  Mathbox for Asger C. Ipsen
21.19.1  Continuous nowhere differentiable functions
Theorem	dnival 37430*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))
Theorem	dnicld1 37431	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)
Theorem	dnicld2 37432*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ)
Theorem	dnif 37433	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇:ℝ⟶ℝ
Theorem	dnizeq0 37434*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) = 0)
Theorem	dnizphlfeqhlf 37435*	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 37436	Variant of rddif 15514. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))
Theorem	dnibndlem1 37437*	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆))
Theorem	dnibndlem2 37438*	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem3 37439	Lemma for dnibnd 37450. (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 37440	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem5 37441	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem6 37442	Lemma for dnibnd 37450. (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 37443	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem8 37444	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem9 37445*	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem10 37446	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴))
Theorem	dnibndlem11 37447	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2))
Theorem	dnibndlem12 37448*	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem13 37449*	Lemma for dnibnd 37450. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibnd 37450*	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 37451	The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇 ∈ (ℝ–cn→ℝ)
Theorem	knoppcnlem1 37452*	Lemma for knoppcn 37463. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))
Theorem	knoppcnlem2 37453*	Lemma for knoppcn 37463. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ)
Theorem	knoppcnlem3 37454*	Lemma for knoppcn 37463. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ)
Theorem	knoppcnlem4 37455*	Lemma for knoppcn 37463. (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 37456*	Lemma for knoppcn 37463. (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 37457*	Lemma for knoppcn 37463. (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 37458*	Lemma for knoppcn 37463. (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 37459*	Lemma for knoppcn 37463. (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 37460*	Lemma for knoppcn 37463. (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 37461*	Lemma for knoppcn 37463. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) Avoid ax-mulf 11284. (Revised by GG, 19-Apr-2025.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑀)) ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld)))
Theorem	knoppcnlem11 37462*	Lemma for knoppcn 37463. (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 37463*	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 37464*	Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐶) < 1)    ⇒   ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ)
Theorem	unblimceq0lem 37465*	Lemma for unblimceq0 37466. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦))))
Theorem	unblimceq0 37466*	If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅)
Theorem	unbdqndv1 37467*	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 37468	Lemma for unbdqndv2 37470. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    &   ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷)))    ⇒   ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))))
Theorem	unbdqndv2lem2 37469*	Lemma for unbdqndv2 37470. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))    &   ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑈 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝑉)    &   ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)    &   ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))    ⇒   ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
Theorem	unbdqndv2 37470*	Variant of unbdqndv1 37467 with the hypothesis that (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) is unbounded where 𝑥 ≤ 𝐴 and 𝐴 ≤ 𝑦. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦) ∧ ((𝑦 − 𝑥) < 𝑑 ∧ 𝑥 ≠ 𝑦) ∧ 𝑏 ≤ ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (𝑦 − 𝑥))))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ dom (ℝ D 𝐹))
Theorem	knoppndvlem1 37471	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀) ∈ ℝ)
Theorem	knoppndvlem2 37472	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 < 𝐼)    ⇒   ⊢ (𝜑 → (((2 · 𝑁)↑𝐼) · ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀)) ∈ ℤ)
Theorem	knoppndvlem3 37473	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1))
Theorem	knoppndvlem4 37474*	Lemma for knoppndv 37493. (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 37475*	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ)
Theorem	knoppndvlem6 37476*	Lemma for knoppndv 37493. (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 37477*	Lemma for knoppndv 37493. (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 37478*	Lemma for knoppndv 37493. (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 37479*	Lemma for knoppndv 37493. (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 37480*	Lemma for knoppndv 37493. (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 37481*	Lemma for knoppndv 37493. (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 37482	Lemma for knoppndv 37493. (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 37483	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → 𝐶 ≠ 0)
Theorem	knoppndvlem14 37484*	Lemma for knoppndv 37493. (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 37485*	Lemma for knoppndv 37493. (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 37486	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 19-Jul-2021.)
⊢ 𝐴 = ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀)    &   ⊢ 𝐵 = ((((2 · 𝑁)↑ -𝐽) / 2) · (𝑀 + 1))    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑ -𝐽) / 2))
Theorem	knoppndvlem17 37487*	Lemma for knoppndv 37493. (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 37488*	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 14-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑ -𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
Theorem	knoppndvlem19 37489*	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 17-Aug-2021.)
⊢ 𝐴 = ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑚)    &   ⊢ 𝐵 = ((((2 · 𝑁)↑ -𝐽) / 2) · (𝑚 + 1))    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵))
Theorem	knoppndvlem20 37490	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 18-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+)
Theorem	knoppndvlem21 37491*	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 18-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ 𝐺 = (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐻 ∈ ℝ)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    &   ⊢ (𝜑 → (((2 · 𝑁)↑ -𝐽) / 2) < 𝐷)    &   ⊢ (𝜑 → 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎))))
Theorem	knoppndvlem22 37492*	Lemma for knoppndv 37493. (Contributed by Asger C. Ipsen, 19-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐻 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎))))
Theorem	knoppndv 37493*	The continuous nowhere differentiable function 𝑊 ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, nowhere differentiable. (Contributed by Asger C. Ipsen, 19-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → dom (ℝ D 𝑊) = ∅)
Theorem	knoppf 37494*	Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑊:ℝ⟶ℝ)
Theorem	knoppcn2 37495*	Variant of knoppcn 37463 with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    ⇒   ⊢ (𝜑 → 𝑊 ∈ (ℝ–cn→ℝ))
Theorem	cnndvlem1 37496*	Lemma for cnndv 37498. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    ⇒   ⊢ (𝑊 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑊) = ∅)
Theorem	cnndvlem2 37497*	Lemma for cnndv 37498. (Contributed by Asger C. Ipsen, 26-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    ⇒   ⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅)
Theorem	cnndv 37498	There exists a continuous nowhere differentiable function. The result follows directly from knoppcn 37463 and knoppndv 37493. (Contributed by Asger C. Ipsen, 26-Aug-2021.)
⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅)
21.20  Mathbox for BJ In this mathbox, we try to respect the ordering of the sections of the main part. There are strengthenings of theorems of the main part, as well as work on reducing axiom dependencies.
21.20.1  Propositional calculus Miscellaneous utility theorems of propositional calculus.
21.20.1.1  Derived rules of inference In this section, we prove a few rules of inference derived from modus ponens ax-mp 5, and which do not depend on any other axioms.
Theorem	bj-mp2c 37499	A double modus ponens inference. Inference associated with mpd 16. (Contributed by BJ, 24-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜒
Theorem	bj-mp2d 37500	A double modus ponens inference. Inference associated with mpcom 39. (Contributed by BJ, 24-Sep-2019.)
⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜒