Home | Metamath
Proof Explorer Theorem List (p. 415 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rnmptbd2 41401* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
Theorem | infnsuprnmpt 41402* | The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) = -sup(ran (𝑥 ∈ 𝐴 ↦ -𝐵), ℝ, < )) | ||
Theorem | suprclrnmpt 41403* | Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) ∈ ℝ) | ||
Theorem | suprubrnmpt2 41404* | A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | suprubrnmpt 41405* | A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | rnmptssdf 41406* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptbdlem 41407* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptbd 41408* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptss2 41409* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ ran (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | elmptima 41410* | The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵)) | ||
Theorem | ralrnmpt3 41411* | A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | fvelima2 41412* | Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (𝐹 “ 𝐶)) → ∃𝑥 ∈ (𝐴 ∩ 𝐶)(𝐹‘𝑥) = 𝐵) | ||
Theorem | funresd 41413 | A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴)) | ||
Theorem | rnmptssbi 41414* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)) | ||
Theorem | fnfvelrnd 41415 | A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | imass2d 41416 | Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | imassmpt 41417* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷)) | ||
Theorem | fpmd 41418 | A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | fconst7 41419* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | sub2times 41420 | Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴) | ||
Theorem | abssubrp 41421 | The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+) | ||
Theorem | elfzfzo 41422 | Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝑀..^𝑁) ↔ (𝐴 ∈ (𝑀...𝑁) ∧ 𝐴 < 𝑁)) | ||
Theorem | oddfl 41423 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
Theorem | abscosbd 41424 | Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1) | ||
Theorem | mul13d 41425 | Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴))) | ||
Theorem | negpilt0 41426 | Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ -π < 0 | ||
Theorem | dstregt0 41427* | A complex number 𝐴 that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) | ||
Theorem | subadd4b 41428 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵))) | ||
Theorem | xrlttri5d 41429 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | neglt 41430 | The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴) | ||
Theorem | zltlesub 41431 | If an integer 𝑁 is less than or equal to a real, and we subtract a quantity less than 1, then 𝑁 is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 1) & ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑁 ≤ (𝐴 − 𝐵)) | ||
Theorem | divlt0gt0d 41432 | The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) < 0) | ||
Theorem | subsub23d 41433 | Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | 2timesgt 41434 | Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 < (2 · 𝐴)) | ||
Theorem | reopn 41435 | The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℝ ∈ (topGen‘ran (,)) | ||
Theorem | elfzop1le2 41436 | A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 + 1) ≤ 𝑁) | ||
Theorem | sub31 41437 | Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐶 − (𝐵 − 𝐴))) | ||
Theorem | nnne1ge2 41438 | A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁) | ||
Theorem | lefldiveq 41439 | A closed enough, smaller real 𝐶 has the same floor of 𝐴 when both are divided by 𝐵. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,]𝐴)) ⇒ ⊢ (𝜑 → (⌊‘(𝐴 / 𝐵)) = (⌊‘(𝐶 / 𝐵))) | ||
Theorem | negsubdi3d 41440 | Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 − -𝐵)) | ||
Theorem | ltdiv2dd 41441 | Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) < (𝐶 / 𝐴)) | ||
Theorem | abssinbd 41442 | Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(sin‘𝐴)) ≤ 1) | ||
Theorem | halffl 41443 | Floor of (1 / 2). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (⌊‘(1 / 2)) = 0 | ||
Theorem | monoords 41444* | Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐼 < 𝐽) ⇒ ⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) | ||
Theorem | hashssle 41445 | The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 13760, and hashssle 41445 should be deleted afterwards. |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴)) | ||
Theorem | lttri5d 41446 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | fzisoeu 41447* | A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 13810 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐻 ∈ Fin) & ⊢ (𝜑 → < Or 𝐻) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1)) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) | ||
Theorem | lt3addmuld 41448 | If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐷) & ⊢ (𝜑 → 𝐵 < 𝐷) & ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) < (3 · 𝐷)) | ||
Theorem | absnpncan2d 41449 | Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐷)) ≤ (((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷)))) | ||
Theorem | fperiodmullem 41450* | A function with period T is also periodic with period nonnegative multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | fperiodmul 41451* | A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | upbdrech 41452* | Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐶 = sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | lt4addmuld 41453 | If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐸) & ⊢ (𝜑 → 𝐵 < 𝐸) & ⊢ (𝜑 → 𝐶 < 𝐸) & ⊢ (𝜑 → 𝐷 < 𝐸) ⇒ ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) + 𝐷) < (4 · 𝐸)) | ||
Theorem | absnpncan3d 41454 | Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐸)) ≤ ((((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷))) + (abs‘(𝐷 − 𝐸)))) | ||
Theorem | upbdrech2 41455* | Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐶 = if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < )) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | ssfiunibd 41456* | A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑥 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐶 𝐵 ≤ 𝑤) | ||
Theorem | fzdifsuc2 41457 | Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 12957, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘(𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzsscn 41458 | A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℂ | ||
Theorem | divcan8d 41459 | A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / (𝐴 · 𝐵)) = (1 / 𝐴)) | ||
Theorem | dmmcand 41460 | Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 · 𝐶)) = (𝐴 · 𝐶)) | ||
Theorem | fzssre 41461 | A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℝ | ||
Theorem | elfzelzd 41462 | A member of a finite set of sequential integer is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | bccld 41463 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | leadd12dd 41464 | Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | fzssnn0 41465 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | xreqle 41466 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | xaddid2d 41467 | 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (0 +𝑒 𝐴) = 𝐴) | ||
Theorem | xadd0ge 41468 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | elfzolem1 41469 | A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ≤ (𝑁 − 1)) | ||
Theorem | xrgtned 41470 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | xrleneltd 41471 | 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | xaddcomd 41472 | The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
Theorem | supxrre3 41473* | The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | ||
Theorem | uzfissfz 41474* | For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 𝐴 ⊆ (𝑀...𝑘)) | ||
Theorem | xleadd2d 41475 | Addition of extended reals preserves the "less than or equal to" relation, in the right slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) | ||
Theorem | suprltrp 41476* | The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 (sup(𝐴, ℝ, < ) − 𝑋) < 𝑧) | ||
Theorem | xleadd1d 41477 | Addition of extended reals preserves the "less than or equal to" relation, in the left slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) | ||
Theorem | xreqled 41478 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | xrgepnfd 41479 | An extended real greater than or equal to +∞ is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → +∞ ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | xrge0nemnfd 41480 | A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≠ -∞) | ||
Theorem | supxrgere 41481* | If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | iuneqfzuzlem 41482* | Lemma for iuneqfzuz 41483: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵) | ||
Theorem | iuneqfzuz 41483* | If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 = ∪ 𝑛 ∈ 𝑍 𝐵) | ||
Theorem | xle2addd 41484 | Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)) | ||
Theorem | supxrgelem 41485* | If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | supxrge 41486* | If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | suplesup 41487* | If any element of 𝐴 can be approximated from below by members of 𝐵, then the supremum of 𝐴 is less than or equal to the supremum of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ 𝐵 (𝑥 − 𝑦) < 𝑧) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | infxrglb 41488* | The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (inf(𝐴, ℝ*, < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵)) | ||
Theorem | xadd0ge2 41489 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 𝐴)) | ||
Theorem | nepnfltpnf 41490 | An extended real that is not +∞ is less than +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ≠ +∞) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 < +∞) | ||
Theorem | ltadd12dd 41491 | Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | nemnftgtmnft 41492 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) | ||
Theorem | xrgtso 41493 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ◡ < Or ℝ* | ||
Theorem | rpex 41494 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℝ+ ∈ V | ||
Theorem | xrge0ge0 41495 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ (0[,]+∞) → 0 ≤ 𝐴) | ||
Theorem | xrssre 41496 | A subset of extended reals that does not contain +∞ and -∞ is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → ¬ +∞ ∈ 𝐴) & ⊢ (𝜑 → ¬ -∞ ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℝ) | ||
Theorem | ssuzfz 41497 | A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < ))) | ||
Theorem | absfun 41498 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Fun abs | ||
Theorem | infrpge 41499* | The infimum of a nonempty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)) | ||
Theorem | xrlexaddrp 41500* | If an extended real number 𝐴 can be approximated from above, adding positive reals to 𝐵, then 𝐴 is less than or equal to 𝐵. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |