P. 406 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40501-40600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xralrple4 40501*	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 40502*	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 40503	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℤ)
Theorem	suplesup2 40504*	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 40505	𝑁 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 40506*	A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnn0 40507	The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ℕ ≠ ∅
Theorem	fzct 40508	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑁...𝑀) ≼ ω
Theorem	rpgtrecnn 40509*	Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴)
Theorem	fzossuz 40510	A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀)
Theorem	fzossz 40511	A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑀..^𝑁) ⊆ ℤ
Theorem	infrefilb 40512	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 40513	The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))
Theorem	xrralrecnnle 40514*	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 40515	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑁..^𝑀) ≼ ω
Theorem	frexr 40516	A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)
Theorem	nnrecrp 40517	The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+)
Theorem	qred 40518	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	reclt0d 40519	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) < 0)
Theorem	lt0neg1dd 40520	If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 0 < -𝐴)
Theorem	mnfled 40521	Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -∞ ≤ 𝐴)
Theorem	infxrcld 40522	The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	xrralrecnnge 40523*	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 40524	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0))
Theorem	ltmulneg 40525	Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 0)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶)))
Theorem	allbutfi 40526*	For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 40214 and eliuniin2 40236 (here, the precondition can be dropped; see eliuniincex 40225). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵    ⇒   ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)
Theorem	ltdiv23neg 40527	Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	xreqnltd 40528	A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 < 𝐵)
Theorem	mnfnre2 40529	Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ¬ -∞ ∈ ℝ
Theorem	uzssre 40530	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (ℤ≥‘𝑀) ⊆ ℝ
Theorem	zssxr 40531	The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℤ ⊆ ℝ*
Theorem	fisupclrnmpt 40532*	A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴)
Theorem	supxrunb3 40533*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	elfzod 40534	Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 < 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀..^𝑁))
Theorem	fimaxre4 40535*	A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)
Theorem	ren0 40536	The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℝ ≠ ∅
Theorem	eluzelz2 40537	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ)
Theorem	pnfnre2 40538	Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ¬ +∞ ∈ ℝ
Theorem	resabs2d 40539	Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	uzid2 40540	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzidd 40541	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	supxrleubrnmpt 40542*	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 40543	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℝ
Theorem	uzssd 40544	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	eluzd 40545	Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑍)
Theorem	elfzd 40546	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
Theorem	infxrlbrnmpt2 40547*	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 40548	An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞)))
Theorem	uz0 40549	The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅)
Theorem	eluzelz2d 40550	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℤ)
Theorem	infleinf2 40551*	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 40552*	"Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
Theorem	uzidd2 40553	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑍)
Theorem	uzssd2 40554	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabslelem 40555*	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 40556*	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 40557*	Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵))
Theorem	supxrrernmpt 40558*	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 40559*	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 40560*	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 40561*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞))
Theorem	uzn0d 40562	The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑍 ≠ ∅)
Theorem	uzssd3 40563	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabsle2 40564*	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 40565*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞))
Theorem	supxrre3rnmpt 40566*	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 40567*	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 40568*	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 40569	A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
Theorem	supxrmnf2 40570	Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < ))
Theorem	supxrcli 40571	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ⊆ ℝ*    ⇒   ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ*
Theorem	uzid3 40572	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁))
Theorem	infxrlesupxr 40573	The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 40587. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < ))
Theorem	xnegeqd 40574	Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵)
Theorem	xnegrecl 40575	The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
Theorem	xnegnegi 40576	Extended real version of negneg 10673. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -𝑒-𝑒𝐴 = 𝐴
Theorem	xnegeqi 40577	Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ -𝑒𝐴 = -𝑒𝐵
Theorem	nfxnegd 40578	Deduction version of nfxneg 40600. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥-𝑒𝐴)
Theorem	xnegnegd 40579	Extended real version of negnegd 10725. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -𝑒-𝑒𝐴 = 𝐴)
Theorem	uzred 40580	An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	xnegcli 40581	Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -𝑒𝐴 ∈ ℝ*
Theorem	supminfrnmpt 40582*	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	ceilged 40583	The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (⌈‘𝐴))
Theorem	infxrpnf 40584	Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < ))
Theorem	infxrrnmptcl 40585*	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 40586	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	supxrltinfxr 40587	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 40588	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	ceilcld 40589	Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (⌈‘𝐴) ∈ ℤ)
Theorem	supxrleubrnmptf 40590	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 40591	'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	zxrd 40592	An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	infxrgelbrnmpt 40593*	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 40594	Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 2) < 𝐴)
Theorem	uzssz2 40595	An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℤ
Theorem	leneg3d 40596	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	max2d 40597	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	uzn0bi 40598	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 40599	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
Theorem	nfxneg 40600	Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥-𝑒𝐴