P. 121 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12001-12100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	maxle1 12001	The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
Theorem	maxle2 12002	The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < ))
Theorem	maxleast 12003	The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶)
Theorem	maxleastb 12004	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	maxleastlt 12005	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ, < ))) → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	maxleb 12006	Equivalence of ≤ and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
Theorem	dfabsmax 12007	Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = sup({𝐴, -𝐴}, ℝ, < ))
Theorem	maxltsup 12008	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	max0addsup 12009	The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
⊢ (𝐴 ∈ ℝ → (sup({𝐴, 0}, ℝ, < ) + sup({ -𝐴, 0}, ℝ, < )) = (abs‘𝐴))
Theorem	rexanre 12010*	Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓))))
Theorem	rexico 12011*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	maxclpr 12012	The maximum of two real numbers is one of those numbers if and only if dichotomy (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) holds. For example, this can be combined with zletric 9700 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ∈ {𝐴, 𝐵} ↔ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)))
Theorem	rpmaxcl 12013	The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℝ+)
Theorem	zmaxcl 12014	The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℤ)
Theorem	nn0maxcl 12015	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℕ0)
Theorem	2zsupmax 12016	Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	fimaxre2 12017*	A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	negfi 12018*	The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin)
Theorem	fiidxsupcl 12019*	A set of integers indexed by a finite set has an upper bound. (Contributed by Jim Kingdon, 8-Sep-2026.)
⊢ (𝜑 → 𝐹:𝐴⟶ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ≤ 𝑥)
4.8.6  The minimum of two real numbers
Theorem	mincom 12020	The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ inf({𝐴, 𝐵}, ℝ, < ) = inf({𝐵, 𝐴}, ℝ, < )
Theorem	minmax 12021	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) = -sup({ -𝐴, -𝐵}, ℝ, < ))
Theorem	mincl 12022	The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ∈ ℝ)
Theorem	min1inf 12023	The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ≤ 𝐴)
Theorem	min2inf 12024	The minimum of two numbers is less than or equal to the second. (Contributed by Jim Kingdon, 9-Feb-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ≤ 𝐵)
Theorem	lemininf 12025	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ inf({𝐵, 𝐶}, ℝ, < ) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶)))
Theorem	ltmininf 12026	Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < inf({𝐵, 𝐶}, ℝ, < ) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	minabs 12027	The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) − (abs‘(𝐴 − 𝐵))) / 2))
Theorem	minclpr 12028	The minimum of two real numbers is one of those numbers if and only if dichotomy (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) holds. For example, this can be combined with zletric 9700 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 23-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (inf({𝐴, 𝐵}, ℝ, < ) ∈ {𝐴, 𝐵} ↔ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)))
Theorem	rpmincl 12029	The minumum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → inf({𝐴, 𝐵}, ℝ, < ) ∈ ℝ+)
Theorem	zmincl 12030	The minumum of two integers is an integer. (Contributed by Jim Kingdon, 27-Aug-2026.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) ∈ ℤ)
Theorem	bdtrilem 12031	Lemma for bdtri 12032. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶))) ≤ (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))))
Theorem	bdtri 12032	Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → inf({(𝐴 + 𝐵), 𝐶}, ℝ, < ) ≤ (inf({𝐴, 𝐶}, ℝ, < ) + inf({𝐵, 𝐶}, ℝ, < )))
Theorem	mul0inf 12033	Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11851 and mulap0bd 8994 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = 0 ↔ inf({(abs‘𝐴), (abs‘𝐵)}, ℝ, < ) = 0))
Theorem	mingeb 12034	Equivalence of ≤ and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ inf({𝐴, 𝐵}, ℝ, < ) = 𝐴))
Theorem	2zinfmin 12035	Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐴, 𝐵))
4.8.7  The maximum of two extended reals
Theorem	xrmaxleim 12036	Value of maximum when we know which extended real is larger. (Contributed by Jim Kingdon, 25-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ*, < ) = 𝐵))
Theorem	xrmaxiflemcl 12037	Lemma for xrmaxif 12043. Closure. (Contributed by Jim Kingdon, 29-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) ∈ ℝ*)
Theorem	xrmaxifle 12038	An upper bound for {𝐴, 𝐵} in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))
Theorem	xrmaxiflemab 12039	Lemma for xrmaxif 12043. A variation of xrmaxleim 12036- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
Theorem	xrmaxiflemlub 12040	Lemma for xrmaxif 12043. A least upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 28-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 < if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	xrmaxiflemcom 12041	Lemma for xrmaxif 12043. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
Theorem	xrmaxiflemval 12042*	Lemma for xrmaxif 12043. Value of the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)
⊢ 𝑀 = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑀 ∈ ℝ* ∧ ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑀 < 𝑥 ∧ ∀𝑥 ∈ ℝ* (𝑥 < 𝑀 → ∃𝑧 ∈ {𝐴, 𝐵}𝑥 < 𝑧)))
Theorem	xrmaxif 12043	Maximum of two extended reals in terms of if expressions. (Contributed by Jim Kingdon, 26-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → sup({𝐴, 𝐵}, ℝ*, < ) = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))
Theorem	xrmaxcl 12044	The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → sup({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ*)
Theorem	xrmax1sup 12045	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ*, < ))
Theorem	xrmax2sup 12046	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ*, < ))
Theorem	xrmaxrecl 12047	The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) = sup({𝐴, 𝐵}, ℝ, < ))
Theorem	xrmaxleastlt 12048	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ*, < ))) → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	xrltmaxsup 12049	The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 < sup({𝐴, 𝐵}, ℝ*, < ) ↔ (𝐶 < 𝐴 ∨ 𝐶 < 𝐵)))
Theorem	xrmaxltsup 12050	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	xrmaxlesup 12051	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (sup({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	xrmaxaddlem 12052	Lemma for xrmaxadd 12053. The case where 𝐴 is real. (Contributed by Jim Kingdon, 11-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +e 𝐵), (𝐴 +e 𝐶)}, ℝ*, < ) = (𝐴 +e sup({𝐵, 𝐶}, ℝ*, < )))
Theorem	xrmaxadd 12053	Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +e 𝐵), (𝐴 +e 𝐶)}, ℝ*, < ) = (𝐴 +e sup({𝐵, 𝐶}, ℝ*, < )))
4.8.8  The minimum of two extended reals
Theorem	xrnegiso 12054	Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ -e𝑥)    ⇒   ⊢ (𝐹 Isom < , ◡ < (ℝ*, ℝ*) ∧ ◡𝐹 = 𝐹)
Theorem	infxrnegsupex 12055*	The infimum of a set of extended reals 𝐴 is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = -esup({𝑧 ∈ ℝ* ∣ -e𝑧 ∈ 𝐴}, ℝ*, < ))
Theorem	xrnegcon1d 12056	Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (-e𝐴 = 𝐵 ↔ -e𝐵 = 𝐴))
Theorem	xrminmax 12057	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) = -esup({-e𝐴, -e𝐵}, ℝ*, < ))
Theorem	xrmincl 12058	The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ*)
Theorem	xrmin1inf 12059	The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐴)
Theorem	xrmin2inf 12060	The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐵)
Theorem	xrmineqinf 12061	The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → inf({𝐴, 𝐵}, ℝ*, < ) = 𝐵)
Theorem	xrltmininf 12062	Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < inf({𝐵, 𝐶}, ℝ*, < ) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	xrlemininf 12063	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ≤ inf({𝐵, 𝐶}, ℝ*, < ) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶)))
Theorem	xrminltinf 12064	Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (inf({𝐵, 𝐶}, ℝ*, < ) < 𝐴 ↔ (𝐵 < 𝐴 ∨ 𝐶 < 𝐴)))
Theorem	xrminrecl 12065	The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ*, < ) = inf({𝐴, 𝐵}, ℝ, < ))
Theorem	xrminrpcl 12066	The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → inf({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ+)
Theorem	xrminadd 12067	Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → inf({(𝐴 +e 𝐵), (𝐴 +e 𝐶)}, ℝ*, < ) = (𝐴 +e inf({𝐵, 𝐶}, ℝ*, < )))
Theorem	xrbdtri 12068	Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → inf({(𝐴 +e 𝐵), 𝐶}, ℝ*, < ) ≤ (inf({𝐴, 𝐶}, ℝ*, < ) +e inf({𝐵, 𝐶}, ℝ*, < )))
Theorem	iooinsup 12069	Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (sup({𝐴, 𝐶}, ℝ*, < )(,)inf({𝐵, 𝐷}, ℝ*, < )))
4.9  Elementary limits and convergence
4.9.1  Limits
Syntax	cli 12070	Extend class notation with convergence relation for limits.
class ⇝
Definition	df-clim 12071*	Define the limit relation for complex number sequences. See clim 12073 for its relational expression. (Contributed by NM, 28-Aug-2005.)
⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
Theorem	climrel 12072	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ Rel ⇝
Theorem	clim 12073*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑗 such that the absolute difference of any later complex number in the sequence and the limit is less than 𝑥. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	climcl 12074	Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
Theorem	clim2 12075*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 12073. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	clim2c 12076*	Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	clim0 12077*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥)))
Theorem	clim0c 12078*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥))
Theorem	climi 12079*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝐶))
Theorem	climi2 12080*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	climi0 12081*	Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 0)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝐶)
Theorem	climconst 12082*	An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
Theorem	climconst2 12083	A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ≥‘𝑀) ⊆ 𝑍    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴)
Theorem	climz 12084	The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ × {0}) ⇝ 0
Theorem	climuni 12085	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵) → 𝐴 = 𝐵)
Theorem	fclim 12086	The limit relation is function-like, and with codomian the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ⇝ :dom ⇝ ⟶ℂ
Theorem	climdm 12087	Two ways to express that a function has a limit. (The expression ( ⇝ ‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘𝐹))
Theorem	climeu 12088*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥)
Theorem	climreu 12089*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥)
Theorem	climmo 12090*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
⊢ ∃*𝑥 𝐹 ⇝ 𝑥
Theorem	climeq 12091*	Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climmpt 12092*	Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	2clim 12093*	If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	climshftlemg 12094	A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴))
Theorem	climres 12095	A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climshft 12096	A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 shift 𝑀) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	serclim0 12097	The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ (𝑀 ∈ ℤ → seq𝑀( + , ((ℤ≥‘𝑀) × {0})) ⇝ 0)
Theorem	climshft2 12098*	A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climabs0 12099*	Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0))
Theorem	climcn1 12100*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐵 ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐹‘𝐴))