P. 128 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eluz 12701	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
Theorem	uzid 12702	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzidd 12703	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzn0 12704	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅)
Theorem	uztrn 12705	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁))
Theorem	uztrn2 12706	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝐾)    ⇒   ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)
Theorem	uzneg 12707	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁))
Theorem	uzssz 12708	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	uzssre 12709	An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (ℤ≥‘𝑀) ⊆ ℝ
Theorem	uzss 12710	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	uztric 12711	Totality 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 12712	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁))
Theorem	eluzp1m1 12713	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
Theorem	eluzp1l 12714	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	eluzp1p1 12715	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
Theorem	eluzaddi 12716	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsubi 12717	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	eluzadd 12718	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsub 12719	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	subeluzsub 12720	Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀 − 𝐾) ∈ (ℤ≥‘(𝑀 − 𝑁)))
Theorem	uzm1 12721	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀)))
Theorem	uznn0sub 12722	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0)
Theorem	uzin 12723	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	uzp1 12724	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
Theorem	nn0uz 12725	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ0 = (ℤ≥‘0)
Theorem	nnuz 12726	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ = (ℤ≥‘1)
Theorem	elnnuz 12727	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))
Theorem	elnn0uz 12728	A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
Theorem	eluz2nn 12729	An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)
Theorem	eluz4eluz2 12730	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 12731	An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ)
Theorem	eluzge2nn0 12732	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 12733	An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0)
Theorem	uzuzle23 12734	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 12735	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 12736	An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 12768. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ)
Theorem	1eluzge0 12737	1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 1 ∈ (ℤ≥‘0)
Theorem	2eluzge0 12738	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 12739	2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 2 ∈ (ℤ≥‘1)
Theorem	uznnssnn 12740	The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ)
Theorem	raluz 12741*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	raluz2 12742*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	rexuz 12743*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	rexuz2 12744*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	2rexuz 12745*	Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.)
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑))
Theorem	peano2uz 12746	Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
Theorem	peano2uzs 12747	Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍)
Theorem	peano2uzr 12748	Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	uzaddcl 12749	Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	nn0pzuz 12750	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 12751*	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 12752*	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 12751 or uzind4ALT 12752 may be used; see comment for nnind 12096. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑀 ∈ ℤ → 𝜓)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    &   ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	uzind4s 12753*	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 12754*	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 12753 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.)
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑)
Theorem	uzind4i 12755*	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 12751 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 12692). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	uzwo 12756*	Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
Theorem	uzwo2 12757*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃!𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
Theorem	nnwo 12758*	Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.)
⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnwof 12759*	Well-ordering principle: any nonempty set of positive integers has a least element. This version allows 𝑥 and 𝑦 to be present in 𝐴 as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnwos 12760*	Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
Theorem	indstr 12761*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	eluznn0 12762	Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0)
Theorem	eluznn 12763	Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)
Theorem	eluz2b1 12764	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
Theorem	eluz2gt1 12765	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁)
Theorem	eluz2b2 12766	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
Theorem	eluz2b3 12767	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
Theorem	uz2m1nn 12768	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 12769	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 12770	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))
Theorem	uz2mulcl 12771	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2))
Theorem	indstr2 12772*	Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜒    &   ⊢ (𝑥 ∈ (ℤ≥‘2) → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	uzinfi 12773	Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ inf((ℤ≥‘𝑀), ℝ, < ) = 𝑀
Theorem	nninf 12774	The infimum of the set of positive integers is one. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.)
⊢ inf(ℕ, ℝ, < ) = 1
Theorem	nn0inf 12775	The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.)
⊢ inf(ℕ0, ℝ, < ) = 0
Theorem	infssuzle 12776	The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	infssuzcl 12777	The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → inf(𝑆, ℝ, < ) ∈ 𝑆)
Theorem	ublbneg 12778*	The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦)
Theorem	eqreznegel 12779*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴})
Theorem	supminf 12780*	The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011.) ( Revised by AV, 13-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
Theorem	lbzbi 12781*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))
Theorem	zsupss 12782*	Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 11054.) (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suprzcl2 12783*	The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12505 avoids ax-pre-sup 11054.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	suprzub 12784*	The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	uzsupss 12785*	Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 21-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	nn01to3 12786	A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))
Theorem	nn0ge2m1nnALT 12787	Alternate proof of nn0ge2m1nn 12407: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 12693, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 12407. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ)
5.4.12  Well-ordering principle for bounded-below sets of integers
Theorem	uzwo3 12788*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12757 allows the lower bound 𝐵 to be any real number. See also nnwo 12758 and nnwos 12760. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	zmin 12789*	There is a unique smallest integer greater than or equal to a given real number. (Contributed by NM, 12-Nov-2004.) (Revised by Mario Carneiro, 13-Jun-2014.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))
Theorem	zmax 12790*	There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))
Theorem	zbtwnre 12791*	There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28. (Contributed by NM, 13-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))
Theorem	rebtwnz 12792*	There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))
5.4.13  Rational numbers (as a subset of complex numbers)
Syntax	cq 12793	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 12794	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12795 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	elq 12795*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 12796*	If 𝐴 is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℕ (𝐴 · 𝑥) ∈ ℤ)
Theorem	znq 12797	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 12798	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 12799	An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	qred 12800	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)