HomeTheorem List (p. 303 of 437)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 303 of 437) | < 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-28364) |
Hilbert Space Explorer
(28365-29889) |
Users' Mathboxes
(29890-43671) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | cxdiv 30201 | Extend class notation to include division of extended reals. |
| class /𝑒 | ||
| Definition | df-xdiv 30202* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥)) | ||
| Theorem | xdivval 30203* | Value of division: the (unique) element 𝑥 such that (𝐵 · 𝑥) = 𝐴. This is meaningful only when 𝐵 is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (℩𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)) | ||
| Theorem | xrecex 30204* | Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1) | ||
| Theorem | xmulcand 30205 | Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | xreceu 30206* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴) | ||
| Theorem | xdivcld 30207 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
| Theorem | xdivcl 30208 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
| Theorem | xdivmul 30209 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴)) | ||
| Theorem | rexdiv 30210 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵)) | ||
| Theorem | xdivrec 30211 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵))) | ||
| Theorem | xdivid 30212 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1) | ||
| Theorem | xdiv0 30213 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0) | ||
| Theorem | xdiv0rp 30214 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0) | ||
| Theorem | eliccioo 30215 | Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵))) | ||
| Theorem | elxrge02 30216 | Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞)) | ||
| Theorem | xdivpnfrp 30217 | Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞) | ||
| Theorem | rpxdivcld 30218 | Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+) | ||
| Theorem | xrpxdivcld 30219 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞)) | ||
| Theorem | ressplusf 30220 | The group operation function +𝑓 of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ ⨣ = (+g‘𝐺) & ⊢ ⨣ Fn (𝐵 × 𝐵) & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (+𝑓‘𝐻) = ( ⨣ ↾ (𝐴 × 𝐴)) | ||
| Theorem | ressnm 30221 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻)) | ||
| Theorem | abvpropd2 30222 | Weaker version of abvpropd 19245. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
| Theorem | oppgle 30223 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝑂 = (oppg‘𝑅) & ⊢ ≤ = (le‘𝑅) ⇒ ⊢ ≤ = (le‘𝑂) | ||
| Theorem | oppglt 30224 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝑂 = (oppg‘𝑅) & ⊢ < = (lt‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂)) | ||
| Theorem | ressprs 30225 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset ) | ||
| Theorem | oduprs 30226 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset ) | ||
| Theorem | posrasymb 30227 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
| Theorem | tospos 30228 | A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset) | ||
| Theorem | resspos 30229 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset) | ||
| Theorem | resstos 30230 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ ((𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Toset) | ||
| Theorem | tleile 30231 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
| Theorem | tltnle 30232 | In a Toset, less-than is equivalent to not inverse "less than or equal to" see pltnle 17363. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋)) | ||
| Theorem | odutos 30233 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset) | ||
| Theorem | tlt2 30234 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋)) | ||
| Theorem | tlt3 30235 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋)) | ||
| Theorem | trleile 30236 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
| Theorem | toslublem 30237* | Lemma for toslub 30238 and xrsclat 30250. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) | ||
| Theorem | toslub 30238 | In a toset, the lowest upper bound lub, defined for partial orders is the supremum, sup(𝐴, 𝐵, < ), defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018.) (Revised by Thierry Arnoux, 24-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((lub‘𝐾)‘𝐴) = sup(𝐴, 𝐵, < )) | ||
| Theorem | tosglblem 30239* | Lemma for tosglb 30240 and xrsclat 30250. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑)))) | ||
| Theorem | tosglb 30240 | Same theorem as toslub 30238, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < )) | ||
| Theorem | clatp0cl 30241 | The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0.‘𝑊) ⇒ ⊢ (𝑊 ∈ CLat → 0 ∈ 𝐵) | ||
| Theorem | clatp1cl 30242 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 1 = (1.‘𝑊) ⇒ ⊢ (𝑊 ∈ CLat → 1 ∈ 𝐵) | ||
| Axiom | ax-xrssca 30243 | Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ ℝfld = (Scalar‘ℝ*𝑠) | ||
| Axiom | ax-xrsvsca 30244 | Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ ·e = ( ·𝑠 ‘ℝ*𝑠) | ||
| Theorem | xrs0 30245 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12396 and df-xrs 16559), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ 0 = (0g‘ℝ*𝑠) | ||
| Theorem | xrslt 30246 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ < = (lt‘ℝ*𝑠) | ||
| Theorem | xrsinvgval 30247 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12396 and df-xrs 16559), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
| Theorem | xrsmulgzz 30248 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrstos 30249 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ Toset | ||
| Theorem | xrsclat 30250 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ CLat | ||
| Theorem | xrsp0 30251 | The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Proof shortened by AV, 28-Sep-2020.) |
| ⊢ -∞ = (0.‘ℝ*𝑠) | ||
| Theorem | xrsp1 30252 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ +∞ = (1.‘ℝ*𝑠) | ||
| Theorem | ressmulgnn 30253 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
| Theorem | ressmulgnn0 30254 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (0g‘𝐺) = (0g‘𝐻) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
| Theorem | xrge0base 30255 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge00 30256 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0plusg 30257 | The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
| ⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0le 30258 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
| ⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0mulgnn0 30259 | The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴(.g‘(ℝ*𝑠 ↾s (0[,]+∞)))𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrge0addass 30260 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xrge0addgt0 30261 | The sum of nonnegative and positive numbers is positive. See addgtge0 10866. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
| ⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
| Theorem | xrge0adddir 30262 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
| Theorem | xrge0adddi 30263 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
| Theorem | xrge0npcan 30264 | Extended nonnegative real version of npcan 10634. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | fsumrp0cl 30265* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
| Theorem | abliso 30266 | The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Abel) | ||
| Syntax | comnd 30267 | Extend class notation with the class of all right ordered monoids. |
| class oMnd | ||
| Syntax | cogrp 30268 | Extend class notation with the class of all right ordered groups. |
| class oGrp | ||
| Definition | df-omnd 30269* | Define class of all right ordered monoids. An ordered monoid is a monoid with a total ordering compatible with its operation. It is possible to use this definition also for left ordered monoids, by applying it to (oppg‘𝑀). (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ oMnd = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))} | ||
| Definition | df-ogrp 30270 | Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ oGrp = (Grp ∩ oMnd) | ||
| Theorem | isomnd 30271* | A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ≤ = (le‘𝑀) ⇒ ⊢ (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎 ≤ 𝑏 → (𝑎 + 𝑐) ≤ (𝑏 + 𝑐)))) | ||
| Theorem | isogrp 30272 | A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd)) | ||
| Theorem | ogrpgrp 30273 | A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
| ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) | ||
| Theorem | omndmnd 30274 | A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) | ||
| Theorem | omndtos 30275 | A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) | ||
| Theorem | omndadd 30276 | In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍)) | ||
| Theorem | omndaddr 30277 | In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (((oppg‘𝑀) ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑍 + 𝑋) ≤ (𝑍 + 𝑌)) | ||
| Theorem | omndadd2d 30278 | In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑍) & ⊢ (𝜑 → 𝑌 ≤ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ CMnd) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) | ||
| Theorem | omndadd2rd 30279 | In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑍) & ⊢ (𝜑 → 𝑌 ≤ 𝑊) & ⊢ (𝜑 → (oppg‘𝑀) ∈ oMnd) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) | ||
| Theorem | submomnd 30280 | A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) | ||
| Theorem | xrge0omnd 30281 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd | ||
| Theorem | omndmul2 30282 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑁 · 𝑋)) | ||
| Theorem | omndmul3 30283 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ≤ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 0 ≤ 𝑋) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑃 · 𝑋)) | ||
| Theorem | omndmul 30284 | In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑁 · 𝑌)) | ||
| Theorem | ogrpinvOLD 30285 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 30-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) → (𝐼‘𝑋) ≤ 0 ) | ||
| Theorem | ogrpinv0le 30286 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 ≤ 𝑋 ↔ (𝐼‘𝑋) ≤ 0 )) | ||
| Theorem | ogrpsub 30287 | In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍)) | ||
| Theorem | ogrpaddlt 30288 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) | ||
| Theorem | ogrpaddltbi 30289 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋 + 𝑍) < (𝑌 + 𝑍))) | ||
| Theorem | ogrpaddltrd 30290 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < 𝑌) ⇒ ⊢ (𝜑 → (𝑍 + 𝑋) < (𝑍 + 𝑌)) | ||
| Theorem | ogrpaddltrbid 30291 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 < 𝑌 ↔ (𝑍 + 𝑋) < (𝑍 + 𝑌))) | ||
| Theorem | ogrpsublt 30292 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍)) | ||
| Theorem | ogrpinv0lt 30293 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ (𝐼‘𝑋) < 0 )) | ||
| Theorem | ogrpinvlt 30294 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (((𝐺 ∈ oGrp ∧ (oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝐼‘𝑌) < (𝐼‘𝑋))) | ||
| Syntax | csgns 30295 | Extend class notation to include the Signum function. |
| class sgns | ||
| Definition | df-sgns 30296* | Signum function for a structure. See also df-sgn 14240 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.) |
| ⊢ sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))) | ||
| Theorem | sgnsv 30297* | The sign mapping. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ < = (lt‘𝑅) & ⊢ 𝑆 = (sgns‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑆 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1)))) | ||
| Theorem | sgnsval 30298 | The sign value. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ < = (lt‘𝑅) & ⊢ 𝑆 = (sgns‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑆‘𝑋) = if(𝑋 = 0 , 0, if( 0 < 𝑋, 1, -1))) | ||
| Theorem | sgnsf 30299 | The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ < = (lt‘𝑅) & ⊢ 𝑆 = (sgns‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑆:𝐵⟶{-1, 0, 1}) | ||
| Syntax | cinftm 30300 | Class notation for the infinitesimal relation. |
| class ⋘ | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |