Home | Metamath
Proof Explorer Theorem List (p. 338 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnssi2 33701 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐵 ∈ ℕ → 𝜑) & ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓) | ||
Theorem | nnssi3 33702 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐶 ∈ ℕ → 𝜑) & ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓) | ||
Theorem | nndivsub 33703 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ)) | ||
Theorem | nndivlub 33704 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴)) | ||
Syntax | cgcdOLD 33705 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (𝐴, 𝐵) | ||
Definition | df-gcdOLD 33706* | 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 33707 | 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 33708* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) | ||
Theorem | dnicld1 33709 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) | ||
Theorem | dnicld2 33710* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ) | ||
Theorem | dnif 33711 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇:ℝ⟶ℝ | ||
Theorem | dnizeq0 33712* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) = 0) | ||
Theorem | dnizphlfeqhlf 33713* | 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 33714 | Variant of rddif 14690. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | ||
Theorem | dnibndlem1 33715* | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆)) | ||
Theorem | dnibndlem2 33716* | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem3 33717 | Lemma for dnibnd 33728. (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 33718 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem5 33719 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem6 33720 | Lemma for dnibnd 33728. (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 33721 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem8 33722 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem9 33723* | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1)) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem10 33724 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴)) | ||
Theorem | dnibndlem11 33725 | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2)) | ||
Theorem | dnibndlem12 33726* | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem13 33727* | Lemma for dnibnd 33728. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibnd 33728* | 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 33729 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇 ∈ (ℝ–cn→ℝ) | ||
Theorem | knoppcnlem1 33730* | Lemma for knoppcn 33741. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) | ||
Theorem | knoppcnlem2 33731* | Lemma for knoppcn 33741. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) | ||
Theorem | knoppcnlem3 33732* | Lemma for knoppcn 33741. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ) | ||
Theorem | knoppcnlem4 33733* | Lemma for knoppcn 33741. (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 33734* | Lemma for knoppcn 33741. (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 33735* | Lemma for knoppcn 33741. (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 33736* | Lemma for knoppcn 33741. (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 33737* | Lemma for knoppcn 33741. (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 33738* | Lemma for knoppcn 33741. (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 33739* | Lemma for knoppcn 33741. (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 33740* | Lemma for knoppcn 33741. (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 33741* | 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 33742* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐶) < 1) ⇒ ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ) | ||
Theorem | unblimceq0lem 33743* | Lemma for unblimceq0 33744. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦)))) | ||
Theorem | unblimceq0 33744* | If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅) | ||
Theorem | unbdqndv1 33745* | 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 33746 | Lemma for unbdqndv2 33748. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷))) ⇒ ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) | ||
Theorem | unbdqndv2lem2 33747* | Lemma for unbdqndv2 33748. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴))) & ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑈 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝑉) & ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷) & ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) ⇒ ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) | ||
Theorem | unbdqndv2 33748* | Variant of unbdqndv1 33745 with the hypothesis that (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) is unbounded where 𝑥 ≤ 𝐴 and 𝐴 ≤ 𝑦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦) ∧ ((𝑦 − 𝑥) < 𝑑 ∧ 𝑥 ≠ 𝑦) ∧ 𝑏 ≤ ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (𝑦 − 𝑥)))) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ dom (ℝ D 𝐹)) | ||
Theorem | knoppndvlem1 33749 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | ||
Theorem | knoppndvlem2 33750 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 < 𝐼) ⇒ ⊢ (𝜑 → (((2 · 𝑁)↑𝐼) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) ∈ ℤ) | ||
Theorem | knoppndvlem3 33751 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | ||
Theorem | knoppndvlem4 33752* | Lemma for knoppndv 33771. (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 33753* | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ) | ||
Theorem | knoppndvlem6 33754* | Lemma for knoppndv 33771. (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 33755* | Lemma for knoppndv 33771. (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 33756* | Lemma for knoppndv 33771. (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 33757* | Lemma for knoppndv 33771. (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 33758* | Lemma for knoppndv 33771. (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 33759* | Lemma for knoppndv 33771. (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 33760 | Lemma for knoppndv 33771. (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 33761 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → 𝐶 ≠ 0) | ||
Theorem | knoppndvlem14 33762* | Lemma for knoppndv 33771. (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 33763* | Lemma for knoppndv 33771. (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 33764 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 19-Jul-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) | ||
Theorem | knoppndvlem17 33765* | Lemma for knoppndv 33771. (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 33766* | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 14-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | ||
Theorem | knoppndvlem19 33767* | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 17-Aug-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵)) | ||
Theorem | knoppndvlem20 33768 | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 18-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+) | ||
Theorem | knoppndvlem21 33769* | Lemma for knoppndv 33771. (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 33770* | Lemma for knoppndv 33771. (Contributed by Asger C. Ipsen, 19-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎)))) | ||
Theorem | knoppndv 33771* | 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 33772* | Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝑊:ℝ⟶ℝ) | ||
Theorem | knoppcn2 33773* | Variant of knoppcn 33741 with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → 𝑊 ∈ (ℝ–cn→ℝ)) | ||
Theorem | cnndvlem1 33774* | Lemma for cnndv 33776. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ (𝑊 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑊) = ∅) | ||
Theorem | cnndvlem2 33775* | Lemma for cnndv 33776. (Contributed by Asger C. Ipsen, 26-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅) | ||
Theorem | cnndv 33776 | There exists a continuous nowhere differentiable function. The result follows directly from knoppcn 33741 and knoppndv 33771. (Contributed by Asger C. Ipsen, 26-Aug-2021.) |
⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅) | ||
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. | ||
Miscellaneous utility theorems of propositional calculus. | ||
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 33777 | A double modus ponens inference. Inference associated with mpd 15. (Contributed by BJ, 24-Sep-2019.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ 𝜒 | ||
Theorem | bj-mp2d 33778 | A double modus ponens inference. Inference associated with mpcom 38. (Contributed by BJ, 24-Sep-2019.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) ⇒ ⊢ 𝜒 | ||
In this section, we prove a syntactic theorem (bj-0 33779) asserting that some formula is well-formed. Then, we use this syntactic theorem to shorten the proof of a "usual" theorem (bj-1 33780) and explain in the comment of that theorem why this phenomenon is unusual. | ||
Theorem | bj-0 33779 | A syntactic theorem. See the section comment and the comment of bj-1 33780. 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 2106 and weq 1955. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
wff ((𝜑 → 𝜓) → 𝜒) | ||
Theorem | bj-1 33780 |
In this proof, the use of the syntactic theorem bj-0 33779
allows to reduce
the total length by one (non-essential) step. See also the section
comment and the comment of bj-0 33779. Since bj-0 33779
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 33779
as a theorem referencing
it). The full proof reads $= wph wps wch bj-0 id $. (while, without
using bj-0 33779, 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 1955 or wel 2106). 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 33780 is a special instance of id 22. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) | ||
Theorem | bj-a1k 33781 | Weakening of ax-1 6. This shortens the proofs of dfwe2 7484 (937>925), ordunisuc2 7547 (789>777), r111 9193 (558>545), smo11 7992 (1176>1164). (Contributed by BJ, 11-Aug-2020.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓))) | ||
Theorem | bj-nnclav 33782 | When ⊥ is substituted for 𝜓, this formula is the Clavius law with a doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | bj-jarrii 33783 | Inference associated with jarri 107. (Contributed by BJ, 29-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜒) & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
Theorem | bj-imim21 33784 | The propositional function (𝜒 → (. → 𝜃)) is decreasing. (Contributed by BJ, 19-Jul-2019.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃)))) | ||
Theorem | bj-imim21i 33785 | Inference associated with bj-imim21 33784. Its associated inference is syl5 34. (Contributed by BJ, 19-Jul-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃))) | ||
Theorem | bj-peircestab 33786 | Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any proposition (that is the interpretation when ⊥ is substitued for 𝜓). (Contributed by BJ, 30-Nov-2023.) (Proof modification is discouraged.) |
⊢ (((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓) | ||
Theorem | bj-stabpeirce 33787 | Over minimal implicational calculus, Peirce's law is implied by the (classical refutation equivalent of) the double negation of the stability of any proposition. (Contributed by BJ, 30-Nov-2023.) (Proof modification is discouraged.) |
⊢ ((((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓) → (((𝜓 → 𝜑) → 𝜓) → 𝜓)) | ||
Positive calculus is understood to be intuitionistic. | ||
Theorem | bj-syl66ib 33788 | A mixed syllogism inference derived from syl6ib 252. In addition to bj-dvelimdv1 34074, it can also shorten alexsubALTlem4 22588 (4821>4812), supsrlem 10522 (2868>2863). (Contributed by BJ, 20-Oct-2021.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜃 → 𝜏) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | bj-orim2 33789 | Proof of orim2 961 from the axiomatic definition of disjunction (olc 862, orc 861, jao 954) and minimal implicational calculus. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))) | ||
Theorem | bj-currypeirce 33790 | Curry's axiom curryax 887 (a non-intuitionistic positive statement sometimes called a paradox of material implication) implies Peirce's axiom peirce 203 over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the elimination axiom jao 954 via its inference form jaoi 851; the introduction axioms olc 862 and orc 861 are not needed). Note that this theorem shows that actually, the standard instance of curryax 887 implies the standard instance of peirce 203, which is not the case for the converse bj-peircecurry 33791. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | ||
Theorem | bj-peircecurry 33791 | Peirce's axiom peirce 203 implies Curry's axiom curryax 887 over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the introduction axioms olc 862 and orc 861; the elimination axiom jao 954 is not needed). See bj-currypeirce 33790 for the converse. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ∨ (𝜑 → 𝜓)) | ||
Theorem | bj-animbi 33792 | Conjunction in terms of implication and biconditional. Note that the proof is intuitionistic (use of ax-3 8 comes from the unusual definition of the biconditional in set.mm). (Contributed by BJ, 23-Sep-2023.) |
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ↔ (𝜑 → 𝜓))) | ||
Theorem | bj-currypara 33793 | Curry's paradox. Note that the proof is intuitionistic (use ax-3 8 comes from the unusual definition of the biconditional in set.mm). The paradox comes from the case where 𝜑 is the self-referential sentence "If this sentence is true, then 𝜓", so that one can prove everything. Therefore, a consistent system cannot allow the formation of such self-referential sentences. This has lead to the study of logics rejecting contraction pm2.43 56, such as affine logic and linear logic. (Contributed by BJ, 23-Sep-2023.) |
⊢ ((𝜑 ↔ (𝜑 → 𝜓)) → 𝜓) | ||
Theorem | bj-con2com 33794 | A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19-Mar-2020.) |
⊢ (𝜑 → ((𝜓 → ¬ 𝜑) → ¬ 𝜓)) | ||
Theorem | bj-con2comi 33795 | Inference associated with bj-con2com 33794. Its associated inference is mt2 201. TODO: when in the main part, add to mt2 201 that it is the inference associated with bj-con2comi 33795. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ((𝜓 → ¬ 𝜑) → ¬ 𝜓) | ||
Theorem | bj-pm2.01i 33796 | Inference associated with the weak Clavius law pm2.01 190. (Contributed by BJ, 30-Mar-2020.) |
⊢ (𝜑 → ¬ 𝜑) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bj-nimn 33797 | If a formula is true, then it does not imply its negation. (Contributed by BJ, 19-Mar-2020.) A shorter proof is possible using id 22 and jc 164, however, the present proof uses theorems that are more basic than jc 164. (Proof modification is discouraged.) |
⊢ (𝜑 → ¬ (𝜑 → ¬ 𝜑)) | ||
Theorem | bj-nimni 33798 | Inference associated with bj-nimn 33797. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → ¬ 𝜑) | ||
Theorem | bj-peircei 33799 | Inference associated with peirce 203. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | bj-looinvi 33800 | Inference associated with looinv 204. Its associated inference is bj-looinvii 33801. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) ⇒ ⊢ ((𝜓 → 𝜑) → 𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |