![]() |
Metamath
Proof Explorer Theorem List (p. 359 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30606) |
![]() (30607-32129) |
![]() (32130-48006) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-gcdOLD 35801* | 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 35802 | 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 35803* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) | ||
Theorem | dnicld1 35804 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) | ||
Theorem | dnicld2 35805* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ) | ||
Theorem | dnif 35806 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇:ℝ⟶ℝ | ||
Theorem | dnizeq0 35807* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) = 0) | ||
Theorem | dnizphlfeqhlf 35808* | 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 35809 | Variant of rddif 15283. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | ||
Theorem | dnibndlem1 35810* | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆)) | ||
Theorem | dnibndlem2 35811* | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem3 35812 | Lemma for dnibnd 35823. (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 35813 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem5 35814 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem6 35815 | Lemma for dnibnd 35823. (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 35816 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem8 35817 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem9 35818* | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1)) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem10 35819 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴)) | ||
Theorem | dnibndlem11 35820 | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2)) | ||
Theorem | dnibndlem12 35821* | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem13 35822* | Lemma for dnibnd 35823. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibnd 35823* | 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 35824 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇 ∈ (ℝ–cn→ℝ) | ||
Theorem | knoppcnlem1 35825* | Lemma for knoppcn 35836. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) | ||
Theorem | knoppcnlem2 35826* | Lemma for knoppcn 35836. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) | ||
Theorem | knoppcnlem3 35827* | Lemma for knoppcn 35836. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ) | ||
Theorem | knoppcnlem4 35828* | Lemma for knoppcn 35836. (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 35829* | Lemma for knoppcn 35836. (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 35830* | Lemma for knoppcn 35836. (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 35831* | Lemma for knoppcn 35836. (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 35832* | Lemma for knoppcn 35836. (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 35833* | Lemma for knoppcn 35836. (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 35834* | Lemma for knoppcn 35836. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) Avoid ax-mulf 11185. (Revised by GG, 19-Apr-2025.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑀)) ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld))) | ||
Theorem | knoppcnlem11 35835* | Lemma for knoppcn 35836. (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 35836* | 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 35837* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐶) < 1) ⇒ ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ) | ||
Theorem | unblimceq0lem 35838* | Lemma for unblimceq0 35839. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦)))) | ||
Theorem | unblimceq0 35839* | If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅) | ||
Theorem | unbdqndv1 35840* | 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 35841 | Lemma for unbdqndv2 35843. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷))) ⇒ ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) | ||
Theorem | unbdqndv2lem2 35842* | Lemma for unbdqndv2 35843. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴))) & ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑈 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝑉) & ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷) & ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) ⇒ ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) | ||
Theorem | unbdqndv2 35843* | Variant of unbdqndv1 35840 with the hypothesis that (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) is unbounded where 𝑥 ≤ 𝐴 and 𝐴 ≤ 𝑦. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦) ∧ ((𝑦 − 𝑥) < 𝑑 ∧ 𝑥 ≠ 𝑦) ∧ 𝑏 ≤ ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (𝑦 − 𝑥)))) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ dom (ℝ D 𝐹)) | ||
Theorem | knoppndvlem1 35844 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | ||
Theorem | knoppndvlem2 35845 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 < 𝐼) ⇒ ⊢ (𝜑 → (((2 · 𝑁)↑𝐼) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) ∈ ℤ) | ||
Theorem | knoppndvlem3 35846 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | ||
Theorem | knoppndvlem4 35847* | Lemma for knoppndv 35866. (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 35848* | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ) | ||
Theorem | knoppndvlem6 35849* | Lemma for knoppndv 35866. (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 35850* | Lemma for knoppndv 35866. (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 35851* | Lemma for knoppndv 35866. (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 35852* | Lemma for knoppndv 35866. (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 35853* | Lemma for knoppndv 35866. (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 35854* | Lemma for knoppndv 35866. (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 35855 | Lemma for knoppndv 35866. (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 35856 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → 𝐶 ≠ 0) | ||
Theorem | knoppndvlem14 35857* | Lemma for knoppndv 35866. (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 35858* | Lemma for knoppndv 35866. (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 35859 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 19-Jul-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) | ||
Theorem | knoppndvlem17 35860* | Lemma for knoppndv 35866. (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 35861* | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 14-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | ||
Theorem | knoppndvlem19 35862* | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 17-Aug-2021.) |
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚) & ⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1)) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵)) | ||
Theorem | knoppndvlem20 35863 | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 18-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+) | ||
Theorem | knoppndvlem21 35864* | Lemma for knoppndv 35866. (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 35865* | Lemma for knoppndv 35866. (Contributed by Asger C. Ipsen, 19-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐻 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ((𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏) ∧ ((𝑏 − 𝑎) < 𝐷 ∧ 𝑎 ≠ 𝑏) ∧ 𝐸 ≤ ((abs‘((𝑊‘𝑏) − (𝑊‘𝑎))) / (𝑏 − 𝑎)))) | ||
Theorem | knoppndv 35866* | 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 35867* | Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝑊:ℝ⟶ℝ) | ||
Theorem | knoppcn2 35868* | Variant of knoppcn 35836 with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) ⇒ ⊢ (𝜑 → 𝑊 ∈ (ℝ–cn→ℝ)) | ||
Theorem | cnndvlem1 35869* | Lemma for cnndv 35871. (Contributed by Asger C. Ipsen, 25-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ (𝑊 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑊) = ∅) | ||
Theorem | cnndvlem2 35870* | Lemma for cnndv 35871. (Contributed by Asger C. Ipsen, 26-Aug-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ (((1 / 2)↑𝑛) · (𝑇‘(((2 · 3)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) ⇒ ⊢ ∃𝑓(𝑓 ∈ (ℝ–cn→ℝ) ∧ dom (ℝ D 𝑓) = ∅) | ||
Theorem | cnndv 35871 | There exists a continuous nowhere differentiable function. The result follows directly from knoppcn 35836 and knoppndv 35866. (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 35872 | A double modus ponens inference. Inference associated with mpd 15. (Contributed by BJ, 24-Sep-2019.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ 𝜒 | ||
Theorem | bj-mp2d 35873 | 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 35874) asserting that some formula is well-formed. Then, we use this syntactic theorem to shorten the proof of a "usual" theorem (bj-1 35875) and explain in the comment of that theorem why this phenomenon is unusual. | ||
Theorem | bj-0 35874 | A syntactic theorem. See the section comment and the comment of bj-1 35875. 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 2099 and weq 1958. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
wff ((𝜑 → 𝜓) → 𝜒) | ||
Theorem | bj-1 35875 |
In this proof, the use of the syntactic theorem bj-0 35874
allows to reduce
the total length by one (non-essential) step. See also the section
comment and the comment of bj-0 35874. Since bj-0 35874
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 35874
as a theorem referencing
it). The full proof reads $= wph wps wch bj-0 id $. (while, without
using bj-0 35874, 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 1958 or wel 2099). 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 35875 is a special instance of id 22. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) | ||
Theorem | bj-a1k 35876 | Weakening of ax-1 6. As a consequence, its associated inference is an instance (where we allow extra hypotheses) of ax-1 6. Its commuted form is 2a1 28 (but bj-a1k 35876 does not require ax-2 7). This shortens the proofs of dfwe2 7754 (937>925), ordunisuc2 7826 (789>777), r111 9765 (558>545), smo11 8359 (1176>1164). (Contributed by BJ, 11-Aug-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓))) | ||
Theorem | bj-poni 35877 | Inference associated with "pon", pm2.27 42. Its associated inference is ax-mp 5. (Contributed by BJ, 30-Jul-2024.) |
⊢ 𝜑 ⇒ ⊢ ((𝜑 → 𝜓) → 𝜓) | ||
Theorem | bj-nnclav 35878 | 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 201 and pm2.27 42 chained using syl 17. (Contributed by BJ, 4-Dec-2023.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | bj-nnclavi 35879 | Inference associated with bj-nnclav 35878. Its associated inference is an instance of syl 17. Notice the non-intuitionistic proof from bj-peircei 35898 and bj-poni 35877. (Contributed by BJ, 30-Jul-2024.) |
⊢ ((𝜑 → 𝜓) → 𝜑) ⇒ ⊢ ((𝜑 → 𝜓) → 𝜓) | ||
Theorem | bj-nnclavc 35880 | Commuted form of bj-nnclav 35878. Notice the non-intuitionistic proof from bj-peircei 35898 and imim1i 63. (Contributed by BJ, 30-Jul-2024.) A proof which is shorter when compressed uses embantd 59. (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜑) → 𝜓)) | ||
Theorem | bj-nnclavci 35881 | Inference associated with bj-nnclavc 35880. Its associated inference is an instance of syl 17. Notice the non-intuitionistic proof from peirce 201 and syl 17. (Contributed by BJ, 30-Jul-2024.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜓) | ||
Theorem | bj-jarrii 35882 | Inference associated with jarri 107. 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 35883 | The propositional function (𝜒 → (. → 𝜃)) is decreasing. (Contributed by BJ, 19-Jul-2019.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃)))) | ||
Theorem | bj-imim21i 35884 | Inference associated with bj-imim21 35883. Its associated inference is syl5 34. (Contributed by BJ, 19-Jul-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 → (𝜓 → 𝜃)) → (𝜒 → (𝜑 → 𝜃))) | ||
Theorem | bj-peircestab 35885 | 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 35886). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 201. (Proof modification is discouraged.) |
⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒) | ||
Theorem | bj-stabpeirce 35886 | 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 35885). (Contributed by BJ, 30-Nov-2023.) (Revised by BJ, 30-Jul-2024.) (Proof modification is discouraged.) |
⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜃) → 𝜏) → (((𝜓 → 𝜒) → 𝜃) → 𝜏)) | ||
Positive calculus is understood to be intuitionistic. | ||
Theorem | bj-syl66ib 35887 | A mixed syllogism inference derived from imbitrdi 250. In addition to bj-dvelimdv1 36187, it can also shorten alexsubALTlem4 23875 (4821>4812), supsrlem 11101 (2868>2863). (Contributed by BJ, 20-Oct-2021.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜃 → 𝜏) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | bj-orim2 35888 | Proof of orim2 964 from the axiomatic definition of disjunction (olc 865, orc 864, jao 957) and minimal implicational calculus. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))) | ||
Theorem | bj-currypeirce 35889 | Curry's axiom curryax 890 (a non-intuitionistic positive statement sometimes called a paradox of material implication) implies Peirce's axiom peirce 201 over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the elimination axiom jao 957 via its inference form jaoi 854; the introduction axioms olc 865 and orc 864 are not needed). Note that this theorem shows that actually, the standard instance of curryax 890 implies the standard instance of peirce 201, which is not the case for the converse bj-peircecurry 35890. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | ||
Theorem | bj-peircecurry 35890 | Peirce's axiom peirce 201 implies Curry's axiom curryax 890 over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the introduction axioms olc 865 and orc 864; the elimination axiom jao 957 is not needed). See bj-currypeirce 35889 for the converse. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ∨ (𝜑 → 𝜓)) | ||
Theorem | bj-animbi 35891 | 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 35892 | 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 35893 | A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19-Mar-2020.) |
⊢ (𝜑 → ((𝜓 → ¬ 𝜑) → ¬ 𝜓)) | ||
Theorem | bj-con2comi 35894 | Inference associated with bj-con2com 35893. Its associated inference is mt2 199. TODO: when in the main part, add to mt2 199 that it is the inference associated with bj-con2comi 35894. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ((𝜓 → ¬ 𝜑) → ¬ 𝜓) | ||
Theorem | bj-pm2.01i 35895 | Inference associated with the weak Clavius law pm2.01 188. (Contributed by BJ, 30-Mar-2020.) |
⊢ (𝜑 → ¬ 𝜑) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bj-nimn 35896 | 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 161, however, the present proof uses theorems that are more basic than jc 161. (Proof modification is discouraged.) |
⊢ (𝜑 → ¬ (𝜑 → ¬ 𝜑)) | ||
Theorem | bj-nimni 35897 | Inference associated with bj-nimn 35896. (Contributed by BJ, 19-Mar-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → ¬ 𝜑) | ||
Theorem | bj-peircei 35898 | Inference associated with peirce 201. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | bj-looinvi 35899 | Inference associated with looinv 202. Its associated inference is bj-looinvii 35900. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) ⇒ ⊢ ((𝜓 → 𝜑) → 𝜑) | ||
Theorem | bj-looinvii 35900 | Inference associated with bj-looinvi 35899. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |