P. 376 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37501-37600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ttc0el 37501	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 9613. As written, ax-reg 9613 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9666 / ax-inf2 9669; in particular, ax-reg 9613 alone is insufficient to assert that every set has a transitive closure (tz9.1 9757), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9613 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 9613 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9666 / ax-inf2 9669 (e.g., so that we can prove unir1 9848 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9613 into ax-regs 35894, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9613 and add ax-tco 37438, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9613 with a set-induction axiom mh-setind 37502. Fourth, we can take unir1 9848 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 35894 implies the other three principles: ax-reg 9613 + ax-tco 37438 via axreg 35895 + tz9.1regs 35902, mh-setind 37502 via setindregs 35898, and unir1 9848 via unir1regs 35903. So we just have to show that ax-regs 35894 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 9613 and ax-inf 9666 / ax-inf2 9669? One candidate is mh-setind 37502, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9613 + ax-tco 37438, expanded using mh-regprimbi 37511 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 37502*	Principle of set induction setind 9775, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 37503	A version of mh-setind 37502 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)
Theorem	regsfromregtco 37504*	Derivation of ax-regs 35894 from ax-reg 9613 + ax-tco 37438. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∃𝑦 𝑦 ∈ 𝑤 → ∃𝑦(𝑦 ∈ 𝑤 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤)))    &   ⊢ ∃𝑢(𝑣 ∈ 𝑢 ∧ ∀𝑡(𝑡 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢)))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromsetind 37505*	Derivation of ax-regs 35894 from mh-setind 37502. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) → ¬ 𝜑)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromunir1 37506*	Derivation of ax-regs 35894 from unir1 9848. (Contributed by Matthew House, 4-Mar-2026.)
⊢ ∪ (𝑅1 “ On) = V    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.18.5  Short axioms written in primitive symbols
Theorem	mh-inf3f1 37507	A variant of inf3 9663. 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 7993. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (𝜑 → 𝐹:𝐴⟶1-1𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶1-1𝐴)
Theorem	mh-inf3sn 37508*	Version of inf3 9663 for the set of Zermelo ordinals ∅, {∅}, {{∅}}, {{{∅}}}, etc., where the successor of 𝑦 is {𝑦}. Unlike inf3 9663, the proof does not require ax-reg 9613, since the singleton properties snnz 4737 and sneqr 4798 are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	mh-prprimbi 37509*	Shortest possible version of ax-pr 5395 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑧(𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧))
Theorem	mh-unprimbi 37510*	Shortest possible version of ax-un 7775 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	mh-regprimbi 37511*	Shortest possible version of ax-reg 9613 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 37512*	Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf 9666 or ax-inf2 9669 from this axiom requires ax-ext 2735, ax-rep 5235, and ax-reg 9613, see inf3 9663 and inf0 9649. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim2bi 37513*	Shortest possible axiom of infinity in primitive symbols not requiring ax-reg 9613. Deriving ax-inf 9666 or ax-inf2 9669 from this axiom requires ax-ext 2735 and ax-rep 5235, see mh-inf3sn 37508 and inf0 9649. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑦 → ¬ (𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧)) → 𝑦 ∈ 𝑥))
Theorem	mh-infprim3bi 37514*	An axiom of infinity in primitive symbols not requiring ax-reg 9613. This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines 9613. It directly implies ax-inf 9666, but deriving ax-inf2 9669 requires ax-ext 2735 and ax-rep 5235, see mh-inf3sn 37508. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 {𝑧} ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ¬ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧 ¬ ¬ (𝑧 ∈ 𝑦 → ¬ ∀𝑦 ¬ ((𝑦 ∈ 𝑧 → 𝑦 = 𝑥) → ¬ (𝑦 = 𝑥 → 𝑦 ∈ 𝑧))))))
21.19  Mathbox for Asger C. Ipsen
21.19.1  Continuous nowhere differentiable functions
Theorem	dnival 37515*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))
Theorem	dnicld1 37516	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)
Theorem	dnicld2 37517*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ)
Theorem	dnif 37518	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇:ℝ⟶ℝ
Theorem	dnizeq0 37519*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) = 0)
Theorem	dnizphlfeqhlf 37520*	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 37521	Variant of rddif 15537. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))
Theorem	dnibndlem1 37522*	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆))
Theorem	dnibndlem2 37523*	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem3 37524	Lemma for dnibnd 37535. (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 37525	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem5 37526	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem6 37527	Lemma for dnibnd 37535. (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 37528	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem8 37529	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem9 37530*	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem10 37531	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴))
Theorem	dnibndlem11 37532	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2))
Theorem	dnibndlem12 37533*	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem13 37534*	Lemma for dnibnd 37535. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibnd 37535*	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 37536	The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇 ∈ (ℝ–cn→ℝ)
Theorem	knoppcnlem1 37537*	Lemma for knoppcn 37548. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))
Theorem	knoppcnlem2 37538*	Lemma for knoppcn 37548. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ)
Theorem	knoppcnlem3 37539*	Lemma for knoppcn 37548. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ)
Theorem	knoppcnlem4 37540*	Lemma for knoppcn 37548. (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 37541*	Lemma for knoppcn 37548. (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 37542*	Lemma for knoppcn 37548. (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 37543*	Lemma for knoppcn 37548. (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 37544*	Lemma for knoppcn 37548. (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 37545*	Lemma for knoppcn 37548. (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 37546*	Lemma for knoppcn 37548. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) Avoid ax-mulf 11307. (Revised by GG, 19-Apr-2025.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑀)) ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld)))
Theorem	knoppcnlem11 37547*	Lemma for knoppcn 37548. (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 37548*	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 37549*	Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐶) < 1)    ⇒   ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ)
Theorem	unblimceq0lem 37550*	Lemma for unblimceq0 37551. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦))))
Theorem	unblimceq0 37551*	If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅)
Theorem	unbdqndv1 37552*	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 37553	Lemma for unbdqndv2 37555. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    &   ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷)))    ⇒   ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))))
Theorem	unbdqndv2lem2 37554*	Lemma for unbdqndv2 37555. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))    &   ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑈 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝑉)    &   ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)    &   ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))    ⇒   ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
Theorem	unbdqndv2 37555*	Variant of unbdqndv1 37552 with the hypothesis that (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) is unbounded where 𝑥 ≤ 𝐴 and 𝐴 ≤ 𝑦. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦) ∧ ((𝑦 − 𝑥) < 𝑑 ∧ 𝑥 ≠ 𝑦) ∧ 𝑏 ≤ ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (𝑦 − 𝑥))))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ dom (ℝ D 𝐹))
Theorem	knoppndvlem1 37556	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀) ∈ ℝ)
Theorem	knoppndvlem2 37557	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 < 𝐼)    ⇒   ⊢ (𝜑 → (((2 · 𝑁)↑𝐼) · ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀)) ∈ ℤ)
Theorem	knoppndvlem3 37558	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1))
Theorem	knoppndvlem4 37559*	Lemma for knoppndv 37578. (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 37560*	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ)
Theorem	knoppndvlem6 37561*	Lemma for knoppndv 37578. (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 37562*	Lemma for knoppndv 37578. (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 37563*	Lemma for knoppndv 37578. (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 37564*	Lemma for knoppndv 37578. (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 37565*	Lemma for knoppndv 37578. (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 37566*	Lemma for knoppndv 37578. (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 37567	Lemma for knoppndv 37578. (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 37568	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → 𝐶 ≠ 0)
Theorem	knoppndvlem14 37569*	Lemma for knoppndv 37578. (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 37570*	Lemma for knoppndv 37578. (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 37571	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 19-Jul-2021.)
⊢ 𝐴 = ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑀)    &   ⊢ 𝐵 = ((((2 · 𝑁)↑ -𝐽) / 2) · (𝑀 + 1))    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑ -𝐽) / 2))
Theorem	knoppndvlem17 37572*	Lemma for knoppndv 37578. (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 37573*	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 14-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑ -𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
Theorem	knoppndvlem19 37574*	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 17-Aug-2021.)
⊢ 𝐴 = ((((2 · 𝑁)↑ -𝐽) / 2) · 𝑚)    &   ⊢ 𝐵 = ((((2 · 𝑁)↑ -𝐽) / 2) · (𝑚 + 1))    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵))
Theorem	knoppndvlem20 37575	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 18-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+)
Theorem	knoppndvlem21 37576*	Lemma for knoppndv 37578. (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 37577*	Lemma for knoppndv 37578. (Contributed by Asger C. Ipsen, 19-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐻 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎))))
Theorem	knoppndv 37578*	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 37579*	Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑊:ℝ⟶ℝ)
Theorem	knoppcn2 37580*	Variant of knoppcn 37548 with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ( -1(,)1))    ⇒   ⊢ (𝜑 → 𝑊 ∈ (ℝ–cn→ℝ))
Theorem	cnndvlem1 37581*	Lemma for cnndv 37583. (Contributed by Asger C. Ipsen, 25-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    ⇒   ⊢ (𝑊 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑊) = ∅)
Theorem	cnndvlem2 37582*	Lemma for cnndv 37583. (Contributed by Asger C. Ipsen, 26-Aug-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦)))))    &   ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))    ⇒   ⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅)
Theorem	cnndv 37583	There exists a continuous nowhere differentiable function. The result follows directly from knoppcn 37548 and knoppndv 37578. (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 37584	A double modus ponens inference. Inference associated with mpd 16. (Contributed by BJ, 24-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜒
Theorem	bj-mp2d 37585	A double modus ponens inference. Inference associated with mpcom 39. (Contributed by BJ, 24-Sep-2019.)
⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜒
21.20.1.2  A syntactic theorem In this section, we prove a syntactic theorem (bj-0 37586) asserting that some formula is well-formed. Then, we use this syntactic theorem to shorten the proof of a "usual" theorem (bj-1 37587) and explain in the comment of that theorem why this phenomenon is unusual.
Theorem	bj-0 37586	A syntactic theorem. See the section comment and the comment of bj-1 37587. The full proof (that is, with the syntactic, non-essential steps) does not appear on this webpage. It has five steps and reads $= wph wps wi wch wi $. The only other syntactic theorems in the main part of set.mm are wel 2148 and weq 1997. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
wff ((𝜑 → 𝜓) → 𝜒)
Theorem	bj-1 37587	In this proof, the use of the syntactic theorem bj-0 37586 allows to reduce the total length by one (non-essential) step. See also the section comment and the comment of bj-0 37586. Since bj-0 37586 is used in a non-essential step, this use does not appear on this webpage (but the present theorem appears on the webpage for bj-0 37586 as a theorem referencing it). The full proof reads $= wph wps wch bj-0 id $. (while, without using bj-0 37586, it would read $= wph wps wi wch wi id $.). Now we explain why syntactic theorems are not useful in set.mm. Suppose that the syntactic theorem thm-0 proves that PHI is a well-formed formula, and that thm-0 is used to shorten the proof of thm-1. Assume that PHI does have proper non-atomic subformulas (which is not the case of the formula proved by weq 1997 or wel 2148). Then, the proof of thm-1 does not construct all the proper non-atomic subformulas of PHI (if it did, then using thm-0 would not shorten it). Therefore, thm-1 is a special instance of a more general theorem with essentially the same proof. In the present case, bj-1 37587 is a special instance of id 23. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))
21.20.1.3  Minimal implicational calculus Minimal implicational calculus, or intuitionistic implicational calculus, is the logical calculus with axioms ax-mp 5, ax-1 6, ax-2 7.
Theorem	bj-poni 37588	Inference associated with "pon", pm2.27 43. Its associated inference is ax-mp 5. (Contributed by BJ, 30-Jul-2024.)
⊢ 𝜑    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜓)
Theorem	bj-nnclav 37589	When ⊥ is substituted for 𝜓, this formula is the Clavius law with a doubly negated consequent, which is therefore a minimalistic tautology. Notice the non-intuitionistic proof from peirce 205 and pm2.27 43 chained using syl 18. (Contributed by BJ, 4-Dec-2023.)
⊢ (((𝜑 → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓))
Theorem	bj-nnclavi 37590	Inference associated with bj-nnclav 37589. Its associated inference is an instance of syl 18. Notice the non-intuitionistic proof from bj-peircei 37612 and bj-poni 37588. (Contributed by BJ, 30-Jul-2024.)
⊢ ((𝜑 → 𝜓) → 𝜑)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜓)
Theorem	bj-nnclavc 37591	Commuted form of bj-nnclav 37589. Notice the non-intuitionistic proof from bj-peircei 37612 and imim1i 64. (Contributed by BJ, 30-Jul-2024.) A proof which is shorter when compressed uses embantd 60. (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜑) → 𝜓))
Theorem	bj-nnclavci 37592	Inference associated with bj-nnclavc 37591. Its associated inference is an instance of syl 18. Notice the non-intuitionistic proof from peirce 205 and syl 18. (Contributed by BJ, 30-Jul-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜓)
Theorem	bj-jarrii 37593	Inference associated with jarri 108. Contrary to it, it does not require ax-2 7, but only ax-mp 5 and ax-1 6. (Contributed by BJ, 29-Mar-2020.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → 𝜒)    &   ⊢ 𝜓    ⇒   ⊢ 𝜒
Theorem	bj-imim21 37594	The propositional function (𝜑 → (. → 𝜓)) is decreasing. (Contributed by BJ, 19-Jul-2019.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃))))
Theorem	bj-imim21i 37595	The propositional function (𝜑 → (. → 𝜓)) is decreasing. Its associated inference is syl5 35. (Contributed by BJ, 19-Jul-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃)))
Theorem	bj-imim11 37596	The propositional function ((. → 𝜑) → 𝜓) is increasing. (Contributed by BJ, 3-Apr-2026.)
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜒) → 𝜃) → ((𝜓 → 𝜒) → 𝜃)))
Theorem	bj-imim11i 37597	The propositional function ((. → 𝜑) → 𝜓) is increasing. Its associated inference is wl-syls2 38633. (Contributed by BJ, 3-Apr-2026.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜑 → 𝜒) → 𝜃) → ((𝜓 → 𝜒) → 𝜃))
Theorem	bj-peircestab 37598	Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any formula (that is the interpretation when ⊥ is substituted for 𝜓 and for 𝜒). Therefore, the double negation of the stability of any formula is provable in classical refutability calculus. It is also provable in intuitionistic calculus (see iset.mm/bj-nnst) but it is not provable in minimal calculus (see bj-stabpeirce 37599). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 205. (Proof modification is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)
Theorem	bj-stabpeirce 37599	This minimal implicational calculus tautology is used in the following argument: When 𝜑, 𝜓, 𝜒, 𝜃, 𝜏 are replaced respectively by (𝜑 → ⊥), ⊥, 𝜑, ⊥, ⊥, the antecedent becomes ¬ ¬ (¬ ¬ 𝜑 → 𝜑), that is, the double negation of the stability of 𝜑. If that statement were provable in minimal calculus, then, since ⊥ plays no particular role in minimal calculus, also the statement with 𝜓 in place of ⊥ would be provable. The corresponding consequent is (((𝜓 → 𝜑) → 𝜓) → 𝜓), that is, the non-intuitionistic Peirce law. Therefore, the double negation of the stability of any formula is not provable in minimal calculus. However, it is provable both in intuitionistic calculus (see iset.mm/bj-nnst) and in classical refutability calculus (see bj-peircestab 37598). (Contributed by BJ, 30-Nov-2023.) (Revised by BJ, 30-Jul-2024.) (Proof modification is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜃) → 𝜏) → (((𝜓 → 𝜒) → 𝜃) → 𝜏))
21.20.1.4  Positive calculus Positive calculus is understood to be intuitionistic. Its primitive connectives are implication, equivalence, conjunction, and disjunction. Due to the current axiomatization of set.mm, axiom ax-3 8, which does not belong to positive calculus, may appear as a dependency of some theorems in this section.
Theorem	bj-bisimpl 37600	Implication from equivalence with a conjunct. Its associated inference is simplbi 502. (Contributed by BJ, 20-Mar-2026.)
⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓))