Type  Label  Description 
Statement 

Theorem  eluzadd 8501 
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ ((𝑁 ∈ (ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈
(ℤ_{≥}‘(𝑀 + 𝐾))) 

Theorem  eluzsub 8502 
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2Sep2009.)

⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈
(ℤ_{≥}‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈
(ℤ_{≥}‘𝑀)) 

Theorem  uzm1 8503 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)

⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ_{≥}‘𝑀))) 

Theorem  uznn0sub 8504 
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4Sep2005.)

⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑁 − 𝑀) ∈
ℕ_{0}) 

Theorem  uzin 8505 
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24Dec2013.)

⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((ℤ_{≥}‘𝑀) ∩ (ℤ_{≥}‘𝑁)) =
(ℤ_{≥}‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) 

Theorem  uzp1 8506 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)

⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈
(ℤ_{≥}‘(𝑀 + 1)))) 

Theorem  nn0uz 8507 
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2Sep2005.)

⊢ ℕ_{0} =
(ℤ_{≥}‘0) 

Theorem  nnuz 8508 
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2Sep2005.)

⊢ ℕ =
(ℤ_{≥}‘1) 

Theorem  elnnuz 8509 
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6Jun2006.)

⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ_{≥}‘1)) 

Theorem  elnn0uz 8510 
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6Jun2006.)

⊢ (𝑁 ∈ ℕ_{0} ↔ 𝑁 ∈
(ℤ_{≥}‘0)) 

Theorem  eluz2nn 8511 
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3Nov2018.)

⊢ (𝐴 ∈ (ℤ_{≥}‘2)
→ 𝐴 ∈
ℕ) 

Theorem  eluzge2nn0 8512 
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27Aug2018.) (Proof shortened by AV,
3Nov2018.)

⊢ (𝑁 ∈ (ℤ_{≥}‘2)
→ 𝑁 ∈
ℕ_{0}) 

Theorem  uzuzle23 8513 
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, 17Sep2018.)

⊢ (𝐴 ∈ (ℤ_{≥}‘3)
→ 𝐴 ∈
(ℤ_{≥}‘2)) 

Theorem  eluzge3nn 8514 
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17Sep2018.)

⊢ (𝑁 ∈ (ℤ_{≥}‘3)
→ 𝑁 ∈
ℕ) 

Theorem  uz3m2nn 8515 
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17Sep2018.)

⊢ (𝑁 ∈ (ℤ_{≥}‘3)
→ (𝑁 − 2)
∈ ℕ) 

Theorem  1eluzge0 8516 
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.)

⊢ 1 ∈
(ℤ_{≥}‘0) 

Theorem  2eluzge0 8517 
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.) (Proof shortened by OpenAI, 25Mar2020.)

⊢ 2 ∈
(ℤ_{≥}‘0) 

Theorem  2eluzge0OLD 8518 
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.) Obsolete version of 2eluzge0 8517 as of
25Mar2020. (New usage is discouraged.)
(Proof modification is discouraged.)

⊢ 2 ∈
(ℤ_{≥}‘0) 

Theorem  2eluzge1 8519 
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8Jun2018.)

⊢ 2 ∈
(ℤ_{≥}‘1) 

Theorem  uznnssnn 8520 
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29Jun2013.)

⊢ (𝑁 ∈ ℕ →
(ℤ_{≥}‘𝑁) ⊆ ℕ) 

Theorem  raluz 8521* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)

⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈
(ℤ_{≥}‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) 

Theorem  raluz2 8522* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)

⊢ (∀𝑛 ∈ (ℤ_{≥}‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) 

Theorem  rexuz 8523* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)

⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈
(ℤ_{≥}‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) 

Theorem  rexuz2 8524* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)

⊢ (∃𝑛 ∈ (ℤ_{≥}‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) 

Theorem  2rexuz 8525* 
Double existential quantification in an upper set of integers.
(Contributed by NM, 3Nov2005.)

⊢ (∃𝑚∃𝑛 ∈ (ℤ_{≥}‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) 

Theorem  peano2uz 8526 
Second Peano postulate for an upper set of integers. (Contributed by NM,
7Sep2005.)

⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑁 + 1) ∈
(ℤ_{≥}‘𝑀)) 

Theorem  peano2uzs 8527 
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26Dec2013.)

⊢ 𝑍 = (ℤ_{≥}‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) 

Theorem  peano2uzr 8528 
Reversed second Peano axiom for upper integers. (Contributed by NM,
2Jan2006.)

⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ_{≥}‘(𝑀 + 1))) → 𝑁 ∈ (ℤ_{≥}‘𝑀)) 

Theorem  uzaddcl 8529 
Addition closure law for an upper set of integers. (Contributed by NM,
4Jun2006.)

⊢ ((𝑁 ∈ (ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ ℕ_{0}) → (𝑁 + 𝐾) ∈
(ℤ_{≥}‘𝑀)) 

Theorem  nn0pzuz 8530 
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,
3Oct2018.)

⊢ ((𝑁 ∈ ℕ_{0} ∧ 𝑍 ∈ ℤ) → (𝑁 + 𝑍) ∈
(ℤ_{≥}‘𝑍)) 

Theorem  uzind4 8531* 
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, 7Sep2005.)

⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → 𝜏) 

Theorem  uzind4ALT 8532* 
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 8531 or
uzind4ALT 8532 may be used; see comment for nnind 7930. (Contributed by NM,
7Sep2005.) (New usage is discouraged.)
(Proof modification is discouraged.)

⊢ (𝑀 ∈ ℤ → 𝜓)
& ⊢ (𝑘 ∈ (ℤ_{≥}‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → 𝜏) 

Theorem  uzind4s 8533* 
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, 4Nov2005.)

⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑘]𝜑)
& ⊢ (𝑘 ∈ (ℤ_{≥}‘𝑀) → (𝜑 → [(𝑘 + 1) / 𝑘]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → [𝑁 / 𝑘]𝜑) 

Theorem  uzind4s2 8534* 
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 8533 when 𝑗 and 𝑘 must
be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM,
16Nov2005.)

⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)
& ⊢ (𝑘 ∈ (ℤ_{≥}‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → [𝑁 / 𝑗]𝜑) 

Theorem  uzind4i 8535* 
Induction on the upper integers that start at 𝑀. The first
hypothesis specifies the lower bound, the next four give us the
substitution instances we need, and the last two are the basis and the
induction step. (Contributed by NM, 4Sep2005.)

⊢ 𝑀 ∈ ℤ & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → 𝜏) 

Theorem  indstr 8536* 
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17Aug2001.)

⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) 

Theorem  eluznn0 8537 
Membership in a nonnegative upper set of integers implies membership in
ℕ_{0}. (Contributed by Paul
Chapman, 22Jun2011.)

⊢ ((𝑁 ∈ ℕ_{0} ∧ 𝑀 ∈
(ℤ_{≥}‘𝑁)) → 𝑀 ∈
ℕ_{0}) 

Theorem  eluznn 8538 
Membership in a positive upper set of integers implies membership in
ℕ. (Contributed by JJ, 1Oct2018.)

⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ_{≥}‘𝑁)) → 𝑀 ∈ ℕ) 

Theorem  eluz2b1 8539 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈ (ℤ_{≥}‘2)
↔ (𝑁 ∈ ℤ
∧ 1 < 𝑁)) 

Theorem  eluz2b2 8540 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈ (ℤ_{≥}‘2)
↔ (𝑁 ∈ ℕ
∧ 1 < 𝑁)) 

Theorem  eluz2b3 8541 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈ (ℤ_{≥}‘2)
↔ (𝑁 ∈ ℕ
∧ 𝑁 ≠
1)) 

Theorem  uz2m1nn 8542 
One less than an integer greater than or equal to 2 is a positive integer.
(Contributed by Paul Chapman, 17Nov2012.)

⊢ (𝑁 ∈ (ℤ_{≥}‘2)
→ (𝑁 − 1)
∈ ℕ) 

Theorem  1nuz2 8543 
1 is not in (ℤ_{≥}‘2).
(Contributed by Paul Chapman,
21Nov2012.)

⊢ ¬ 1 ∈
(ℤ_{≥}‘2) 

Theorem  elnn1uz2 8544 
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17Nov2012.)

⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ_{≥}‘2))) 

Theorem  uz2mulcl 8545 
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26Oct2012.)

⊢ ((𝑀 ∈ (ℤ_{≥}‘2)
∧ 𝑁 ∈
(ℤ_{≥}‘2)) → (𝑀 · 𝑁) ∈
(ℤ_{≥}‘2)) 

Theorem  indstr2 8546* 
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, 21Nov2012.)

⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜒 & ⊢ (𝑥 ∈
(ℤ_{≥}‘2) → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) 

Theorem  eluzdc 8547 
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18Apr2020.)

⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁
∈ (ℤ_{≥}‘𝑀)) 

Theorem  ublbneg 8548* 
The image under negation of a boundedabove set of reals is bounded
below. (Contributed by Paul Chapman, 21Mar2011.)

⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ 𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) 

Theorem  eqreznegel 8549* 
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21Mar2011.)

⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ 𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴}) 

Theorem  negm 8550* 
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10Apr2020.)

⊢ ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ {𝑧 ∈ ℝ ∣ 𝑧 ∈ 𝐴}) 

Theorem  lbzbi 8551* 
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21Mar2011.)

⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) 

Theorem  nn01to3 8552 
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13Sep2018.)

⊢ ((𝑁 ∈ ℕ_{0} ∧ 1 ≤
𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) 

Theorem  nn0ge2m1nnALT 8553 
Alternate proof of nn0ge2m1nn 8242: 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 8479, 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 8242. (Contributed by Alexander van der Vekens,
1Aug2018.)
(New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝑁 ∈ ℕ_{0} ∧ 2 ≤
𝑁) → (𝑁 − 1) ∈
ℕ) 

3.4.11 Rational numbers (as a subset of complex
numbers)


Syntax  cq 8554 
Extend class notation to include the class of rationals.

class ℚ 

Definition  dfq 8555 
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 8557
for the relation "is rational." (Contributed
by NM, 8Jan2002.)

⊢ ℚ = ( / “ (ℤ ×
ℕ)) 

Theorem  divfnzn 8556 
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, 19Mar2020.)

⊢ ( / ↾ (ℤ × ℕ)) Fn
(ℤ × ℕ) 

Theorem  elq 8557* 
Membership in the set of rationals. (Contributed by NM, 8Jan2002.)
(Revised by Mario Carneiro, 28Jan2014.)

⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) 

Theorem  qmulz 8558* 
If 𝐴 is rational, then some integer
multiple of it is an integer.
(Contributed by NM, 7Nov2008.) (Revised by Mario Carneiro,
22Jul2014.)

⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℕ (𝐴 · 𝑥) ∈ ℤ) 

Theorem  znq 8559 
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12Jan2002.)

⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) 

Theorem  qre 8560 
A rational number is a real number. (Contributed by NM,
14Nov2002.)

⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) 

Theorem  zq 8561 
An integer is a rational number. (Contributed by NM, 9Jan2002.)

⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) 

Theorem  zssq 8562 
The integers are a subset of the rationals. (Contributed by NM,
9Jan2002.)

⊢ ℤ ⊆ ℚ 

Theorem  nn0ssq 8563 
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31Jul2004.)

⊢ ℕ_{0} ⊆
ℚ 

Theorem  nnssq 8564 
The positive integers are a subset of the rationals. (Contributed by NM,
31Jul2004.)

⊢ ℕ ⊆ ℚ 

Theorem  qssre 8565 
The rationals are a subset of the reals. (Contributed by NM,
9Jan2002.)

⊢ ℚ ⊆ ℝ 

Theorem  qsscn 8566 
The rationals are a subset of the complex numbers. (Contributed by NM,
2Aug2004.)

⊢ ℚ ⊆ ℂ 

Theorem  qex 8567 
The set of rational numbers exists. (Contributed by NM, 30Jul2004.)
(Revised by Mario Carneiro, 17Nov2014.)

⊢ ℚ ∈ V 

Theorem  nnq 8568 
A positive integer is rational. (Contributed by NM, 17Nov2004.)

⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) 

Theorem  qcn 8569 
A rational number is a complex number. (Contributed by NM,
2Aug2004.)

⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) 

Theorem  qaddcl 8570 
Closure of addition of rationals. (Contributed by NM, 1Aug2004.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) 

Theorem  qnegcl 8571 
Closure law for the negative of a rational. (Contributed by NM,
2Aug2004.) (Revised by Mario Carneiro, 15Sep2014.)

⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℚ) 

Theorem  qmulcl 8572 
Closure of multiplication of rationals. (Contributed by NM,
1Aug2004.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) 

Theorem  qsubcl 8573 
Closure of subtraction of rationals. (Contributed by NM, 2Aug2004.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) 

Theorem  qapne 8574 
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20Mar2020.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵)) 

Theorem  qltlen 8575 
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7621 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11Oct2021.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) 

Theorem  qreccl 8576 
Closure of reciprocal of rationals. (Contributed by NM, 3Aug2004.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) 

Theorem  qdivcl 8577 
Closure of division of rationals. (Contributed by NM, 3Aug2004.)

⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) 

Theorem  qrevaddcl 8578 
Reverse closure law for addition of rationals. (Contributed by NM,
2Aug2004.)

⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) 

Theorem  nnrecq 8579 
The reciprocal of a positive integer is rational. (Contributed by NM,
17Nov2004.)

⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈
ℚ) 

Theorem  irradd 8580 
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7Nov2008.)

⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℚ)) 

Theorem  irrmul 8581 
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). (Contributed by NM, 7Nov2008.)

⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ ∧
𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖
ℚ)) 

3.4.12 Complex numbers as pairs of
reals


Theorem  cnref1o 8582* 
There is a natural onetoone mapping from (ℝ ×
ℝ) to ℂ,
where we map ⟨𝑥, 𝑦⟩ to (𝑥 + (i · 𝑦)). In our
construction of the complex numbers, this is in fact our
definition of
ℂ (see dfc 6895), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16Jun2013.) (Revised by Mario Carneiro,
17Feb2014.)

⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ 𝐹:(ℝ × ℝ)–11onto→ℂ 

3.5 Order sets


3.5.1 Positive reals (as a subset of complex
numbers)


Syntax  crp 8583 
Extend class notation to include the class of positive reals.

class ℝ^{+} 

Definition  dfrp 8584 
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27Oct2007.)

⊢ ℝ^{+} = {𝑥 ∈ ℝ ∣ 0 < 𝑥} 

Theorem  elrp 8585 
Membership in the set of positive reals. (Contributed by NM,
27Oct2007.)

⊢ (𝐴 ∈ ℝ^{+} ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) 

Theorem  elrpii 8586 
Membership in the set of positive reals. (Contributed by NM,
23Feb2008.)

⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈
ℝ^{+} 

Theorem  1rp 8587 
1 is a positive real. (Contributed by Jeff Hankins, 23Nov2008.)

⊢ 1 ∈
ℝ^{+} 

Theorem  2rp 8588 
2 is a positive real. (Contributed by Mario Carneiro, 28May2016.)

⊢ 2 ∈
ℝ^{+} 

Theorem  rpre 8589 
A positive real is a real. (Contributed by NM, 27Oct2007.)

⊢ (𝐴 ∈ ℝ^{+} → 𝐴 ∈
ℝ) 

Theorem  rpxr 8590 
A positive real is an extended real. (Contributed by Mario Carneiro,
21Aug2015.)

⊢ (𝐴 ∈ ℝ^{+} → 𝐴 ∈
ℝ^{*}) 

Theorem  rpcn 8591 
A positive real is a complex number. (Contributed by NM, 11Nov2008.)

⊢ (𝐴 ∈ ℝ^{+} → 𝐴 ∈
ℂ) 

Theorem  nnrp 8592 
A positive integer is a positive real. (Contributed by NM,
28Nov2008.)

⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ^{+}) 

Theorem  rpssre 8593 
The positive reals are a subset of the reals. (Contributed by NM,
24Feb2008.)

⊢ ℝ^{+} ⊆
ℝ 

Theorem  rpgt0 8594 
A positive real is greater than zero. (Contributed by FL,
27Dec2007.)

⊢ (𝐴 ∈ ℝ^{+} → 0 <
𝐴) 

Theorem  rpge0 8595 
A positive real is greater than or equal to zero. (Contributed by NM,
22Feb2008.)

⊢ (𝐴 ∈ ℝ^{+} → 0 ≤
𝐴) 

Theorem  rpregt0 8596 
A positive real is a positive real number. (Contributed by NM,
11Nov2008.) (Revised by Mario Carneiro, 31Jan2014.)

⊢ (𝐴 ∈ ℝ^{+} → (𝐴 ∈ ℝ ∧ 0 <
𝐴)) 

Theorem  rprege0 8597 
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31Jan2014.)

⊢ (𝐴 ∈ ℝ^{+} → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) 

Theorem  rpne0 8598 
A positive real is nonzero. (Contributed by NM, 18Jul2008.)

⊢ (𝐴 ∈ ℝ^{+} → 𝐴 ≠ 0) 

Theorem  rpap0 8599 
A positive real is apart from zero. (Contributed by Jim Kingdon,
22Mar2020.)

⊢ (𝐴 ∈ ℝ^{+} → 𝐴 # 0) 

Theorem  rprene0 8600 
A positive real is a nonzero real number. (Contributed by NM,
11Nov2008.)

⊢ (𝐴 ∈ ℝ^{+} → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) 