P. 100 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9901-10000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uzuzle24 9901	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	uzuzle34 9902	An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ (ℤ≥‘3))
Theorem	uzuzle35 9903	An integer greater than or equal to 5 is an integer greater than or equal to 3. (Contributed by AV, 15-Nov-2025.)
⊢ (𝐴 ∈ (ℤ≥‘5) → 𝐴 ∈ (ℤ≥‘3))
Theorem	eluz2nn 9904	An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)
Theorem	eluz3nn 9905	An integer greater than or equal to 3 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) (Proof shortened by AV, 30-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ)
Theorem	eluz4eluz2 9906	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 9907	An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ)
Theorem	eluzge2nn0 9908	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 9909	An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0)
Theorem	eluzge3nn 9910	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 9911	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 9912	1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 1 ∈ (ℤ≥‘0)
Theorem	2eluzge0 9913	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 9914	2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 2 ∈ (ℤ≥‘1)
Theorem	uznnssnn 9915	The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ)
Theorem	raluz 9916*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	raluz2 9917*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑)))
Theorem	rexuz 9918*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	rexuz2 9919*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑)))
Theorem	2rexuz 9920*	Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.)
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑))
Theorem	peano2uz 9921	Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
Theorem	peano2uzs 9922	Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍)
Theorem	peano2uzr 9923	Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	uzaddcl 9924	Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	nn0pzuz 9925	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 9926*	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 9927*	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 9926 or uzind4ALT 9927 may be used; see comment for nnind 9258. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑀 ∈ ℤ → 𝜓)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    &   ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	uzind4s 9928*	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 9929*	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 9928 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.)
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑)
Theorem	uzind4i 9930*	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 9926 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 9864). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏)
Theorem	indstr 9931*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	infrenegsupex 9932*	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 9933*	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 9951. (Contributed by Jim Kingdon, 15-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))
Theorem	infsupneg 9934*	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 9933. (Contributed by Jim Kingdon, 15-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
Theorem	supminfex 9935*	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 9936*	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 9937	Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0)
Theorem	eluznn 9938	Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)
Theorem	eluz2b1 9939	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
Theorem	eluz2gt1 9940	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁)
Theorem	eluz2b2 9941	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
Theorem	eluz2b3 9942	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
Theorem	uz2m1nn 9943	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 9944	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 9945	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))
Theorem	uz2mulcl 9946	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2))
Theorem	indstr2 9947*	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	eluzdc 9948	Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	elnn0dc 9949	Membership of an integer in ℕ0 is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
⊢ (𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ0)
Theorem	elnndc 9950	Membership of an integer in ℕ is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
⊢ (𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ)
Theorem	ublbneg 9951*	The image under negation of a bounded-above set of reals is bounded below. For a theorem which is similar but also adds that the bounds need to be the tightest possible, see supinfneg 9933. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦)
Theorem	eqreznegel 9952*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴})
Theorem	negm 9953*	The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴})
Theorem	lbzbi 9954*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))
Theorem	nn01to3 9955	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 9956	Alternate proof of nn0ge2m1nn 9565: 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 9865, 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 9565. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ)
4.4.12  Rational numbers (as a subset of complex numbers)
Syntax	cq 9957	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 9958	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 9960 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	divfnzn 9959	Division restricted to ℤ × ℕ is a function. Given excluded middle, it would be easy to prove this for ℂ × (ℂ ∖ {0}). The key difference is that an element of ℕ is apart from zero, whereas being an element of ℂ ∖ {0} implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ ( / ↾ (ℤ × ℕ)) Fn (ℤ × ℕ)
Theorem	elq 9960*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 9961*	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 9962	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 9963	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 9964	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	zssq 9965	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 9966	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 9967	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ ⊆ ℚ
Theorem	qssre 9968	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
⊢ ℚ ⊆ ℝ
Theorem	qsscn 9969	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℚ ⊆ ℂ
Theorem	qex 9970	The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℚ ∈ V
Theorem	nnq 9971	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ)
Theorem	qcn 9972	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Theorem	qaddcl 9973	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)
Theorem	qnegcl 9974	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ)
Theorem	qmulcl 9975	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ)
Theorem	qsubcl 9976	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ)
Theorem	qapne 9977	Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵))
Theorem	qltlen 9978	Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8911 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴)))
Theorem	qlttri2 9979	Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 9-Nov-2021.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	qreccl 9980	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ)
Theorem	qdivcl 9981	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qrevaddcl 9982	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ))
Theorem	nnrecq 9983	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ)
Theorem	irradd 9984	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmul 9985	The product of a real which is not rational with a nonzero rational is not rational. Note that by "not rational" we mean the negation of "is rational" (whereas "irrational" is often defined to mean apart from any rational number - given excluded middle these two definitions would be equivalent). For a similar theorem with irrational in place of not rational, see irrmulap 9986. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmulap 9986*	The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 9985. (Contributed by Jim Kingdon, 25-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℚ 𝐴 # 𝑞)    &   ⊢ (𝜑 → 𝐵 ∈ ℚ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) # 𝑄)
Theorem	elpq 9987*	A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	elpqb 9988*	A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
4.4.13  Complex numbers as pairs of reals
Theorem	cnref1o 9989*	There is a natural one-to-one mapping from (ℝ × ℝ) to ℂ, where we map ⟨𝑥, 𝑦⟩ to (𝑥 + (i · 𝑦)). In our construction of the complex numbers, this is in fact our definition of ℂ (see df-c 8138), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ
Theorem	addex 9990	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ + ∈ V
Theorem	mulex 9991	The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ · ∈ V
4.5  Order sets
4.5.1  Positive reals (as a subset of complex numbers)
Syntax	crp 9992	Extend class notation to include the class of positive reals.
class ℝ+
Definition	df-rp 9993	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	elrp 9994	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	elrpii 9995	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ∈ ℝ+
Theorem	1rp 9996	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ 1 ∈ ℝ+
Theorem	2rp 9997	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ 2 ∈ ℝ+
Theorem	3rp 9998	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 3 ∈ ℝ+
Theorem	rpre 9999	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
Theorem	rpxr 10000	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)