P. 428 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42701-42800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fconst7 42701*	An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵}))
20.37.3  Ordering on real numbers - Real and complex numbers basic operations
Theorem	sub2times 42702	Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴)
Theorem	abssubrp 42703	The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+)
Theorem	elfzfzo 42704	Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝑀..^𝑁) ↔ (𝐴 ∈ (𝑀...𝑁) ∧ 𝐴 < 𝑁))
Theorem	oddfl 42705	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1))
Theorem	abscosbd 42706	Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1)
Theorem	mul13d 42707	Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴)))
Theorem	negpilt0 42708	Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ -π < 0
Theorem	dstregt0 42709*	A complex number 𝐴 that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦)))
Theorem	subadd4b 42710	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵)))
Theorem	xrlttri5d 42711	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	neglt 42712	The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴)
Theorem	zltlesub 42713	If an integer 𝑁 is less than or equal to a real, and we subtract a quantity less than 1, then 𝑁 is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 1)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑁 ≤ (𝐴 − 𝐵))
Theorem	divlt0gt0d 42714	The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) < 0)
Theorem	subsub23d 42715	Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵))
Theorem	2timesgt 42716	Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 < (2 · 𝐴))
Theorem	reopn 42717	The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ℝ ∈ (topGen‘ran (,))
Theorem	elfzop1le2 42718	A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 + 1) ≤ 𝑁)
Theorem	sub31 42719	Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐶 − (𝐵 − 𝐴)))
Theorem	nnne1ge2 42720	A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁)
Theorem	lefldiveq 42721	A closed enough, smaller real 𝐶 has the same floor of 𝐴 when both are divided by 𝐵. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,]𝐴))    ⇒   ⊢ (𝜑 → (⌊‘(𝐴 / 𝐵)) = (⌊‘(𝐶 / 𝐵)))
Theorem	negsubdi3d 42722	Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 − -𝐵))
Theorem	ltdiv2dd 42723	Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐵) < (𝐶 / 𝐴))
Theorem	abssinbd 42724	Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → (abs‘(sin‘𝐴)) ≤ 1)
Theorem	halffl 42725	Floor of (1 / 2). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (⌊‘(1 / 2)) = 0
Theorem	monoords 42726*	Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐼 < 𝐽)    ⇒   ⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽))
Theorem	hashssle 42727	The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 14052, and hashssle 42727 should be deleted afterwards.
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴))
Theorem	lttri5d 42728	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	fzisoeu 42729*	A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 14104 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐻 ∈ Fin)    &   ⊢ (𝜑 → < Or 𝐻)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1))    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
Theorem	lt3addmuld 42730	If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐷)    &   ⊢ (𝜑 → 𝐵 < 𝐷)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) < (3 · 𝐷))
Theorem	absnpncan2d 42731	Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐷)) ≤ (((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷))))
Theorem	fperiodmullem 42732*	A function with period 𝑇 is also periodic with period nonnegative multiple of 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋))
Theorem	fperiodmul 42733*	A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋))
Theorem	upbdrech 42734*	Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    &   ⊢ 𝐶 = sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶))
Theorem	lt4addmuld 42735	If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐸)    &   ⊢ (𝜑 → 𝐵 < 𝐸)    &   ⊢ (𝜑 → 𝐶 < 𝐸)    &   ⊢ (𝜑 → 𝐷 < 𝐸)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) + 𝐷) < (4 · 𝐸))
Theorem	absnpncan3d 42736	Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐸)) ≤ ((((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷))) + (abs‘(𝐷 − 𝐸))))
Theorem	upbdrech2 42737*	Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    &   ⊢ 𝐶 = if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < ))    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶))
Theorem	ssfiunibd 42738*	A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑥 𝐵 ≤ 𝑦)    &   ⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐶 𝐵 ≤ 𝑤)
Theorem	fzdifsuc2 42739	Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 13245, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑁 ∈ (ℤ≥‘(𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)}))
Theorem	fzsscn 42740	A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑀...𝑁) ⊆ ℂ
Theorem	divcan8d 42741	A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 / (𝐴 · 𝐵)) = (1 / 𝐴))
Theorem	dmmcand 42742	Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 · 𝐶)) = (𝐴 · 𝐶))
Theorem	fzssre 42743	A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑀...𝑁) ⊆ ℝ
Theorem	bccld 42744	A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ0)
Theorem	leadd12dd 42745	Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))
Theorem	fzssnn0 42746	A finite set of sequential integers that is a subset of ℕ0. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (0...𝑁) ⊆ ℕ0
Theorem	xreqle 42747	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵)
Theorem	xaddid2d 42748	0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (0 +𝑒 𝐴) = 𝐴)
Theorem	xadd0ge 42749	A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 +𝑒 𝐵))
Theorem	elfzolem1 42750	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 42751	'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	xrleneltd 42752	'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	xaddcomd 42753	The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴))
Theorem	supxrre3 42754*	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 42755*	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 42756	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 42757*	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 42758	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 42759	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	xrgepnfd 42760	An extended real greater than or equal to +∞ is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → +∞ ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = +∞)
Theorem	xrge0nemnfd 42761	A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	supxrgere 42762*	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 42763*	Lemma for iuneqfzuz 42764: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    ⇒   ⊢ (∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)𝐴 = ∪ 𝑛 ∈ (𝑁...𝑚)𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵)
Theorem	iuneqfzuz 42764*	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 42765	Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷))
Theorem	supxrgelem 42766*	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 42767*	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 42768*	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 42769*	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 42770	A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 𝐴))
Theorem	nepnfltpnf 42771	An extended real that is not +∞ is less than +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ≠ +∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → 𝐴 < +∞)
Theorem	ltadd12dd 42772	Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐶)    &   ⊢ (𝜑 → 𝐵 < 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷))
Theorem	nemnftgtmnft 42773	An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → -∞ < 𝐴)
Theorem	xrgtso 42774	'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ◡ < Or ℝ*
Theorem	rpex 42775	The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ℝ+ ∈ V
Theorem	xrge0ge0 42776	A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝐴 ∈ (0[,]+∞) → 0 ≤ 𝐴)
Theorem	xrssre 42777	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 42778	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 42779	The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Fun abs
Theorem	infrpge 42780*	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 42781*	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 42782*	The supremum function distributes over subtraction in a sense similar to that in supaddc 11872. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 − 𝐵)}    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 𝐵) = sup(𝐶, ℝ, < ))
Theorem	xralrple2 42783*	Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. A variant on xralrple 12868. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ ((1 + 𝑥) · 𝐵)))
Theorem	nnuzdisj 42784	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 42785	Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐵 ↔ (𝐴 / 𝐵) < 𝐴))
Theorem	xrltned 42786	'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	nnsplit 42787	Express the set of positive integers as the disjoint (see nnuzdisj 42784) union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
Theorem	divdiv3d 42788	Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐶 · 𝐵)))
Theorem	abslt2sqd 42789	Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵))    ⇒   ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2))
Theorem	qenom 42790	The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ℚ ≈ ω
Theorem	qct 42791	The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ℚ ≼ ω
Theorem	xrltnled 42792	'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
Theorem	lenlteq 42793	'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xrred 42794	An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ -∞)    &   ⊢ (𝜑 → 𝐴 ≠ +∞)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rr2sscn2 42795	The cartesian square of ℝ is a subset of the cartesian square of ℂ. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ)
Theorem	infxr 42796*	The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵)
Theorem	infxrunb2 42797*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞))
Theorem	infxrbnd2 42798*	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 42799	Lemma for infleinf 42801, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2)))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2)))    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊))
Theorem	infleinflem2 42800	Lemma for infleinf 42801, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 < (𝑅 − 2))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1))    ⇒   ⊢ (𝜑 → 𝑍 < 𝑅)