Home | Metamath
Proof Explorer Theorem List (p. 297 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 | dpval2 29601 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10)) | ||
Theorem | dpval3 29602 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
Theorem | dpmul10 29603 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 | ||
Theorem | decdiv10 29604 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵) | ||
Theorem | dpmul100 29605 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶 | ||
Theorem | dp3mul10 29606 | Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶) | ||
Theorem | dpmul1000 29607 | Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷 | ||
Theorem | dpval3rp 29608 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
Theorem | dp0u 29609 | Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝐴.0) = 𝐴 | ||
Theorem | dp0h 29610 | Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ (0.𝐴) = (𝐴 / ;10) | ||
Theorem | rpdpcl 29611 | Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) ∈ ℝ+ | ||
Theorem | dplt 29612 | Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐴.𝐵) < (𝐴.𝐶) | ||
Theorem | dplti 29613 | Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ (𝐴.𝐵) < 𝐶 | ||
Theorem | dpgti 29614 | Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ 𝐴 < (𝐴.𝐵) | ||
Theorem | dpltc 29615 | Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐴 < 𝐶 & ⊢ 𝐵 < ;10 ⇒ ⊢ (𝐴.𝐵) < (𝐶.𝐷) | ||
Theorem | dpexpp1 29616 | Add one zero to the mantisse, and a one to the exponent in a scientific notation. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ (𝑃 + 1) = 𝑄 & ⊢ 𝑃 ∈ ℤ & ⊢ 𝑄 ∈ ℤ ⇒ ⊢ ((𝐴.𝐵) · (;10↑𝑃)) = ((0._𝐴𝐵) · (;10↑𝑄)) | ||
Theorem | 0dp2dp 29617 | Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵) | ||
Theorem | dpadd2 29618 | Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℝ+ & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ (𝐺 + 𝐻) = 𝐼 & ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) ⇒ ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹) | ||
Theorem | dpadd 29619 | Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹 ⇒ ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) | ||
Theorem | dpadd3 29620 | Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ 𝐼 ∈ ℕ0 & ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼 ⇒ ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼) | ||
Theorem | dpmul 29621 | Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐽 ∈ ℕ0 & ⊢ 𝐾 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐹 & ⊢ (𝐴 · 𝐷) = 𝑀 & ⊢ (𝐵 · 𝐶) = 𝐿 & ⊢ (𝐵 · 𝐷) = ;𝐸𝐾 & ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽 & ⊢ (𝐹 + 𝐺) = 𝐼 ⇒ ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾) | ||
Theorem | dpmul4 29622 | An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐽 ∈ ℕ0 & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ 𝐼 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑂 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ0 & ⊢ 𝑆 ∈ ℕ0 & ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑈 ∈ ℕ0 & ⊢ 𝑊 ∈ ℕ0 & ⊢ 𝑋 ∈ ℕ0 & ⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑍 ∈ ℕ0 & ⊢ 𝑈 < ;10 & ⊢ 𝑃 < ;10 & ⊢ 𝑄 < ;10 & ⊢ (;;𝐿𝑀𝑁 + 𝑂) = ;;;𝑅𝑆𝑇𝑈 & ⊢ ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼._𝐽𝐾) & ⊢ ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂._𝑃𝑄) & ⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = ;;;𝑊𝑋𝑌𝑍 & ⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) ⇒ ⊢ ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) < (𝑊._𝑋_𝑌𝑍) | ||
Theorem | threehalves 29623 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ (3 / 2) = (1.5) | ||
Theorem | 1mhdrd 29624 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ ((0._99) + (0._01)) = 1 | ||
Syntax | cxdiv 29625 | Extend class notation to include division of extended reals. |
class /𝑒 | ||
Definition | df-xdiv 29626* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥)) | ||
Theorem | xdivval 29627* | 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 29628* | Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1) | ||
Theorem | xmulcand 29629 | Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | xreceu 29630* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴) | ||
Theorem | xdivcld 29631 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivcl 29632 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivmul 29633 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴)) | ||
Theorem | rexdiv 29634 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵)) | ||
Theorem | xdivrec 29635 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵))) | ||
Theorem | xdivid 29636 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1) | ||
Theorem | xdiv0 29637 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0) | ||
Theorem | xdiv0rp 29638 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0) | ||
Theorem | eliccioo 29639 | Membership in a closed interval of extended reals vs. the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵))) | ||
Theorem | elxrge02 29640 | Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞)) | ||
Theorem | xdivpnfrp 29641 | Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞) | ||
Theorem | rpxdivcld 29642 | Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+) | ||
Theorem | xrpxdivcld 29643 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | bhmafibid1 29644 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid2 29645 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | ||
Theorem | 2sqn0 29646 | If the sum of two squares is prime, none of the original number is zero. (Contributed by Thierry Arnoux, 4-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | 2sqcoprm 29647 | If the sum of two squares is prime, the two original numbers are coprime. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
Theorem | 2sqmod 29648 | Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) & ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | 2sqmo 29649* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 25157 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | ressplusf 29650 | 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 29651 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻)) | ||
Theorem | abvpropd2 29652 | Weaker version of abvpropd 18842. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
Theorem | oppgle 29653 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ ≤ = (le‘𝑅) ⇒ ⊢ ≤ = (le‘𝑂) | ||
Theorem | oppglt 29654 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ < = (lt‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂)) | ||
Theorem | ressprs 29655 | The restriction of a preordered set is still a preordered set. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Preset ) | ||
Theorem | oduprs 29656 | Being a preset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Preset → 𝐷 ∈ Preset ) | ||
Theorem | posrasymb 29657 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | tospos 29658 | A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset) | ||
Theorem | resspos 29659 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset) | ||
Theorem | resstos 29660 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Toset) | ||
Theorem | tleile 29661 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
Theorem | tltnle 29662 | In a Toset, less-than is equivalent to not inverse less-than-or-equal see pltnle 16966. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋)) | ||
Theorem | odutos 29663 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset) | ||
Theorem | tlt2 29664 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | tlt3 29665 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | trleile 29666 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
Theorem | toslublem 29667* | Lemma for toslub 29668 and xrsclat 29680. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) | ||
Theorem | toslub 29668 | 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 29669* | Lemma for tosglb 29670 and xrsclat 29680. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑)))) | ||
Theorem | tosglb 29670 | Same theorem as toslub 29668, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < )) | ||
Theorem | clatp0cl 29671 | 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 29672 | 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 29673 | 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 29674 | 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 29675 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12079 and df-xrs 16162), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ 0 = (0g‘ℝ*𝑠) | ||
Theorem | xrslt 29676 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ < = (lt‘ℝ*𝑠) | ||
Theorem | xrsinvgval 29677 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12079 and df-xrs 16162), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
Theorem | xrsmulgzz 29678 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
Theorem | xrstos 29679 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ Toset | ||
Theorem | xrsclat 29680 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ CLat | ||
Theorem | xrsp0 29681 | 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 29682 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ +∞ = (1.‘ℝ*𝑠) | ||
Theorem | ressmulgnn 29683 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
Theorem | ressmulgnn0 29684 | 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 29685 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge00 29686 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0plusg 29687 | 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 29688 | The lower-or-equal relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0mulgnn0 29689 | 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 29690 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
Theorem | xrge0addgt0 29691 | The sum of nonnegative and positive numbers is positive. See addgtge0 10516. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
Theorem | xrge0adddir 29692 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | xrge0adddi 29693 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
Theorem | xrge0npcan 29694 | Extended nonnegative real version of npcan 10290. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
Theorem | fsumrp0cl 29695* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
Theorem | abliso 29696 | 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 29697 | Extend class notation with the class of all right ordered monoids. |
class oMnd | ||
Syntax | cogrp 29698 | Extend class notation with the class of all right ordered groups. |
class oGrp | ||
Definition | df-omnd 29699* | 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 29700 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |