Home | Metamath
Proof Explorer Theorem List (p. 417 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fzssre 41601 | A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℝ | ||
Theorem | elfzelzd 41602 | A member of a finite set of sequential integer is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | bccld 41603 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | leadd12dd 41604 | Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | fzssnn0 41605 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | xreqle 41606 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | xaddid2d 41607 | 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (0 +𝑒 𝐴) = 𝐴) | ||
Theorem | xadd0ge 41608 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | elfzolem1 41609 | 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 41610 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | xrleneltd 41611 | 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | xaddcomd 41612 | The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
Theorem | supxrre3 41613* | 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 41614* | 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 41615 | 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 41616* | 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 41617 | 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 41618 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | xrgepnfd 41619 | An extended real greater than or equal to +∞ is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → +∞ ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | xrge0nemnfd 41620 | A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≠ -∞) | ||
Theorem | supxrgere 41621* | 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 41622* | Lemma for iuneqfzuz 41623: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵) | ||
Theorem | iuneqfzuz 41623* | 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 41624 | Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)) | ||
Theorem | supxrgelem 41625* | 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 41626* | 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 41627* | 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 41628* | 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 41629 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 𝐴)) | ||
Theorem | nepnfltpnf 41630 | An extended real that is not +∞ is less than +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ≠ +∞) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 < +∞) | ||
Theorem | ltadd12dd 41631 | Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | nemnftgtmnft 41632 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) | ||
Theorem | xrgtso 41633 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ◡ < Or ℝ* | ||
Theorem | rpex 41634 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℝ+ ∈ V | ||
Theorem | xrge0ge0 41635 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ (0[,]+∞) → 0 ≤ 𝐴) | ||
Theorem | xrssre 41636 | 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 41637 | 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 41638 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Fun abs | ||
Theorem | infrpge 41639* | 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 41640* | 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.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | supsubc 41641* | The supremum function distributes over subtraction in a sense similar to that in supaddc 11608. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 − 𝐵)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 𝐵) = sup(𝐶, ℝ, < )) | ||
Theorem | xralrple2 41642* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. A variant on xralrple 12599. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ ((1 + 𝑥) · 𝐵))) | ||
Theorem | nnuzdisj 41643 | The first 𝑁 elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ | ||
Theorem | ltdivgt1 41644 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐵 ↔ (𝐴 / 𝐵) < 𝐴)) | ||
Theorem | xrltned 41645 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nnsplit 41646 | Express the set of positive integers as the disjoint (see nnuzdisj 41643) union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | divdiv3d 41647 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐶 · 𝐵))) | ||
Theorem | abslt2sqd 41648 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵)) ⇒ ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2)) | ||
Theorem | qenom 41649 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≈ ω | ||
Theorem | qct 41650 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≼ ω | ||
Theorem | xrltnled 41651 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | lenlteq 41652 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrred 41653 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ -∞) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rr2sscn2 41654 | The cartesian square of ℝ is a subset of the cartesian square of ℂ. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ) | ||
Theorem | infxr 41655* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | infxrunb2 41656* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | infxrbnd2 41657* | The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ -∞ < inf(𝐴, ℝ*, < ))) | ||
Theorem | infleinflem1 41658 | Lemma for infleinf 41660, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2))) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2))) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊)) | ||
Theorem | infleinflem2 41659 | Lemma for infleinf 41660, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < (𝑅 − 2)) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1)) ⇒ ⊢ (𝜑 → 𝑍 < 𝑅) | ||
Theorem | infleinf 41660* | If any element of 𝐵 can be approximated from above by members of 𝐴, then the infimum of 𝐴 is less than or equal to the infimum of 𝐵. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, < )) | ||
Theorem | xralrple4 41661* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + (𝑥↑𝑁)))) | ||
Theorem | xralrple3 41662* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + (𝐶 · 𝑥)))) | ||
Theorem | eluzelzd 41663 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | suplesup2 41664* | If any element of 𝐴 is less than or equal to an element in 𝐵, then the supremum of 𝐴 is less than or equal to the supremum of 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | recnnltrp 41665 | 𝑁 is a natural number large enough that its reciprocal is smaller than the given positive 𝐸. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) ⇒ ⊢ (𝐸 ∈ ℝ+ → (𝑁 ∈ ℕ ∧ (1 / 𝑁) < 𝐸)) | ||
Theorem | fiminre2 41666* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnn0 41667 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ℕ ≠ ∅ | ||
Theorem | fzct 41668 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁...𝑀) ≼ ω | ||
Theorem | rpgtrecnn 41669* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) | ||
Theorem | fzossuz 41670 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | infrefilb 41671 | The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴) | ||
Theorem | infxrrefi 41672 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < )) | ||
Theorem | xrralrecnnle 41673* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ 𝐴 ≤ (𝐵 + (1 / 𝑛)))) | ||
Theorem | fzoct 41674 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁..^𝑀) ≼ ω | ||
Theorem | frexr 41675 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | ||
Theorem | nnrecrp 41676 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+) | ||
Theorem | qred 41677 | A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | reclt0d 41678 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) < 0) | ||
Theorem | lt0neg1dd 41679 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 0 < -𝐴) | ||
Theorem | mnfled 41680 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -∞ ≤ 𝐴) | ||
Theorem | infxrcld 41681 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | xrralrecnnge 41682* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐴 − (1 / 𝑛)) ≤ 𝐵)) | ||
Theorem | reclt0 41683 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0)) | ||
Theorem | ltmulneg 41684 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶))) | ||
Theorem | allbutfi 41685* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 41385 and eliuniin2 41406 (here, the precondition can be dropped; see eliuniincex 41395). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) | ||
Theorem | ltdiv23neg 41686 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | xreqnltd 41687 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐵) | ||
Theorem | mnfnre2 41688 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ¬ -∞ ∈ ℝ | ||
Theorem | uzssre 41689 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (ℤ≥‘𝑀) ⊆ ℝ | ||
Theorem | zssxr 41690 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℤ ⊆ ℝ* | ||
Theorem | fisupclrnmpt 41691* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supxrunb3 41692* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | elfzod 41693 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 < 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀..^𝑁)) | ||
Theorem | fimaxre4 41694* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) | ||
Theorem | ren0 41695 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℝ ≠ ∅ | ||
Theorem | eluzelz2 41696 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ) | ||
Theorem | resabs2d 41697 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)) | ||
Theorem | uzid2 41698 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | supxrleubrnmpt 41699* | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | uzssre2 41700 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℝ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |