![]() |
Metamath
Proof Explorer Theorem List (p. 453 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rnmptss2 45201* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ ran (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | elmptima 45202* | The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵)) | ||
Theorem | ralrnmpt3 45203* | A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | fvelima2 45204* | Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (𝐹 “ 𝐶)) → ∃𝑥 ∈ (𝐴 ∩ 𝐶)(𝐹‘𝑥) = 𝐵) | ||
Theorem | rnmptssbi 45205* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)) | ||
Theorem | imass2d 45206 | Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | imassmpt 45207* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷)) | ||
Theorem | fpmd 45208 | A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | fconst7 45209* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | fnmptif 45210 | Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | dmmptif 45211 | Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | mpteq2dfa 45212 | Slightly more general equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | dmmpt1 45213 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom (𝑥 ∈ 𝐵 ↦ 𝐶) = 𝐵) | ||
Theorem | fmptff 45214 | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | fvmptelcdmf 45215 | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fmptdff 45216 | A version of fmptd 7133 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fvmpt2df 45217 | Deduction version of fvmpt2 7026. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) | ||
Theorem | rn1st 45218 | The range of a function with a first-countable domain is itself first-countable. This is a variation of 1stcrestlem 23475, with a not-free hypothesis replacing a disjoint variable constraint. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
Theorem | rnmptssff 45219 | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptssdff 45220 | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | fvmpt4d 45221 | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
Theorem | sub2times 45222 | Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴) | ||
Theorem | nnxrd 45223 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | nnxr 45224 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ*) | ||
Theorem | abssubrp 45225 | The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+) | ||
Theorem | elfzfzo 45226 | 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 45227 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
Theorem | abscosbd 45228 | Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1) | ||
Theorem | mul13d 45229 | Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴))) | ||
Theorem | negpilt0 45230 | Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ -π < 0 | ||
Theorem | dstregt0 45231* | 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 45232 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵))) | ||
Theorem | xrlttri5d 45233 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | neglt 45234 | The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴) | ||
Theorem | zltlesub 45235 | 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 45236 | The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) < 0) | ||
Theorem | subsub23d 45237 | Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | 2timesgt 45238 | Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 < (2 · 𝐴)) | ||
Theorem | reopn 45239 | The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℝ ∈ (topGen‘ran (,)) | ||
Theorem | sub31 45240 | Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐶 − (𝐵 − 𝐴))) | ||
Theorem | nnne1ge2 45241 | 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 45242 | 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 45243 | Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 − -𝐵)) | ||
Theorem | ltdiv2dd 45244 | Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) < (𝐶 / 𝐴)) | ||
Theorem | abssinbd 45245 | Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(sin‘𝐴)) ≤ 1) | ||
Theorem | halffl 45246 | Floor of (1 / 2). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (⌊‘(1 / 2)) = 0 | ||
Theorem | monoords 45247* | Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐼 < 𝐽) ⇒ ⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) | ||
Theorem | hashssle 45248 | 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 14444, and hashssle 45248 should be deleted afterwards. |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴)) | ||
Theorem | lttri5d 45249 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | fzisoeu 45250* | A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 14497 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐻 ∈ Fin) & ⊢ (𝜑 → < Or 𝐻) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1)) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) | ||
Theorem | lt3addmuld 45251 | 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 45252 | Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐷)) ≤ (((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷)))) | ||
Theorem | fperiodmullem 45253* | A function with period 𝑇 is also periodic with period nonnegative multiple of 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | fperiodmul 45254* | A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | upbdrech 45255* | Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐶 = sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | lt4addmuld 45256 | 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 45257 | 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 45258* | 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 45259* | A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑥 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐶 𝐵 ≤ 𝑤) | ||
Theorem | fzdifsuc2 45260 | Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 13620, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘(𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzsscn 45261 | A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℂ | ||
Theorem | divcan8d 45262 | A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / (𝐴 · 𝐵)) = (1 / 𝐴)) | ||
Theorem | dmmcand 45263 | Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 · 𝐶)) = (𝐴 · 𝐶)) | ||
Theorem | fzssre 45264 | A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℝ | ||
Theorem | bccld 45265 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | leadd12dd 45266 | Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | fzssnn0 45267 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | xreqle 45268 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | xaddlidd 45269 | 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (0 +𝑒 𝐴) = 𝐴) | ||
Theorem | xadd0ge 45270 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | xrgtned 45271 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | xrleneltd 45272 | 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | xaddcomd 45273 | The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
Theorem | supxrre3 45274* | 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 45275* | 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 45276 | 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 45277* | 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 45278 | 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 45279 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | xrgepnfd 45280 | An extended real greater than or equal to +∞ is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → +∞ ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | xrge0nemnfd 45281 | A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≠ -∞) | ||
Theorem | supxrgere 45282* | 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 45283* | Lemma for iuneqfzuz 45284: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵) | ||
Theorem | iuneqfzuz 45284* | 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 45285 | Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)) | ||
Theorem | supxrgelem 45286* | 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 45287* | 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 45288* | 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 45289* | 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 45290 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 𝐴)) | ||
Theorem | nepnfltpnf 45291 | An extended real that is not +∞ is less than +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ≠ +∞) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 < +∞) | ||
Theorem | ltadd12dd 45292 | Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | nemnftgtmnft 45293 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) | ||
Theorem | xrgtso 45294 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ◡ < Or ℝ* | ||
Theorem | rpex 45295 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℝ+ ∈ V | ||
Theorem | xrge0ge0 45296 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ (0[,]+∞) → 0 ≤ 𝐴) | ||
Theorem | xrssre 45297 | 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 45298 | 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 45299 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Fun abs | ||
Theorem | infrpge 45300* | 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(𝐴, ℝ*, < ) +𝑒 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |