Home | Metamath
Proof Explorer Theorem List (p. 435 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eluzd 43401 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑍) | ||
Theorem | infxrlbrnmpt2 43402* | A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐷) | ||
Theorem | xrre4 43403 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞))) | ||
Theorem | uz0 43404 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅) | ||
Theorem | eluzelz2d 43405 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | infleinf2 43406* | If any element in 𝐵 is greater than or equal to an element in 𝐴, then the infimum of 𝐴 is less than or equal to the infimum of 𝐵. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, < )) | ||
Theorem | unb2ltle 43407* | "Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | ||
Theorem | uzidd2 43408 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑍) | ||
Theorem | uzssd2 43409 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabslelem 43410* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) | ||
Theorem | rexabsle 43411* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) | ||
Theorem | allbutfiinf 43412* | Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) | ||
Theorem | supxrrernmpt 43413* | The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | suprleubrnmpt 43414* | The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | infrnmptle 43415* | An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐶), ℝ*, < )) | ||
Theorem | infxrunb3 43416* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | uzn0d 43417 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑍 ≠ ∅) | ||
Theorem | uzssd3 43418 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabsle2 43419* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵))) | ||
Theorem | infxrunb3rnmpt 43420* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞)) | ||
Theorem | supxrre3rnmpt 43421* | The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) | ||
Theorem | uzublem 43422* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝑋 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) & ⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝐾)𝐵 ≤ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) | ||
Theorem | uzub 43423* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝐵 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥)) | ||
Theorem | ssrexr 43424 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℝ*) | ||
Theorem | supxrmnf2 43425 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrcli 43426 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ⊆ ℝ* ⇒ ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ* | ||
Theorem | uzid3 43427 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁)) | ||
Theorem | infxrlesupxr 43428 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 43441. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | xnegeqd 43429 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵) | ||
Theorem | xnegrecl 43430 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ) | ||
Theorem | xnegnegi 43431 | Extended real version of negneg 11384. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒-𝑒𝐴 = 𝐴 | ||
Theorem | xnegeqi 43432 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝑒𝐴 = -𝑒𝐵 | ||
Theorem | nfxnegd 43433 | Deduction version of nfxneg 43453. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝑒𝐴) | ||
Theorem | xnegnegd 43434 | Extended real version of negnegd 11436. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | uzred 43435 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | xnegcli 43436 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒𝐴 ∈ ℝ* | ||
Theorem | supminfrnmpt 43437* | The indexed supremum of a bounded-above set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) = -inf(ran (𝑥 ∈ 𝐴 ↦ -𝐵), ℝ, < )) | ||
Theorem | infxrpnf 43438 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < )) | ||
Theorem | infxrrnmptcl 43439* | The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ∈ ℝ*) | ||
Theorem | leneg2d 43440 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) | ||
Theorem | supxrltinfxr 43441 | The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ sup(∅, ℝ*, < ) < inf(∅, ℝ*, < ) | ||
Theorem | max1d 43442 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | supxrleubrnmptf 43443 | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | nleltd 43444 | 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | zxrd 43445 | An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | infxrgelbrnmpt 43446* | The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐶 ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵)) | ||
Theorem | rphalfltd 43447 | Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) < 𝐴) | ||
Theorem | uzssz2 43448 | An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℤ | ||
Theorem | leneg3d 43449 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) | ||
Theorem | max2d 43450 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | uzn0bi 43451 | The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((ℤ≥‘𝑀) ≠ ∅ ↔ 𝑀 ∈ ℤ) | ||
Theorem | xnegrecl2 43452 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) | ||
Theorem | nfxneg 43453 | Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥-𝑒𝐴 | ||
Theorem | uzxrd 43454 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | infxrpnf2 43455 | Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∖ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < )) | ||
Theorem | supminfxr 43456* | The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ*, < )) | ||
Theorem | infrpgernmpt 43457* | The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐵 ≤ (inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) +𝑒 𝐶)) | ||
Theorem | xnegre 43458 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ)) | ||
Theorem | xnegrecl2d 43459 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | uzxr 43460 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ (ℤ≥‘𝑀) → 𝐴 ∈ ℝ*) | ||
Theorem | supminfxr2 43461* | The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ* ∣ -𝑒𝑥 ∈ 𝐴}, ℝ*, < )) | ||
Theorem | xnegred 43462 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ)) | ||
Theorem | supminfxrrnmpt 43463* | The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -𝑒inf(ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, < )) | ||
Theorem | min1d 43464 | The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | min2d 43465 | The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | pnfged 43466 | Plus infinity is an upper bound for extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ +∞) | ||
Theorem | xrnpnfmnf 43467 | An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 = -∞) | ||
Theorem | uzsscn 43468 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (ℤ≥‘𝑀) ⊆ ℂ | ||
Theorem | absimnre 43469 | The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+) | ||
Theorem | uzsscn2 43470 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℂ | ||
Theorem | xrtgcntopre 43471 | The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ((ordTop‘ ≤ ) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ) | ||
Theorem | absimlere 43472 | The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | rpssxr 43473 | The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ℝ+ ⊆ ℝ* | ||
Theorem | monoordxrv 43474* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) | ||
Theorem | monoordxr 43475* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) | ||
Theorem | monoord2xrv 43476* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | monoord2xr 43477* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | xrpnf 43478* | An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴)) | ||
Theorem | xlenegcon1 43479 | Extended real version of lenegcon1 11592. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ 𝐴)) | ||
Theorem | xlenegcon2 43480 | Extended real version of lenegcon2 11593. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ -𝑒𝐵 ↔ 𝐵 ≤ -𝑒𝐴)) | ||
Theorem | pimxrneun 43481 | The preimage of a set of extended reals that does not contain a value 𝐶 is the union of the preimage of the elements smaller than 𝐶 and the preimage of the subset of elements larger than 𝐶. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶} = ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) | ||
Theorem | gtnelioc 43482 | A real number larger than the upper bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | ioossioc 43483 | An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵) | ||
Theorem | ioondisj2 43484 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioondisj1 43485 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioogtlb 43486 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝐶) | ||
Theorem | evthiccabs 43487* | Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑤)))) | ||
Theorem | ltnelicc 43488 | A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 < 𝐴) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | eliood 43489 | Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) | ||
Theorem | iooabslt 43490 | An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < 𝐵) | ||
Theorem | gtnelicc 43491 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iooinlbub 43492 | An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅ | ||
Theorem | iocgtlb 43493 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐶) | ||
Theorem | iocleub 43494 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | eliccd 43495 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | eliccre 43496 | A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | eliooshift 43497 | Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)(,)(𝐶 + 𝐷)))) | ||
Theorem | eliocd 43498 | Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | icoltub 43499 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵) | ||
Theorem | eliocre 43500 | A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |