P. 457 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45601-45700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abslt2sqd 45601	Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵))    ⇒   ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2))
Theorem	qenom 45602	The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ℚ ≈ ω
Theorem	qct 45603	The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ℚ ≼ ω
Theorem	lenlteq 45604	'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xrred 45605	An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ -∞)    &   ⊢ (𝜑 → 𝐴 ≠ +∞)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rr2sscn2 45606	The cartesian square of ℝ is a subset of the cartesian square of ℂ. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ)
Theorem	infxr 45607*	The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵)
Theorem	infxrunb2 45608*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞))
Theorem	infxrbnd2 45609*	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 45610	Lemma for infleinf 45612, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2)))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2)))    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊))
Theorem	infleinflem2 45611	Lemma for infleinf 45612, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 < (𝑅 − 2))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1))    ⇒   ⊢ (𝜑 → 𝑍 < 𝑅)
Theorem	infleinf 45612*	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 45613*	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 45614*	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 45615	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℤ)
Theorem	suplesup2 45616*	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 45617	𝑁 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	nnn0 45618	The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ℕ ≠ ∅
Theorem	fzct 45619	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑁...𝑀) ≼ ω
Theorem	rpgtrecnn 45620*	Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴)
Theorem	fzossuz 45621	A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀)
Theorem	infxrrefi 45622	The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))
Theorem	xrralrecnnle 45623*	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 45624	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝑁..^𝑀) ≼ ω
Theorem	frexr 45625	A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)
Theorem	nnrecrp 45626	The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+)
Theorem	reclt0d 45627	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) < 0)
Theorem	lt0neg1dd 45628	If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 0 < -𝐴)
Theorem	infxrcld 45629	The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	xrralrecnnge 45630*	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 45631	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0))
Theorem	ltmulneg 45632	Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 0)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶)))
Theorem	allbutfi 45633*	For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 45339 and eliuniin2 45360 (here, the precondition can be dropped; see eliuniincex 45349). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵    ⇒   ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵)
Theorem	ltdiv23neg 45634	Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	xreqnltd 45635	A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 < 𝐵)
Theorem	mnfnre2 45636	Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ¬ -∞ ∈ ℝ
Theorem	zssxr 45637	The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℤ ⊆ ℝ*
Theorem	fisupclrnmpt 45638*	A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴)
Theorem	supxrunb3 45639*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	elfzod 45640	Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 < 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀..^𝑁))
Theorem	fimaxre4 45641*	A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)
Theorem	ren0 45642	The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ℝ ≠ ∅
Theorem	eluzelz2 45643	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ)
Theorem	resabs2d 45644	Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	uzid2 45645	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	supxrleubrnmpt 45646*	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 45647	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℝ
Theorem	uzssd 45648	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	eluzd 45649	Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑍)
Theorem	infxrlbrnmpt2 45650*	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 45651	An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞)))
Theorem	uz0 45652	The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅)
Theorem	eluzelz2d 45653	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℤ)
Theorem	infleinf2 45654*	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 45655*	"Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
Theorem	uzidd2 45656	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑍)
Theorem	uzssd2 45657	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabslelem 45658*	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 45659*	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 45660*	Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵))
Theorem	supxrrernmpt 45661*	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 45662*	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 45663*	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 45664*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞))
Theorem	uzn0d 45665	The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑍 ≠ ∅)
Theorem	uzssd3 45666	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍)
Theorem	rexabsle2 45667*	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 45668*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞))
Theorem	supxrre3rnmpt 45669*	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 45670*	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 45671*	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 45672	A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
Theorem	supxrmnf2 45673	Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < ))
Theorem	supxrcli 45674	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ⊆ ℝ*    ⇒   ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ*
Theorem	uzid3 45675	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁))
Theorem	infxrlesupxr 45676	The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 45689. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < ))
Theorem	xnegeqd 45677	Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵)
Theorem	xnegrecl 45678	The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
Theorem	xnegnegi 45679	Extended real version of negneg 11431. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -𝑒-𝑒𝐴 = 𝐴
Theorem	xnegeqi 45680	Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ -𝑒𝐴 = -𝑒𝐵
Theorem	nfxnegd 45681	Deduction version of nfxneg 45701. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥-𝑒𝐴)
Theorem	xnegnegd 45682	Extended real version of negnegd 11483. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -𝑒-𝑒𝐴 = 𝐴)
Theorem	uzred 45683	An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	xnegcli 45684	Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ -𝑒𝐴 ∈ ℝ*
Theorem	supminfrnmpt 45685*	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 45686	Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < ))
Theorem	infxrrnmptcl 45687*	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 45688	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	supxrltinfxr 45689	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 45690	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	supxrleubrnmptf 45691	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 45692	'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	zxrd 45693	An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	infxrgelbrnmpt 45694*	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 45695	Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 2) < 𝐴)
Theorem	uzssz2 45696	An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℤ
Theorem	leneg3d 45697	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	max2d 45698	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	uzn0bi 45699	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 45700	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)