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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnssi3 33701 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐶 ∈ ℕ → 𝜑) & ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓) | ||
Theorem | nndivsub 33702 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ)) | ||
Theorem | nndivlub 33703 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴)) | ||
Syntax | cgcdOLD 33704 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (𝐴, 𝐵) | ||
Definition | df-gcdOLD 33705* | 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 33706 | 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 33707* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) | ||
Theorem | dnicld1 33708 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) | ||
Theorem | dnicld2 33709* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ) | ||
Theorem | dnif 33710 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇:ℝ⟶ℝ | ||
Theorem | dnizeq0 33711* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) = 0) | ||
Theorem | dnizphlfeqhlf 33712* | 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 33713 | Variant of rddif 14688. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | ||
Theorem | dnibndlem1 33714* | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆)) | ||
Theorem | dnibndlem2 33715* | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem3 33716 | Lemma for dnibnd 33727. (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 33717 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem5 33718 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem6 33719 | Lemma for dnibnd 33727. (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 33720 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem8 33721 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem9 33722* | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1)) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem10 33723 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴)) | ||
Theorem | dnibndlem11 33724 | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2)) | ||
Theorem | dnibndlem12 33725* | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem13 33726* | Lemma for dnibnd 33727. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibnd 33727* | 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 33728 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇 ∈ (ℝ–cn→ℝ) | ||
Theorem | knoppcnlem1 33729* | Lemma for knoppcn 33740. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) | ||
Theorem | knoppcnlem2 33730* | Lemma for knoppcn 33740. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) | ||
Theorem | knoppcnlem3 33731* | Lemma for knoppcn 33740. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ) | ||
Theorem | knoppcnlem4 33732* | Lemma for knoppcn 33740. (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 33733* | Lemma for knoppcn 33740. (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 33734* | Lemma for knoppcn 33740. (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 33735* | Lemma for knoppcn 33740. (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 33736* | Lemma for knoppcn 33740. (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 33737* | Lemma for knoppcn 33740. (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 33738* | Lemma for knoppcn 33740. (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 33739* | Lemma for knoppcn 33740. (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 33740* | 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 33741* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐶) < 1) ⇒ ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ) | ||
Theorem | unblimceq0lem 33742* | Lemma for unblimceq0 33743. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦)))) | ||
Theorem | unblimceq0 33743* | If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅) | ||
Theorem | unbdqndv1 33744* | 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 33745 | Lemma for unbdqndv2 33747. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷))) ⇒ ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) | ||
Theorem | unbdqndv2lem2 33746* | Lemma for unbdqndv2 33747. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴))) & ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑈 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝑉) & ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷) & ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) ⇒ ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) | ||
Theorem | unbdqndv2 33747* | Variant of unbdqndv1 33744 with the hypothesis that (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) is unbounded where 𝑥 ≤ 𝐴 and 𝐴 ≤ 𝑦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦) ∧ ((𝑦 − 𝑥) < 𝑑 ∧ 𝑥 ≠ 𝑦) ∧ 𝑏 ≤ ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (𝑦 − 𝑥)))) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ dom (ℝ D 𝐹)) | ||
Theorem | knoppndvlem1 33748 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | ||
Theorem | knoppndvlem2 33749 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 < 𝐼) ⇒ ⊢ (𝜑 → (((2 · 𝑁)↑𝐼) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) ∈ ℤ) | ||
Theorem | knoppndvlem3 33750 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | ||
Theorem | knoppndvlem4 33751* | Lemma for knoppndv 33770. (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 33752* | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ) | ||
Theorem | knoppndvlem6 33753* | Lemma for knoppndv 33770. (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 33754* | Lemma for knoppndv 33770. (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 33755* | Lemma for knoppndv 33770. (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 33756* | Lemma for knoppndv 33770. (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 33757* | Lemma for knoppndv 33770. (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 33758* | Lemma for knoppndv 33770. (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 33759 | Lemma for knoppndv 33770. (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 33760 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → 𝐶 ≠ 0) | ||
Theorem | knoppndvlem14 33761* | Lemma for knoppndv 33770. (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 33762* | Lemma for knoppndv 33770. (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 33763 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 19-Jul-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) | ||
Theorem | knoppndvlem17 33764* | Lemma for knoppndv 33770. (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 33765* | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 14-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | ||
Theorem | knoppndvlem19 33766* | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 17-Aug-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵)) | ||
Theorem | knoppndvlem20 33767 | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 18-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+) | ||
Theorem | knoppndvlem21 33768* | Lemma for knoppndv 33770. (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 33769* | Lemma for knoppndv 33770. (Contributed by Asger C. Ipsen, 19-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎)))) | ||
Theorem | knoppndv 33770* | 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 33771* | Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝑊:ℝ⟶ℝ) | ||
Theorem | knoppcn2 33772* | Variant of knoppcn 33740 with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → 𝑊 ∈ (ℝ–cn→ℝ)) | ||
Theorem | cnndvlem1 33773* | Lemma for cnndv 33775. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ (𝑊 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑊) = ∅) | ||
Theorem | cnndvlem2 33774* | Lemma for cnndv 33775. (Contributed by Asger C. Ipsen, 26-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅) | ||
Theorem | cnndv 33775 | There exists a continuous nowhere differentiable function. The result follows directly from knoppcn 33740 and knoppndv 33770. (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 33776 | A double modus ponens inference. Inference associated with mpd 15. (Contributed by BJ, 24-Sep-2019.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ 𝜒 | ||
Theorem | bj-mp2d 33777 | 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 33778) asserting that some formula is well-formed. Then, we use this syntactic theorem to shorten the proof of a "usual" theorem (bj-1 33779) and explain in the comment of that theorem why this phenomenon is unusual. | ||
Theorem | bj-0 33778 | A syntactic theorem. See the section comment and the comment of bj-1 33779. 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 33779 |
In this proof, the use of the syntactic theorem bj-0 33778
allows to reduce
the total length by one (non-essential) step. See also the section
comment and the comment of bj-0 33778. Since bj-0 33778
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 33778
as a theorem referencing
it). The full proof reads $= wph wps wch bj-0 id $. (while, without
using bj-0 33778, 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 33779 is a special instance of id 22. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) | ||
Theorem | bj-a1k 33780 | Weakening of ax-1 6. This shortens the proofs of dfwe2 7485 (937>925), ordunisuc2 7548 (789>777), r111 9192 (558>545), smo11 7990 (1176>1164). (Contributed by BJ, 11-Aug-2020.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓))) | ||
Theorem | bj-nnclav 33781 | When ⊥ is substituted for 𝜓, this formula is the Clavius law with a doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | bj-jarrii 33782 | Inference associated with jarri 107. (Contributed by BJ, 29-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜒) & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
Theorem | bj-imim21 33783 | The propositional function (𝜒 → (. → 𝜃)) is decreasing. (Contributed by BJ, 19-Jul-2019.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃)))) | ||
Theorem | bj-imim21i 33784 | Inference associated with bj-imim21 33783. Its associated inference is syl5 34. (Contributed by BJ, 19-Jul-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃))) | ||
Theorem | bj-peircestab 33785 | 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 33786 | 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 33787 | A mixed syllogism inference derived from syl6ib 252. In addition to bj-dvelimdv1 34073, it can also shorten alexsubALTlem4 22586 (4821>4812), supsrlem 10521 (2868>2863). (Contributed by BJ, 20-Oct-2021.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜃 → 𝜏) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | bj-orim2 33788 | 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 33789 | 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 33790. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | ||
Theorem | bj-peircecurry 33790 | 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 33789 for the converse. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ∨ (𝜑 → 𝜓)) | ||
Theorem | bj-animbi 33791 | 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 33792 | 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 33793 | A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19-Mar-2020.) |
⊢ (𝜑 → ((𝜓 → ¬ 𝜑) → ¬ 𝜓)) | ||
Theorem | bj-con2comi 33794 | Inference associated with bj-con2com 33793. 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 33794. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ((𝜓 → ¬ 𝜑) → ¬ 𝜓) | ||
Theorem | bj-pm2.01i 33795 | Inference associated with the weak Clavius law pm2.01 190. (Contributed by BJ, 30-Mar-2020.) |
⊢ (𝜑 → ¬ 𝜑) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bj-nimn 33796 | 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 33797 | Inference associated with bj-nimn 33796. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → ¬ 𝜑) | ||
Theorem | bj-peircei 33798 | Inference associated with peirce 203. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | bj-looinvi 33799 | Inference associated with looinv 204. Its associated inference is bj-looinvii 33800. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) ⇒ ⊢ ((𝜓 → 𝜑) → 𝜑) | ||
Theorem | bj-looinvii 33800 | Inference associated with bj-looinvi 33799. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |