Home | Metamath
Proof Explorer Theorem List (p. 325 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alnof 32401 | For all sets, ⊥ is not true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∀𝑥 ¬ ⊥ | ||
Theorem | nalf 32402 | Not all sets hold ⊥ as true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∀𝑥⊥ | ||
Theorem | extt 32403 | There exists a set that holds ⊤ as true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∃𝑥⊤ | ||
Theorem | nextnt 32404 | There does not exist a set, such that ⊤ is not true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃𝑥 ¬ ⊤ | ||
Theorem | nextf 32405 | There does not exist a set, such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃𝑥⊥ | ||
Theorem | unnf 32406 | There does not exist exactly one set, such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃!𝑥⊥ | ||
Theorem | unnt 32407 | There does not exist exactly one set, such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃!𝑥⊤ | ||
Theorem | mont 32408 | There does not exist at most one set, such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃*𝑥⊤ | ||
Theorem | mof 32409 | There exist at most one set, such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∃*𝑥⊥ | ||
Theorem | meran1 32410 | A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑)))) | ||
Theorem | meran2 32411 | A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜏 ∨ 𝜃) ∨ (𝜒 ∨ (𝜑 ∨ 𝜃)))) | ||
Theorem | meran3 32412 | A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜒 ∨ 𝜑) ∨ (𝜏 ∨ (𝜃 ∨ 𝜑)))) | ||
Theorem | waj-ax 32413 | A single axiom for propositional calculus offered by Wajsberg. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓)))) | ||
Theorem | lukshef-ax2 32414 | A single axiom for propositional calculus offered by Lukasiewicz. (Contributed by Anthony Hart, 14-Aug-2011.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | arg-ax 32415 | ? (Contributed by Anthony Hart, 14-Aug-2011.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | negsym1 32416 |
In the paper "On Variable Functors of Propositional Arguments",
Lukasiewicz introduced a system that can handle variable connectives.
This was done by introducing a variable, marked with a lowercase delta,
which takes a wff as input. In the system, "delta 𝜑 "
means that
"something is true of 𝜑." "delta 𝜑 "
can be substituted with
¬ 𝜑, 𝜓 ∧ 𝜑, ∀𝑥𝜑, etc.
Later on, Meredith discovered a single axiom, in the form of ( delta delta ⊥ → delta 𝜑 ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus. A symmetry with ¬. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ (¬ ¬ ⊥ → ¬ 𝜑) | ||
Theorem | imsym1 32417 |
A symmetry with →.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 → (𝜓 → ⊥)) → (𝜓 → 𝜑)) | ||
Theorem | bisym1 32418 |
A symmetry with ↔.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑)) | ||
Theorem | consym1 32419 |
A symmetry with ∧.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑)) | ||
Theorem | dissym1 32420 |
A symmetry with ∨.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑)) | ||
Theorem | nandsym1 32421 |
A symmetry with ⊼.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑)) | ||
Theorem | unisym1 32422 |
A symmetry with ∀.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑) | ||
Theorem | exisym1 32423 |
A symmetry with ∃.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑) | ||
Theorem | unqsym1 32424 |
A symmetry with ∃!.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 6-Sep-2011.) |
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑) | ||
Theorem | amosym1 32425 |
A symmetry with ∃*.
See negsym1 32416 for more information. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑) | ||
Theorem | subsym1 32426 |
A symmetry with [𝑥 / 𝑦].
See negsym1 32416 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) |
⊢ ([𝑥 / 𝑦][𝑥 / 𝑦]⊥ → [𝑥 / 𝑦]𝜑) | ||
Theorem | ontopbas 32427 | An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.) |
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases) | ||
Theorem | onsstopbas 32428 | The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.) |
⊢ On ⊆ TopBases | ||
Theorem | onpsstopbas 32429 | The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.) |
⊢ On ⊊ TopBases | ||
Theorem | ontgval 32430 | The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.) |
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵) | ||
Theorem | ontgsucval 32431 | The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.) |
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴) | ||
Theorem | onsuctop 32432 | A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top) | ||
Theorem | onsuctopon 32433 | One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴)) | ||
Theorem | ordtoplem 32434 | Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆) ⇒ ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆)) | ||
Theorem | ordtop 32435 | An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽)) | ||
Theorem | onsucconni 32436 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ Conn | ||
Theorem | onsucconn 32437 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn) | ||
Theorem | ordtopconn 32438 | An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn)) | ||
Theorem | onintopssconn 32439 | An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ (On ∩ Top) ⊆ Conn | ||
Theorem | onsuct0 32440 | A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2) | ||
Theorem | ordtopt0 32441 | An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2)) | ||
Theorem | onsucsuccmpi 32442 | The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc suc 𝐴 ∈ Comp | ||
Theorem | onsucsuccmp 32443 | The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.) |
⊢ (𝐴 ∈ On → suc suc 𝐴 ∈ Comp) | ||
Theorem | limsucncmpi 32444 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
⊢ Lim 𝐴 ⇒ ⊢ ¬ suc 𝐴 ∈ Comp | ||
Theorem | limsucncmp 32445 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp) | ||
Theorem | ordcmp 32446 | An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1𝑜. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 = ∪ ∪ 𝐴 → 𝐴 = 1𝑜))) | ||
Theorem | ssoninhaus 32447 | The ordinal topologies 1𝑜 and 2𝑜 are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.) |
⊢ {1𝑜, 2𝑜} ⊆ (On ∩ Haus) | ||
Theorem | onint1 32448 | The ordinal T1 spaces are 1𝑜 and 2𝑜, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.) |
⊢ (On ∩ Fre) = {1𝑜, 2𝑜} | ||
Theorem | oninhaus 32449 | The ordinal Hausdorff spaces are 1𝑜 and 2𝑜. (Contributed by Chen-Pang He, 10-Nov-2015.) |
⊢ (On ∩ Haus) = {1𝑜, 2𝑜} | ||
Theorem | fveleq 32450 | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃))) | ||
Theorem | findfvcl 32451* | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃) & ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃))) ⇒ ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃)) | ||
Theorem | findreccl 32452* | Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) ⇒ ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃)) | ||
Theorem | findabrcl 32453* | Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) ⇒ ⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃) → ((𝑥 ∈ V ↦ (rec(𝐺, 𝐴)‘𝑥))‘𝐶) ∈ 𝑃) | ||
Theorem | nnssi2 32454 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐵 ∈ ℕ → 𝜑) & ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓) | ||
Theorem | nnssi3 32455 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐶 ∈ ℕ → 𝜑) & ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓) | ||
Theorem | nndivsub 32456 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ)) | ||
Theorem | nndivlub 32457 | A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴)) | ||
Syntax | cgcdOLD 32458 | Extend class notation to include the gdc function. (New usage is discouraged.) |
class gcdOLD (𝐴, 𝐵) | ||
Definition | df-gcdOLD 32459* | 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 32460 | 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 32461* | Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) | ||
Theorem | dnicld1 32462 | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) | ||
Theorem | dnicld2 32463* | Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ) | ||
Theorem | dnif 32464 | The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇:ℝ⟶ℝ | ||
Theorem | dnizeq0 32465* | The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑇‘𝐴) = 0) | ||
Theorem | dnizphlfeqhlf 32466* | 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 32467 | Variant of rddif 14080. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | ||
Theorem | dnibndlem1 32468* | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆)) | ||
Theorem | dnibndlem2 32469* | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem3 32470 | Lemma for dnibnd 32481. (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 32471 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem5 32472 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem6 32473 | Lemma for dnibnd 32481. (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 32474 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)))) | ||
Theorem | dnibndlem8 32475 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) | ||
Theorem | dnibndlem9 32476* | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1)) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem10 32477 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴)) | ||
Theorem | dnibndlem11 32478 | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2)) | ||
Theorem | dnibndlem12 32479* | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibndlem13 32480* | Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2)))) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnibnd 32481* | The "distance to nearest integer" function is Lipshitz continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | dnicn 32482 | The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) ⇒ ⊢ 𝑇 ∈ (ℝ–cn→ℝ) | ||
Theorem | knoppcnlem1 32483* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) |
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) | ||
Theorem | knoppcnlem2 32484* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) | ||
Theorem | knoppcnlem3 32485* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ) | ||
Theorem | knoppcnlem4 32486* | Lemma for knoppcn 32494. (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 32487* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))):ℕ0⟶(ℂ ↑𝑚 ℝ)) | ||
Theorem | knoppcnlem6 32488* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐶) < 1) ⇒ ⊢ (𝜑 → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom (⇝𝑢‘ℝ)) | ||
Theorem | knoppcnlem7 32489* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → (seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑀) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑀))) | ||
Theorem | knoppcnlem8 32490* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ ↑𝑚 ℝ)) | ||
Theorem | knoppcnlem9 32491* | Lemma for knoppcn 32494. (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( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊) | ||
Theorem | knoppcnlem10 32492* | Lemma for knoppcn 32494. (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 32493* | Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℝ–cn→ℂ)) | ||
Theorem | knoppcn 32494* | 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 32495* | Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.) |
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) & ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) & ⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐶) < 1) ⇒ ⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ) | ||
Theorem | addgtge0d 32496 | Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
Theorem | unblimceq0lem 32497* | Lemma for unblimceq0 32498. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → ∀𝑐 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑦 ∈ 𝑆 (𝑦 ≠ 𝐴 ∧ (abs‘(𝑦 − 𝐴)) < 𝑑 ∧ 𝑐 ≤ (abs‘(𝐹‘𝑦)))) | ||
Theorem | unblimceq0 32498* | If 𝐹 is unbounded near 𝐴 it has no limit at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∀𝑑 ∈ ℝ+ ∃𝑥 ∈ 𝑆 ((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐴) = ∅) | ||
Theorem | unbdqndv1 32499* | 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 32500 | Lemma for unbdqndv2 32502. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷))) ⇒ ⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |