P. 97 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	9t6e54 9601	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 9602	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 9603	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 9604	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	9t11e99 9605	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
⊢ (9 · ;11) = ;99
Theorem	9lt10 9606	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 9 < ;10
Theorem	8lt10 9607	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 8 < ;10
Theorem	7lt10 9608	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 7 < ;10
Theorem	6lt10 9609	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 6 < ;10
Theorem	5lt10 9610	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 5 < ;10
Theorem	4lt10 9611	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 4 < ;10
Theorem	3lt10 9612	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 3 < ;10
Theorem	2lt10 9613	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 2 < ;10
Theorem	1lt10 9614	1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 1 < ;10
Theorem	decbin0 9615	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 9616	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 9617	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
Theorem	halfthird 9618	Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ ((1 / 2) − (1 / 3)) = (1 / 6)
Theorem	5recm6rec 9619	One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30)
4.4.11  Upper sets of integers
Syntax	cuz 9620	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀".
class ℤ≥
Definition	df-uz 9621*	Define a function whose value at 𝑗 is the semi-infinite set of contiguous integers starting at 𝑗, which we will also call the upper integers starting at 𝑗. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". See uzval 9622 for its value, uzssz 9640 for its relationship to ℤ, nnuz 9656 and nn0uz 9655 for its relationships to ℕ and ℕ0, and eluz1 9624 and eluz2 9626 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 9622*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 9623	The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ℤ≥:ℤ⟶𝒫 ℤ
Theorem	eluz1 9624	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 9625	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 9626	Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show 𝑀 ∈ ℤ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluz1i 9627	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 9628	An integer in an upper set of integers is an element of an upper set of integers with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴) → (𝐶 ∈ (ℤ≥‘𝐴) → 𝐶 ∈ (ℤ≥‘𝐵)))
Theorem	eluzelz 9629	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
Theorem	eluzelre 9630	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
Theorem	eluzelcn 9631	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)
Theorem	eluzle 9632	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)
Theorem	eluz 9633	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
Theorem	uzid 9634	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzidd 9635	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzn0 9636	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅)
Theorem	uztrn 9637	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁))
Theorem	uztrn2 9638	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝐾)    ⇒   ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)
Theorem	uzneg 9639	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁))
Theorem	uzssz 9640	An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (ℤ≥‘𝑀) ⊆ ℤ
Theorem	uzss 9641	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	uztric 9642	Trichotomy of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jun-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁)))
Theorem	uz11 9643	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁))
Theorem	eluzp1m1 9644	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
Theorem	eluzp1l 9645	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	eluzp1p1 9646	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
Theorem	eluzaddi 9647	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsubi 9648	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	eluzadd 9649	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsub 9650	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	uzm1 9651	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀)))
Theorem	uznn0sub 9652	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0)
Theorem	uzin 9653	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	uzp1 9654	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
Theorem	nn0uz 9655	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ0 = (ℤ≥‘0)
Theorem	nnuz 9656	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ = (ℤ≥‘1)
Theorem	elnnuz 9657	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))
Theorem	elnn0uz 9658	A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
Theorem	eluz2nn 9659	An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)
Theorem	eluz4eluz2 9660	An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ (ℤ≥‘2))
Theorem	eluz4nn 9661	An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ)
Theorem	eluzge2nn0 9662	If an integer is greater than or equal to 2, then it is a nonnegative integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℕ0)
Theorem	eluz2n0 9663	An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0)
Theorem	uzuzle23 9664	An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝐴 ∈ (ℤ≥‘3) → 𝐴 ∈ (ℤ≥‘2))
Theorem	eluzge3nn 9665	If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ)
Theorem	uz3m2nn 9666	An integer greater than or equal to 3 decreased by 2 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ)
Theorem	1eluzge0 9667	1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 1 ∈ (ℤ≥‘0)
Theorem	2eluzge0 9668	2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 2 ∈ (ℤ≥‘0)
Theorem	2eluzge1 9669	2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 2 ∈ (ℤ≥‘1)
Theorem	uznnssnn 9670	The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ)
Theorem	raluz 9671*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	raluz2 9672*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	rexuz 9673*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	rexuz2 9674*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	2rexuz 9675*	Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.)
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑))
Theorem	peano2uz 9676	Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
Theorem	peano2uzs 9677	Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍)
Theorem	peano2uzr 9678	Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	uzaddcl 9679	Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	nn0pzuz 9680	The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ) → (𝑁 + 𝑍) ∈ (ℤ≥‘𝑍))
Theorem	uzind4 9681*	Induction on the upper set of integers that starts at an integer 𝑀. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.)
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑀 ∈ ℤ → 𝜓)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	uzind4ALT 9682*	Induction on the upper set of integers that starts at an integer 𝑀. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 9681 or uzind4ALT 9682 may be used; see comment for nnind 9025. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑀 ∈ ℤ → 𝜓)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    &   ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	uzind4s 9683*	Induction on the upper set of integers that starts at an integer 𝑀, using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005.)
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑘]𝜑)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜑 → [(𝑘 + 1) / 𝑘]𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑘]𝜑)
Theorem	uzind4s2 9684*	Induction on the upper set of integers that starts at an integer 𝑀, using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 9683 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.)
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑)
Theorem	uzind4i 9685*	Induction on the upper integers that start at 𝑀. The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 9681 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 9625). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	indstr 9686*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	infrenegsupex 9687*	The infimum of a set of reals 𝐴 is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 14-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
Theorem	supinfneg 9688*	If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 9706. (Contributed by Jim Kingdon, 15-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))
Theorem	infsupneg 9689*	If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 9688. (Contributed by Jim Kingdon, 15-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
Theorem	supminfex 9690*	A supremum is the negation of the infimum of that set's image under negation. (Contributed by Jim Kingdon, 14-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) = -inf({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}, ℝ, < ))
Theorem	infregelbex 9691*	Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧))
Theorem	eluznn0 9692	Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0)
Theorem	eluznn 9693	Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)
Theorem	eluz2b1 9694	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
Theorem	eluz2gt1 9695	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁)
Theorem	eluz2b2 9696	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
Theorem	eluz2b3 9697	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
Theorem	uz2m1nn 9698	One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ ℕ)
Theorem	1nuz2 9699	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 9700	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))