P. 466 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46501-46600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zssxr 46501	The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℤ ⊆ ℝ*
Theorem	fisupclrnmpt 46502*	A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴)
Theorem	supxrunb3 46503*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	fimaxre4 46504*	A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)
Theorem	ren0 46505	The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℝ ≠ ∅
Theorem	eluzelz2 46506	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ)
Theorem	resabs2d 46507	Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	uzid2 46508	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	supxrleubrnmpt 46509*	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 46510	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℝ
Theorem	uzssd 46511	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	eluzd 46512	Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑍)
Theorem	infxrlbrnmpt2 46513*	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 46514	An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞)))
Theorem	uz0 46515	The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅)
Theorem	eluzelz2d 46516	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℤ)
Theorem	infleinf2 46517*	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 46518*	"Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
Theorem	uzidd2 46519	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑍)
Theorem	uzssd2 46520	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabslelem 46521*	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 46522*	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 46523*	Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵))
Theorem	supxrrernmpt 46524*	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 46525*	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 46526*	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 46527*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞))
Theorem	uzn0d 46528	The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑍 ≠ ∅)
Theorem	uzssd3 46529	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabsle2 46530*	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 46531*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞))
Theorem	supxrre3rnmpt 46532*	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 46533*	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 46534*	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 46535	A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
Theorem	supxrmnf2 46536	Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < ))
Theorem	supxrcli 46537	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ⊆ ℝ*    ⇒   ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ*
Theorem	uzid3 46538	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁))
Theorem	infxrlesupxr 46539	The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 46552. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < ))
Theorem	xnegeqd 46540	Equality of two extended numbers with -e in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -e𝐴 = -e𝐵)
Theorem	xnegrecl 46541	The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ ℝ → -e𝐴 ∈ ℝ)
Theorem	xnegnegi 46542	Extended real version of negneg 11611. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -e -e𝐴 = 𝐴
Theorem	xnegeqi 46543	Equality of two extended numbers with -e in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ -e𝐴 = -e𝐵
Theorem	nfxnegd 46544	Deduction version of nfxneg 46564. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 -e𝐴)
Theorem	xnegnegd 46545	Extended real version of negnegd 11663. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -e -e𝐴 = 𝐴)
Theorem	uzred 46546	An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	xnegcli 46547	Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -e𝐴 ∈ ℝ*
Theorem	supminfrnmpt 46548*	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 46549	Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < ))
Theorem	infxrrnmptcl 46550*	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 46551	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	supxrltinfxr 46552	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 46553	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	supxrleubrnmptf 46554	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 46555	'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	zxrd 46556	An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	infxrgelbrnmpt 46557*	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 46558	Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 2) < 𝐴)
Theorem	uzssz2 46559	An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℤ
Theorem	leneg3d 46560	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ( -𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	max2d 46561	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	uzn0bi 46562	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 46563	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ((𝐴 ∈ ℝ* ∧ -e𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
Theorem	nfxneg 46564	Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 -e𝐴
Theorem	uzxrd 46565	An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	infxrpnf2 46566	Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∖ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < ))
Theorem	supminfxr 46567*	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(𝐴, ℝ*, < ) = -einf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ*, < ))
Theorem	infrpgernmpt 46568*	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 (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) +e 𝐶))
Theorem	xnegre 46569	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ -e𝐴 ∈ ℝ))
Theorem	xnegrecl2d 46570	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → -e𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	uzxr 46571	An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ (ℤ≥‘𝑀) → 𝐴 ∈ ℝ*)
Theorem	supminfxr2 46572*	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(𝐴, ℝ*, < ) = -einf({𝑥 ∈ ℝ* ∣ -e𝑥 ∈ 𝐴}, ℝ*, < ))
Theorem	xnegred 46573	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ↔ -e𝐴 ∈ ℝ))
Theorem	supminfxrrnmpt 46574*	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 (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -einf(ran (𝑥 ∈ 𝐴 ↦ -e𝐵), ℝ*, < ))
Theorem	min1d 46575	The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	min2d 46576	The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	xrnpnfmnf 46577	An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ +∞)    ⇒   ⊢ (𝜑 → 𝐴 = -∞)
Theorem	uzsscn 46578	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (ℤ≥‘𝑀) ⊆ ℂ
Theorem	absimnre 46579	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 46580	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℂ
Theorem	xrtgcntopre 46581	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 46582	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 46583	The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ℝ+ ⊆ ℝ*
Theorem	monoordxrv 46584*	Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁))
Theorem	monoordxr 46585*	Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁))
Theorem	monoord2xrv 46586*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	monoord2xr 46587*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	xrpnf 46588*	An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴))
Theorem	xlenegcon1 46589	Extended real version of lenegcon1 11823. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ( -e𝐴 ≤ 𝐵 ↔ -e𝐵 ≤ 𝐴))
Theorem	xlenegcon2 46590	Extended real version of lenegcon2 11824. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ -e𝐵 ↔ 𝐵 ≤ -e𝐴))
Theorem	pimxrneun 46591	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 46592*	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‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))
Theorem	cvgcau 46593*	A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑗𝐹    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑋))
Theorem	cvgcaule 46594*	A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑗𝐹    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) ≤ 𝑋))
Theorem	rexanuz2nf 46595*	A simple counterexample related to theorem rexanuz2 15522, demonstrating the necessity of its disjoint variable constraints. Here, 𝑗 appears free in 𝜑, showing that without these constraints, rexanuz2 15522 and similar theorems would not hold (see rexanre 15519 and rexanuz 15518). (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ 𝑍 = ℕ0    &   ⊢ (𝜑 ↔ (𝑗 = 0 ∧ 𝑗 ≤ 𝑘))    &   ⊢ (𝜓 ↔ 0 < 𝑘)    ⇒   ⊢ ¬ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
21.47.4  Real intervals
Theorem	gtnelioc 46596	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 46597	An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵)
Theorem	ioondisj2 46598	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅)
Theorem	ioondisj1 46599	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅)
Theorem	ioogtlb 46600	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝐶)