![]() |
Metamath
Proof Explorer Theorem List (p. 445 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reclt0 44401 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ด < 0 โ (1 / ๐ด) < 0)) | ||
Theorem | ltmulneg 44402 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ < 0) โ โข (๐ โ (๐ด < ๐ต โ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ))) | ||
Theorem | allbutfi 44403* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 44091 and eliuniin2 44112 (here, the precondition can be dropped; see eliuniincex 44101). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข ๐ = (โคโฅโ๐) & โข ๐ด = โช ๐ โ ๐ โฉ ๐ โ (โคโฅโ๐)๐ต โ โข (๐ โ ๐ด โ โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โ ๐ต) | ||
Theorem | ltdiv23neg 44404 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต < 0) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ < 0) โ โข (๐ โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | xreqnltd 44405 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ ยฌ ๐ด < ๐ต) | ||
Theorem | mnfnre2 44406 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ยฌ -โ โ โ | ||
Theorem | zssxr 44407 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โค โ โ* | ||
Theorem | fisupclrnmpt 44408* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ Or ๐ด) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ต โ โ ) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ ๐ด) โ โข (๐ โ sup(ran (๐ฅ โ ๐ต โฆ ๐ถ), ๐ด, ๐ ) โ ๐ด) | ||
Theorem | supxrunb3 44409* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ โ sup(๐ด, โ*, < ) = +โ)) | ||
Theorem | elfzod 44410 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐พ โ (โคโฅโ๐)) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ < ๐) โ โข (๐ โ ๐พ โ (๐..^๐)) | ||
Theorem | fimaxre4 44411* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ) | ||
Theorem | ren0 44412 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โ โ โ | ||
Theorem | eluzelz2 44413 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐ โ โค) | ||
Theorem | resabs2d 44414 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ต โ ๐ถ) โ โข (๐ โ ((๐ด โพ ๐ต) โพ ๐ถ) = (๐ด โพ ๐ต)) | ||
Theorem | uzid2 44415 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ (โคโฅโ๐) โ ๐ โ (โคโฅโ๐)) | ||
Theorem | supxrleubrnmpt 44416* | 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 44417 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข ๐ โ โ | ||
Theorem | uzssd 44418 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ (โคโฅโ๐) โ (โคโฅโ๐)) | ||
Theorem | eluzd 44419 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โค ๐) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | infxrlbrnmpt2 44420* | 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 44421 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (๐ด โ โ โ (๐ด โ -โ โง ๐ด โ +โ))) | ||
Theorem | uz0 44422 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (ยฌ ๐ โ โค โ (โคโฅโ๐) = โ ) | ||
Theorem | eluzelz2d 44423 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ โ โค) | ||
Theorem | infleinf2 44424* | 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 44425* | "Unbounded below" expressed with < and with โค. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ค โ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ค โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) | ||
Theorem | uzidd2 44426 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | uzssd2 44427 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ (โคโฅโ๐) โ ๐) | ||
Theorem | rexabslelem 44428* | 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 44429* | 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 44430* | Given a "for all but finitely many" condition, the condition holds from ๐ on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข ๐ด = โช ๐ โ ๐ โฉ ๐ โ (โคโฅโ๐)๐ต & โข (๐ โ ๐ โ ๐ด) & โข ๐ = inf({๐ โ ๐ โฃ โ๐ โ (โคโฅโ๐)๐ โ ๐ต}, โ, < ) โ โข (๐ โ (๐ โ ๐ โง โ๐ โ (โคโฅโ๐)๐ โ ๐ต)) | ||
Theorem | supxrrernmpt 44431* | 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 44432* | 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 44433* | 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 44434* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ โ inf(๐ด, โ*, < ) = -โ)) | ||
Theorem | uzn0d 44435 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ โ ) | ||
Theorem | uzssd3 44436 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ (โคโฅโ๐) โ ๐) | ||
Theorem | rexabsle2 44437* | 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 44438* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ*) โ โข (๐ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ โ inf(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) = -โ)) | ||
Theorem | supxrre3rnmpt 44439* | 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 44440* | 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 44441* | 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 44442 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | supxrmnf2 44443 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ* โ sup((๐ด โ {-โ}), โ*, < ) = sup(๐ด, โ*, < )) | ||
Theorem | supxrcli 44444 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด โ โ* โ โข sup(๐ด, โ*, < ) โ โ* | ||
Theorem | uzid3 44445 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐ โ (โคโฅโ๐)) | ||
Theorem | infxrlesupxr 44446 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 44459. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด โ โ ) โ โข (๐ โ inf(๐ด, โ*, < ) โค sup(๐ด, โ*, < )) | ||
Theorem | xnegeqd 44447 | Equality of two extended numbers with -๐ in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ -๐๐ด = -๐๐ต) | ||
Theorem | xnegrecl 44448 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ โ -๐๐ด โ โ) | ||
Theorem | xnegnegi 44449 | Extended real version of negneg 11515. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด โ โ* โ โข -๐-๐๐ด = ๐ด | ||
Theorem | xnegeqi 44450 | Equality of two extended numbers with -๐ in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด = ๐ต โ โข -๐๐ด = -๐๐ต | ||
Theorem | nfxnegd 44451 | Deduction version of nfxneg 44471. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ โฒ๐ฅ๐ด) โ โข (๐ โ โฒ๐ฅ-๐๐ด) | ||
Theorem | xnegnegd 44452 | Extended real version of negnegd 11567. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ -๐-๐๐ด = ๐ด) | ||
Theorem | uzred 44453 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ด โ ๐) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | xnegcli 44454 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด โ โ* โ โข -๐๐ด โ โ* | ||
Theorem | supminfrnmpt 44455* | 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 44456 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ* โ inf((๐ด โช {+โ}), โ*, < ) = inf(๐ด, โ*, < )) | ||
Theorem | infxrrnmptcl 44457* | 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 44458 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โค -๐ต โ ๐ต โค -๐ด)) | ||
Theorem | supxrltinfxr 44459 | 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 44460 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ๐ด โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | supxrleubrnmptf 44461 | 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 44462 | 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ยฌ ๐ต โค ๐ด) โ โข (๐ โ ๐ด < ๐ต) | ||
Theorem | zxrd 44463 | An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โค) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | infxrgelbrnmpt 44464* | 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 44465 | Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด / 2) < ๐ด) | ||
Theorem | uzssz2 44466 | An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ = (โคโฅโ๐) โ โข ๐ โ โค | ||
Theorem | leneg3d 44467 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (-๐ด โค ๐ต โ -๐ต โค ๐ด)) | ||
Theorem | max2d 44468 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ๐ต โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | uzn0bi 44469 | 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 44470 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ((๐ด โ โ* โง -๐๐ด โ โ) โ ๐ด โ โ) | ||
Theorem | nfxneg 44471 | Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข โฒ๐ฅ๐ด โ โข โฒ๐ฅ-๐๐ด | ||
Theorem | uzxrd 44472 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ด โ ๐) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | infxrpnf2 44473 | Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ* โ inf((๐ด โ {+โ}), โ*, < ) = inf(๐ด, โ*, < )) | ||
Theorem | supminfxr 44474* | 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 44475* | 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 44476 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ* โ (๐ด โ โ โ -๐๐ด โ โ)) | ||
Theorem | xnegrecl2d 44477 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ -๐๐ด โ โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | uzxr 44478 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ (โคโฅโ๐) โ ๐ด โ โ*) | ||
Theorem | supminfxr2 44479* | 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 44480 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ (๐ด โ โ โ -๐๐ด โ โ)) | ||
Theorem | supminfxrrnmpt 44481* | 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 44482 | The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ด) | ||
Theorem | min2d 44483 | The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ต) | ||
Theorem | pnfged 44484 | Plus infinity is an upper bound for extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ ๐ด โค +โ) | ||
Theorem | xrnpnfmnf 44485 | An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ยฌ ๐ด โ โ) & โข (๐ โ ๐ด โ +โ) โ โข (๐ โ ๐ด = -โ) | ||
Theorem | uzsscn 44486 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข (โคโฅโ๐) โ โ | ||
Theorem | absimnre 44487 | 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 44488 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข ๐ = (โคโฅโ๐) โ โข ๐ โ โ | ||
Theorem | xrtgcntopre 44489 | 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 44490 | 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 44491 | The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
โข โ+ โ โ* | ||
Theorem | monoordxrv 44492* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ*) & โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ๐) โค (๐นโ(๐ + 1))) โ โข (๐ โ (๐นโ๐) โค (๐นโ๐)) | ||
Theorem | monoordxr 44493* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
โข โฒ๐๐ & โข โฒ๐๐น & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ*) & โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ๐) โค (๐นโ(๐ + 1))) โ โข (๐ โ (๐นโ๐) โค (๐นโ๐)) | ||
Theorem | monoord2xrv 44494* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ*) & โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ(๐ + 1)) โค (๐นโ๐)) โ โข (๐ โ (๐นโ๐) โค (๐นโ๐)) | ||
Theorem | monoord2xr 44495* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
โข โฒ๐๐ & โข โฒ๐๐น & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ*) & โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ(๐ + 1)) โค (๐นโ๐)) โ โข (๐ โ (๐นโ๐) โค (๐นโ๐)) | ||
Theorem | xrpnf 44496* | An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
โข (๐ด โ โ* โ (๐ด = +โ โ โ๐ฅ โ โ ๐ฅ โค ๐ด)) | ||
Theorem | xlenegcon1 44497 | Extended real version of lenegcon1 11723. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (-๐๐ด โค ๐ต โ -๐๐ต โค ๐ด)) | ||
Theorem | xlenegcon2 44498 | Extended real version of lenegcon2 11724. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค -๐๐ต โ ๐ต โค -๐๐ด)) | ||
Theorem | pimxrneun 44499 | 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 | caucvgbf 44500* | A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
โข โฒ๐๐น & โข โฒ๐๐น & โข ๐ = (โคโฅโ๐) โ โข ((๐ โ โค โง ๐น โ ๐) โ (๐น โ dom โ โ โ๐ฅ โ โ+ โ๐ โ ๐ โ๐ โ (โคโฅโ๐)((๐นโ๐) โ โ โง (absโ((๐นโ๐) โ (๐นโ๐))) < ๐ฅ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |